Static semantics v0.1

doc/definition/static-semantics.tex

+\subsection*{Field lookup}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\
+          \fieldDecl{x}{\tau} \in \many{\mathit{ce}}
+        }
+        {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad x \notin \many{\mathit{ce}} \\
+         \fieldLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{x}{\tau}
+        }
+        {\fieldLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+        }
+
+
+\subsection*{Method lookup}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \\
+          \methodDecl{m}{\tau}{\sigma} \in \many{\mathit{ce}}
+        }
+        {\methodLookup{\Phi}
+          {\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\sigma}}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad m \notin \many{\mathit{ce}} \\
+         \methodLookup{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{m}{\tau}{\sigma}
+        }
+        {\methodLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+          {\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\sigma}}
+        }
+
+\subsection*{Method and field absence}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad x \notin \many{\mathit{ce}} \\
+         \fieldAbsent{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{x}
+        }
+        {\fieldAbsent{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{x}
+        }
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\many{\mathit{ce}}}) \in \Phi \quad m \notin \many{\mathit{ce}} \\
+         \methodAbsent{\Phi}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{m}{\tau}{\sigma}
+        }
+        {\methodAbsent{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}
+        }
+
+\iftrans{
+
+\subsection*{Type translation}
+
+To translate covariant generics, we essentially want to treat all contravariant
+occurrences of type variables as $\Dynamic$.  The type translation
+$\down{\tau}$ implements this.  It is defined in terms of the dual operator
+$\up{\tau}$ which translates positive occurences of type variables as $\Dynamic$.
+
+\begin{eqnarray*}
+  \down{T} & = & T \\
+  \down{\Arrow[k]{\tau_0, \ldots, \tau_n}{\tau_r}} & = & 
+     \Arrow[k]{\up{\tau_0}, \ldots, \up{\tau_n}}{\down{\tau_r}} \\
+  \down{\TApp{C}{\tau_0, \ldots, \tau_n}} & = & \TApp{C}{\down{\tau_0}, \ldots, \down{\tau_n}} \\
+  \down{\tau} & = & \tau\ \mbox{if $\tau$ is base type.}

[vsm, 2015/07/28 15:44:32]

What is a "base type" in this case?

Also, if I have (for any T):

class Foo extends List<T> { ... }

Is \down{Foo}  == Foo?

[Leaf, 2015/07/28 20:34:29]

Anything which is not one of the previous three cases.  Maybe I should just say
"otherwise".
Yes.  I'm a little bit informal with the syntax in a way that doesn't matter. 
Technically in this syntax, you would have to write Foo<>.  

+\end{eqnarray*}
+
+\begin{eqnarray*}
+  \up{T} & = & \Dynamic \\
+  \up{\Arrow[k]{\tau_0, \ldots, \tau_n}{\tau_r}} & = & 
+     \Arrow[k]{\down{\tau_0}, \ldots, \down{\tau_n}}{\up{\tau_r}} \\
+  \up{\TApp{C}{\tau_0, \ldots, \tau_n}} & = & \TApp{C}{\up{\tau_0}, \ldots, \up{\tau_n}} \\
+  \up{\tau} & = & \tau\ \mbox{if $\tau$ is base type.}
+\end{eqnarray*}
+
+
+}
 \subsection*{Expression typing: $\yieldsOk{\Phi, \Delta, \Gamma}{e}{\opt{\tau}}{e'}{\tau'}$} 
 \hrulefill\\
 
 
 \sstext{ Expression typing is a relation between typing contexts, a term ($e$),
   an optional type ($\opt{\tau}$), and a type ($\tau'$).  The general idea is
   that we are typechecking a term ($e$) and want to know if it is well-typed.
   The term appears in a context, which may (or may not) impose a type constraint
   on the term.  For example, in $\dvar{x:\tau}{e}$, $e$ appears in a context
   which requires it to be a subtype of $\tau$, or to be coercable to $\tau$.
@@ skipping 70 matching lines @@
 declared types.  
 }{
 
 A fully annotated function elaborates to a function with an elaborated body.
 The rest of the function elaboration rules fill in the reified type using
 contextual information if present and applicable, or $\Dynamic$ otherwise.
 
 }
 
 \infrule{\Gamma' = \extends{\Gamma}{\many{x}}{\many{\tau}} \quad\quad 
-         \yieldsOk{\Phi, \Delta, \Gamma'}{e}{\sigma}{e'}{\sigma'}
+         \stmtOk{\Phi, \Delta, \Gamma'}{s}{\sigma}{s'}{\Gamma'}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\tau}}{\sigma}{e}}
+                  {\elambda{\many{x:\tau}}{\sigma}{s}}
                   {\_}
-                  {\elambda{\many{x:\tau}}{\sigma}{e'}}
+                  {\elambda{\many{x:\tau}}{\sigma}{s'}}
                   {\Arrow[-]{\many{\tau}}{\sigma}}
         } 
 
 \sstext{A function with a missing argument type is well-typed if it is well-typed with
 the argument type replaced with $\Dynamic$.}
 {}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\Dynamic, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\Dynamic, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\opt{\tau}}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\opt{\tau}}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing argument type is well-typed if it is well-typed with
 the argument type replaced with the corresponding argument type from the context
 type.  Note that this rule overlaps with the previous: the formal presentation
 leaves this as a non-deterministic choice.}{}
 
 \infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\upsilon_i, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\upsilon_i, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing return type is well-typed if it is well-typed with
 the return type replaced with $\Dynamic$.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\Dynamic}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\Dynamic}{s}}
                   {\opt{\tau_c}}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{s}}
                   {\opt{\tau_c}}
                   {e_f}
                   {\tau_f}
         } 
 
 \sstext{A function with a missing return type is well-typed if it is well-typed with
 the return type replaced with the corresponding return type from the context
 type.  Note that this rule overlaps with the previous: the formal presentation
 leaves this as a non-deterministic choice.  }{}
 
 \infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\upsilon_r}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\upsilon_r}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
-                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{s}}
                   {\tau_c}
                   {e_f}
                   {\tau_f}
         } 
 
 
 \sstext{Instance creation creates an instance of the appropriate type.}{}
 
 % FIXME(leafp): inference
 % FIXME(leafp): deal with bounds
@@ skipping 72 matching lines @@
                   {e_a'}
                   {\tau_a'} \quad \mbox{for}\ e_a \in \many{e_a}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\ecall{e}{\many{e_a}}}
                   {\_}
                   {\edcall{e'}{\many{e_a'}}}
                   {\Dynamic}
         } 
 
+\iftrans{
 \sstext{A dynamic call expression is well-typed so long as the applicand and the
 arguments are well-typed at any type.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\Dynamic}
                   {e'}
                   {\tau} \\
          \yieldsOk{\Phi, \Delta, \Gamma}
                   {e_a}
                   {\_}
                   {e_a'}
                   {\tau_a} \quad \mbox{for}\ e_a \in \many{e_a}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\edcall{e}{\many{e_a}}}
                   {\_}
                   {\edcall{e'}{\many{e_a'}}}
                   {\Dynamic}
         }
 
+}
+
 \sstext{A method load is well-typed if the term is well-typed, and the method name is
 present in the type of the term.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\_}
                   {e'}
                   {\sigma} \quad\quad
-         \methodLookup{\Phi}{\sigma}{m}{\tau}
+         \methodLookup{\Phi}{\sigma}{m}{\sigma}{\tau}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{e}{m}}
                   {\_}
                   {\eload{e'}{m}}
                   {\tau}
         }
 
 \sstext{A method load from a term of type $\Dynamic$ is well-typed if the term is
 well-typed.}
@@ skipping 10 matching lines @@
                   {e'}
                   {\tau} 
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{e}{m}}
                   {\_}
                   {\edload{e'}{m}}
                   {\Dynamic}
         }
 
+\iftrans{
 \sstext{A dynamic method load is well typed so long as the term is well-typed.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}
                   {e}
                   {\Dynamic}
                   {e'}
                   {\tau} 
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\edload{e}{m}}
                   {\_}
                   {\edload{e'}{m}}
                   {\Dynamic}
         }
 
+}
+
 \sstext{A field load from $\ethis$ is well-typed if the field name is present in the
 type of $\ethis$.}{}
 
 \infrule{\Gamma = \Gamma_\tau & \fieldLookup{\Phi}{\tau}{x}{\sigma}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eload{\ethis}{x}}
                   {\_}
                   {\eload{\ethis}{x}}
                   {\sigma}
@@ skipping 46 matching lines @@
                   {\ethrow}
                   {\_}
                   {\ethrow}
                   {\sigma}
         } 
 
 \sstext{A cast expression is well-typed so long as the term being cast is well-typed.
 The synthesized type is the cast-to type.  We require that the cast-to type be a
 ground type.}{}
 
-\comment{TODO(leafp): specify ground types}

[vsm, 2015/07/28 15:44:32]

Did you add a definition of ground type?  I don't see it.

[Leaf, 2015/07/28 20:34:29]

Done.

-
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad \mbox{$\tau$ is ground}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eas{e}{\tau}}
                   {\_}
                   {\eas{e'}{\tau}}
                   {\tau}
         } 
 
 \sstext{An instance check expression is well-typed if the term being checked is
 well-typed. We require that the cast to-type be a ground type.}{}
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad \mbox{$\tau$ is ground}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\eis{e}{\tau}}
                   {\_}
                   {\eis{e'}{\tau}}
                   {\Bool}
         } 
 
+\iftrans{
+
 \sstext{A check expression is well-typed so long as the term being checked is
 well-typed.  The synthesized type is the target type of the check.}{}
 
 
 \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma}
         }
         {\yieldsOk{\Phi, \Delta, \Gamma}
                   {\echeck{e}{\tau}}
                   {\_}
                   {\echeck{e'}{\tau}}
                   {\tau}
         } 
 
+}
+
 \subsection*{Declaration typing: $\declOk[d]{\Phi, \Delta, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}$}
 \hrulefill\\
 
 \sstext{
 Variable declaration typing checks the well-formedness of the components, and
 produces an output context $\Gamma'$ which contains the binding introduced by
 the declaration.
 
 A simple variable declaration with a declared type is well-typed if the
 initializer for the declaration is well-typed at the declared type.  The output
@@ skipping 102 matching lines @@
 \sstext{A sequence statement is well-typed if the first component is well-typed, and the
 second component is well-typed with the output context of the first component as
 its input context.  The final output context is the output context of the second
 component.}{}
 
 \infrule{\stmtOk{\Phi, \Delta, \Gamma}{s_1}{\tau_r}{s_1'}{\Gamma'} \quad\quad
          \stmtOk{\Phi, \Delta, \Gamma'}{s_2}{\tau_r}{s_2'}{\Gamma''}
         }
         {\stmtOk{\Phi, \Delta, \Gamma}{s_1;s_2}{\tau_r}{s_1';s_2'}{\Gamma''}
         }
+
+\subsection*{Class member typing:  $\declOk[ce]{\Phi, \Delta, \Gamma}{\mathit{vd} : \mathit{ce}}{\mathit{vd}'}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{ 
+
+A class member is well-typed with a given signature ($\mathit{ce}$) taken from
+the class hierarchy if the signature type matches the type on the definition,
+and if the definition is well-typed.
+
+}
+{
+
+Elaborating class members is done with respect to a signature.  The field
+translation simply translates the field as a variable declaration.
+
+}
+
+
+\infrule{
+          \declOk[d]{\Phi, \Delta, \Gamma}
+                 {\dvar{x:\opt{\tau}}{e}}
+                 {\mathit{vd'}}
+                 {\Gamma'}
+        }
+        {
+          \declOk[ce]{\Phi, \Delta, \Gamma}
+                 {\dvar{x:\opt{\tau}}{e} : \fieldDecl{x}{\opt{\tau}}}
+                 {\mathit{vd'}}
+                 {\Gamma'}
+        }
+
+
+\iftrans{
+
+Translating methods requires introducing guard expressions.  The signature
+provides an internal and an external type for the method.  The external type is
+the original declared type of the method, and is the signature which the method
+presents to external clients.  Because we implement covariant generics, clients
+may see an instantiation of this signature which will allow them to violate the
+contract expected by the implementation.  To handle this, we rewrite the method
+to match an internal signature which is in fact covariant in the type

[vsm, 2015/07/28 15:44:32]

"covariant" -> "soundly covariant"?  I was a little confused here as I think the
external signature is also covariant on the type parameters, but not in a sound
way.

[Leaf, 2015/07/28 20:34:29]

Rephrased and clarified.

+parameters.  This property is enforced in the override checking relation: from
+the perspective of this relation, there is simply another internal type which
+defines how to wrap the method with guards.
+
+The translation insists that the internal and external types be function types
+of the appropriate arity, and that the external type is equal to the type of the
+declaration.  The declaration is translated using the underlying function
+definition translation, but is then wrapped with guards to enforce the type
+contract, producing a valid function of the internal (covariant) type.  The
+original body of the function is wrapped in a lambda function, which is applied
+using a dynamic call which checks that the arguments (which may have negative
+occurrences of type variables which are treated as $\Dynamic$ in the internal
+type) are appropriate for the actual body.  The original function returns a type
+$\tau_r$ which may be a super-type of the internal type (since negative
+occurrences of type variables must be treated as dynamic), and so we insert a
+check expression to guard against runtime type mismatches here.
+
+This is a very simplistic translation for now.  We could choose, in the case
+that the body returns a lambda, to push the checking down into the lambda
+(essentially wrapping it in place).  
+
+}
+
+\infrule{ \mathit{vd} = \dfun{\tau_r}{f}{x_0:\tau_0, \ldots, x_n:\tau_n}{s} \\
+          \sigma_e = \Arrow[+]{\tau_0, \ldots, \tau_n}{\tau_r} 
+\iftrans{\quad\quad 
+                 \sigma_i = \Arrow{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r}
+} \\
+          \declOk[d]{\Phi, \Delta, \Gamma}
+                 {\mathit{vd}}
+                 {\dfun{\tau_r}{f}{x_0:\tau_0, \ldots, x_n:\tau_n}{s'}}
+                 {\Gamma'}
+\iftrans{\\
+                 e_g = \elambda{x_0:\tau_0, \ldots, x_n:\tau_n}{\tau_r}{s'}\\
+                 s_g = \sreturn{(\echeck{\edcall{e_g}{x_0 , \ldots, x_n}}{\upsilon_r})} \\
+                 \mathit{vd}_g = \dfun{\upsilon_r}{f}{x_0:\upsilon_0, \ldots, x_n:\upsilon_n}{s_g} 
+}
+        }
+        {
+          \declOk[ce]{\Phi, \Delta, \Gamma}
+                 {\mathit{vd} : \methodDecl{f}{\sigma_i}{\sigma_e}}
+                 {\mathit{vd}_g}
+                 {\Gamma'}
+        }
+
+\subsection*{Class declaration typing:  $\declOk[c]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{ 
+
+A class declaration is well-typed with a given signature ($\Sig$) taken from the
+class hierarchy if the signature matches the definition, and if each member of
+the class is well-typed with the corresponding signature from the class
+signature.  The members are checked with the generic type parameters bound in
+the type context, and with the type of the current class set as the type of
+$\ethis$ on the term context $\Gamma$.
+
+}
+{
+
+Elaboration of a class requires that the class hierarchy $\Phi$ have a matching
+signature for the class declaration.  Each class member in the class is
+elaborated using the corresponding class element from the signature.
+
+}
+
+
+\infrule{\mathit{cd} = \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\mathit{vd}_0, \ldots, \mathit{vd}_n} \\
+         (C : \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\mathit{ce}_0, \ldots, \many{ce}_n}) \in \Phi \\ 
+         \Delta = \many{T} \quad \Gamma_c = \Gamma_{\TApp{C}{\many{T}}} \\
+         \declOk[ce]{\Phi, \Delta, \Gamma_c}{\mathit{vd}_i : \mathit{ce}_i}{\mathit{vd}'_i}{\Gamma'} \quad\quad
+         \mbox{for}\ i \in 0, \ldots, n 
+\iftrans{\\
+         \mathit{cd'} = \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{vd'}}}
+}
+        }
+        {\declOk[c]{\Phi, \Gamma}
+                   {\mathit{cd}}
+                   {\mathit{cd'}}{\Gamma'}
+        }
+
+\subsection*{Override checking:\\  \quad\quad$\overrideOk{\Phi}
+                                             {\TApp{C}{T_0, \ldots, T_n}}
+                                             {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                                             {\mathit{ce}}$}
+\hrulefill\\
+
+\sstext{
+
+The override checking relation is the primary relation that checks the
+consistency of the class hierarchy.  We assume a non-cyclic class hierarchy as a
+syntactic pre-condition.  The override check relation checks that in a class
+declaration $\TApp{C}{T_0, \ldots, T_n}$ which extends $\TApp{G}{\tau_0, \ldots,
+  \tau_k}$, the definition of an element with signature $\mathit{ce}$ is valid.  
+
+}{
+
+Override checking remains largely the same, with the exception of additional
+consistency constraints on the internal signatures for methods.
+
+}
+
+\sstext{
+
+A field with the type elided is a valid override if the same field with type
+$\Dynamic$ is valid.
+
+}{
+
+}
+
+\infrule{
+           \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\Dynamic}}
+
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\_}}
+        }
+
+\sstext{
+
+A field with a type $\tau$ is a valid override if it appears in the super type
+with the same type.
+
+}{
+
+}
+
+\infrule{\fieldLookup{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{x}{\tau}
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\tau}}
+        }
+
+\sstext{
+
+A field with a type $\tau$ is a valid override if it does not appear in the super type.
+
+}{
+
+}
+
+\infrule{\fieldAbsent{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{x}
+        }
+        {
+         \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\fieldDecl{x}{\tau}}
+        }
+
+\sstext{
+
+A method with a type $\sigma$ is a valid override if it does not appear in the super type.
+
+}{
+
+For a non-override method, we require that the internal type $\tau$ be a subtype
+of $\down{\sigma}$ where $\sigma$ is the declared type.  Essentially, this
+enforces the property that the initial declaration of a method in the hierarchy
+has a covariant internal type.
+
+}
+
+\infrule{
+\iftrans{
+      \Delta = T_0, \ldots, T_n \quad\quad
+      \subtypeOf{\Phi, \Delta}{\tau}{\down{\sigma}}\ \\
+}
+      \methodAbsent{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{f}
+    }
+    {
+      \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\methodDecl{f}{\tau}{\sigma}}
+    }
+
+\sstext{
+
+A method with a type $\sigma$ is a valid override if it appears in the super
+type, and $\sigma$ is a subtype of the type of the method in the super class.
+
+}{
+
+For a method override, we reqire two coherence conditions.  As before, we

[vsm, 2015/07/28 15:44:32]

reqire -> require

[Leaf, 2015/07/28 20:34:29]

Done.

+require that the internal type $\tau$ be a subtype of the $\down{\sigma}$ where
+$\sigma$ is the external type.  Moreover, we also insist that the external type
+$\sigma$ be a subtype of the external type of the method in the superclass, and

[vsm, 2015/07/28 15:44:32]

I thought that external types would not soundly subtype due to covariance?

[Leaf, 2015/07/28 20:34:29]

In the presence of variant type parameters, you can think of their being two
aspects to sound subtyping.  1) Are the parameters used according to their
variance, and 2) are the types subtypes.  When we say that we have covariant
generics, what we mean is that we elide #1, and just pretend all type parameters
are only used covariantly, even though they aren't.  We do still require that #2
hold though.  So if we're subtyping List<int> and overriding add, our external
type needs to be a subtype  of int -> void: we don't allow you to override with
String -> void, but you could override with Object -> void.  The subtyping is
correct, but because List is not actually covariant in T, the override is still
unsound: add originally had type T -> void, which is not covariant in T.  The
internal type of add in List will be dynamic -> void, which is properly
covariant, and so the internal override is sound.

+that the internal type $\tau$ be a subtype of the internal type in the
+superclass.  Note that it this last consistency property that ensures that
+covariant generics are ``poisonous'' in the sense that non-generic subclasses of
+generic classes must still have additional checks.  For example, a superclass
+with a method of external type $\sigma_s = \Arrow{T}{T}$ will have internal type
+$\tau_s = \Arrow{\Dynamic}{T}$.  A subclass of an instantiation of this class
+with $\Num$ can validly override this method with one of external type $\sigma =
+\Arrow{\Num}{\Num}$.  This is unsound in general since the argument occurrence
+of $T$ in $\sigma_s$ is contra-variant.  However, the additional consistency
+requirement is that the internal type of the subclass method must be a subtype
+of $\subst{\Num}{T}{\tau_s} = \Arrow{\Dynamic}{\Num}$.  This enforces the
+property that the overriden method must expect to be used at type

[vsm, 2015/07/28 15:44:32]

overriden -> overridden

[Leaf, 2015/07/28 20:34:29]

Done.

+$\Arrow{\Dynamic}{\Num}$, and hence must check its arguments (and potentially
+its return value as well in the higher-order case).  This checking code is
+inserted during the elaboration of class members above.
+
+  }
+
+\infrule{
+\iftrans{
+      \Delta = T_0, \ldots, T_n \quad\quad 
+      \subtypeOf{\Phi, \Delta}{\tau}{\down{\sigma}}\ \\
+}
+      \methodLookup{\Phi}{\TApp{G}{\tau_0, \ldots, \tau_k}}{f}{\tau_s}{\sigma_s} \\
+\iftrans{
+      \subtypeOf{\Phi, \Delta}{\tau}{\tau_s}\quad\quad 
+}
+      \subtypeOf{\Phi, \Delta}{\sigma}{\sigma_s}
+    }
+    {
+      \overrideOk{\Phi}
+                 {\TApp{C}{T_0, \ldots, T_n}}
+                 {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                 {\methodDecl{f}{\tau}{\sigma}}
+    }
+
+\subsection*{Toplevel declaration typing:  $\declOk[t]{\Phi, \Gamma}{\mathit{td}}{\mathit{td'}}{\Gamma'}$}
+\hrulefill\\
+
+\sstext{
+
+Top level variable declarations are well-typed if they are well-typed according
+to their respective specific typing relations.
+
+}{
+
+Top level declaration elaboration falls through to the underlying variable and
+class declaration code.
+
+}
+
+\infrule
+    {\declOk[d]{\Phi, \epsilon, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}
+      
+    }
+    {\declOk[t]{\Phi, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}
+    }
+
+\infrule
+    {\declOk[c]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}
+      
+    }
+    {\declOk[t]{\Phi, \Gamma}{\mathit{cd}}{\mathit{cd'}}{\Gamma'}
+    }
+
+
+\subsection*{Well-formed class signature:  $\ok{\Phi}{\Sig}$}
+\hrulefill\\
+
+\sstext{
+
+The well-formed class signature relation checks whether a class signature is
+well-formed with respect to a given class hierarchy $\Phi$.
+
+}{
+
+}
+
+\sstext{
+
+The $\Object$ signature is always well-formed.
+
+}{
+
+}
+
+\axiom{\ok{\Phi}{\Object}
+      }
+
+\sstext{
+
+A signature for a class $C$ is well-formed if its super-class signature is
+well-formed, and if every element in its signature is a valid override of the
+super-class.
+
+}{
+
+}
+
+\infrule{\Sig = \dclass{\TApp{C}{\many{T}}}
+                              {\TApp{G}{\tau_0, \ldots, \tau_k}}
+                              {\mathit{ce}_0, \ldots, \mathit{ce}_n} \\
+        (G : \Sig') \in \Phi \quad\quad \ok{\Phi}{\Sig'} \\
+        \overrideOk{\Phi}{\TApp{C}{\many{T}}}{\TApp{G}{\tau_0, \ldots, \tau_k}}{\mathit{ce}_i} 
+        \quad\quad
+        \mbox{for}\ \mathit{ce}_i \in \mathit{ce}_0, \ldots, \mathit{ce}_n 
+        }
+        {\ok{\Phi}{\Sig}
+        }
+
+\subsection*{Well-formed class hierarchy:  $\ok{}{\Phi}$}
+\hrulefill\\
+
+\sstext{
+
+A class hierarchy is well-formed if all of the signatures in it are well-formed
+with respect to it.
+
+}{
+
+}
+
+\infrule{\ok{\Phi}{\Sig}\ \mbox{for}\, \Sig\, \in \Phi
+        }
+        {\ok{}{\Phi}
+        }
+
+\subsection*{Program typing:  $\programOk{\Phi}{P}{P'}$}
+\hrulefill\\
+
+%%Definitions:
+%%
+%% \begin{eqnarray*}
+%% \sigof{\mathit{vd}} & = &
+%%   \begin{cases}
+%%     \fieldDecl{x}{\tau} & \mbox{if}\ \mathit{vd} = \dvar{x:\tau}{e}\\
+%%     \fieldDecl{x}{\Dynamic} & \mbox{if}\ \mathit{vd} = \dvar{x:\_}{e}\\
+%%     \methodDecl{f}{\tau_f}{\Arrow[+]{\many{\tau}}{\sigma}} & \mbox{if}\ \mathit{vd} = \dfun{\sigma}{f}{\many{x:\tau}}{s}
+%% \end{cases}\\
+%% \sigof{\mathit{cd}} & = & C\, : \, \dclass{\TApp{C}{\many{T}}}
+%%                                          {\TApp{G}{\tau_0, \ldots, \tau_k}}
+%%                                          {\mathit{ce}_0, \ldots, \mathit{ce}_n} \\
+%% \mbox{where} && 
+%%          \mathit{cd} = \dclass{\TApp{C}{\many{T}}}
+%%                               {\TApp{G}{\tau_0, \ldots, \tau_k}}
+%%                               {\mathit{vd}_0, \ldots, \mathit{vd}_n} \\
+%% \mbox{and} &&
+%%         \mathit{ce}_i = \sigof{vd_i} \quad \mbox{for}\ i \in 0, \ldots, n 
+%%\end{eqnarray*}
+
+\sstext{
+
+Program well-formedness is defined with respect to a class hierarchy $\Phi$.  It
+is not specified how $\Phi$ is produced, but the well-formedness constraints in
+the various judgments should constrain it appropriately.  A program is
+well-formed if each of the top level declarations in the program is well-formed
+in a context in which all of the previous variable declarations have been
+checked and inserted in the context, and if the body of the program is
+well-formed in the final context.  We allow classes to refer to each other in
+any order, since $\Phi$ is pre-specified, but do not model out of order
+definitions of top level variables and functions.  We assume as a syntactic
+property that the class hierarchy $\Phi$ is acyclic.
+
+}{
+
+}
+
+\infrule{  \Gamma_0 = \epsilon \quad\quad
+           \declOk[t]{\Phi, \Gamma_i}{\mathit{td}_i}{\mathit{td}'_i}{\Gamma_{i+1}} \quad 
+           \mbox{for}\ i \in 0,\ldots,n\\
+           \stmtOk{\Phi, \epsilon, \Gamma_{n+1}}{s}{\tau}{s'}{\Gamma_{n+1}'}
+        }
+        { \programOk{\Phi}{\program{\mathit{td}_0, \ldots, \mathit{td}_n}{s}}
+          {\program{\mathit{td}'_0, \ldots, \mathit{td}'_n}{s'}}
+        }