| \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{otherwise} | |
| \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$. | |
| Alternatively if $e$ appears as in $\dvar{x:\_}{e}$, then the context does not | |
| provide a type constraint on $e$. This ``contextual'' type information is | |
| both a constraint on the term, and may also provide a source of information | |
| for type inference in $e$. The optional type $\opt{\tau}$ in the typing | |
| relation corresponds to this contextual type information. Viewing the | |
| relation algorithmically, this should be viewed as an input to the algorithm, | |
| along with the term. The process of checking a term allows us to synthesize a | |
| precise type for the term $e$ which may be more precise than the type required | |
| by the context. The type $\tau'$ in the relation represents this more | |
| precise, synthesized type. This type should be thought of as an output of the | |
| algorithm. It should always be the case that the synthesized (output) type is | |
| a subtype of the checked (input) type if the latter is present. The | |
| checking/synthesis pattern allows for the propagation of type information both | |
| downwards and upwards. | |
| It is often the case that downwards propagation is not useful. Consequently, | |
| to simplify the presentation the rules which do not use the checking type | |
| require that it be empty ($\_$). This does not mean that such terms cannot be | |
| checked when contextual type information is supplied: the first typing rule | |
| allows contextual type information to be dropped so that such rules apply in | |
| the case that we have contextual type information, subject to the contextual | |
| type being a supertype of the synthesized type: | |
| }{ | |
| For subsumption, the elaboration of the underlying term carries through. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad | |
| \subtypeOf{\Phi, \Delta}{\sigma}{\tau} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\sigma}} | |
| \sstext{ | |
| The implicit downcast rule also allows this when the contextual type is a | |
| subtype of the synthesized type, corresponding to an implicit downcast. | |
| }{ | |
| In an implicit downcast, the elaboration adds a check so that an error | |
| will be thrown if the types do not match at runtime. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad | |
| \subtypeOf{\Phi, \Delta}{\tau}{\sigma} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{\echeck{e'}{\tau}}{\tau}} | |
| \sstext{Variables are typed according to their declarations:}{} | |
| \axiom{\yieldsOk{\Phi, \Delta, \extends{\Gamma}{x}{\tau}}{x}{\_}{x}{\tau}} | |
| \sstext{Numbers, booleans, and null all have a fixed synthesized type.}{} | |
| \axiom{\yieldsOk{\Phi, \Delta, \Gamma}{i}{\_}{i}{\Num}} | |
| \axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\eff}{\_}{\eff}{\Bool}} | |
| \axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\ett}{\_}{\ett}{\Bool}} | |
| \axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\enull}{\_}{\enull}{\Bottom}} | |
| \sstext{A $\ethis$ expression is well-typed if we are inside of a method, and $\sigma$ | |
| is the type of the enclosing class.}{} | |
| \infrule{\Gamma = \Gamma'_{\sigma} | |
| } | |
| { | |
| \yieldsOk{\Phi, \Delta, \Gamma}{\ethis}{\_}{\ethis}{\sigma} | |
| } | |
| \sstext{A fully annotated function is well-typed if its body is well-typed at its | |
| declared return type, under the assumption that the variables have their | |
| 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 | |
| \stmtOk{\Phi, \Delta, \Gamma'}{s}{\sigma}{s'}{\Gamma'} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\elambda{\many{x:\tau}}{\sigma}{s}} | |
| {\_} | |
| {\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}}{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}}{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}}{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}}{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}{s}} | |
| {\opt{\tau_c}} | |
| {e_f} | |
| {\tau_f} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\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}{s}} | |
| {\tau_c} | |
| {e_f} | |
| {\tau_f} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\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 | |
| \infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}) \in \Phi \\ | |
| \mbox{len}(\many{\tau}) = n+1} | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\enew{C}{\many{\tau}}{}} | |
| {\_} | |
| {\enew{C}{\many{\tau}}{}} | |
| {\TApp{C}{\many{\tau}}} | |
| } | |
| \sstext{Members of the set of primitive operations (left unspecified) can only be | |
| applied. Applications of primitives are well-typed if the arguments are | |
| well-typed at the types given by the signature of the primitive.}{} | |
| \infrule{\eprim\, :\, \Arrow[]{\many{\tau}}{\sigma} \quad\quad | |
| \yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\tau'} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\eprimapp{\eprim}{\many{e}}} | |
| {\_} | |
| {\eprimapp{\eprim}{\many{e'}}} | |
| {\sigma} | |
| } | |
| \sstext{Function applications are well-typed if the applicand is well-typed and has | |
| function type, and the arguments are well-typed.} | |
| { | |
| Function application of an expression of function type elaborates to either a | |
| call or a dynamic (checked) call, depending on the variance of the applicand. | |
| If the applicand is a covariant (fuzzy) type, then a dynamic call is generated. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma} | |
| {e} | |
| {\_} | |
| {e'} | |
| {\Arrow[k]{\many{\tau_a}}{\tau_r}} \\ | |
| \yieldsOk{\Phi, \Delta, \Gamma} | |
| {e_a} | |
| {\tau_a} | |
| {e_a'} | |
| {\tau_a'} \quad \mbox{for}\ e_a, \tau_a \in \many{e_a}, \many{\tau_a} | |
| \iftrans{\\ e_c = \begin{cases} | |
| \ecall{e'}{\many{e_a'}} & \text{if $k = -$}\\ | |
| \edcall{e'}{\many{e_a'}} & \text{if $k = +$} | |
| \end{cases}} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\ecall{e}{\many{e_a}}} | |
| {\_} | |
| {e_c} | |
| {\tau_r} | |
| } | |
| \sstext{Application of an expression of type $\Dynamic$ is well-typed if the arguments | |
| are well-typed at any type. } | |
| { | |
| Application of an expression of type $\Dynamic$ elaborates to a dynamic call. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma} | |
| {e} | |
| {\_} | |
| {e'} | |
| {\Dynamic} \\ | |
| \yieldsOk{\Phi, \Delta, \Gamma} | |
| {e_a} | |
| {\_} | |
| {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}{\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.} | |
| { | |
| A method load from a term of type $\Dynamic$ elaborates to a dynamic (checked) | |
| load. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma} | |
| {e} | |
| {\Dynamic} | |
| {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} | |
| } | |
| \sstext{An assignment expression is well-typed so long as the term is well-typed at a | |
| type which is compatible with the type of the variable being assigned.}{} | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma} | |
| {e} | |
| {\opt{\tau}} | |
| {e'} | |
| {\sigma} \quad\quad | |
| \yieldsOk{\Phi, \Delta, \Gamma} | |
| {x} | |
| {\sigma} | |
| {x} | |
| {\sigma'} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\eassign{x}{e}} | |
| {\opt{\tau}} | |
| {\eassign{x}{e'}} | |
| {\sigma} | |
| } | |
| \sstext{A field assignment is well-typed if the term being assigned is well-typed, the | |
| field name is present in the type of $\ethis$, and the declared type of the | |
| field is compatible with the type of the expression being assigned.}{} | |
| \infrule{\Gamma = \Gamma_\tau \quad\quad | |
| \yieldsOk{\Phi, \Delta, \Gamma} | |
| {e} | |
| {\opt{\tau}} | |
| {e'} | |
| {\sigma} \\ | |
| \fieldLookup{\Phi}{\tau}{x}{\sigma'} \quad\quad | |
| \subtypeOf{\Phi, \Delta}{\sigma}{\sigma'} | |
| } | |
| {\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\eset{\ethis}{x}{e}} | |
| {\_} | |
| {\eset{\ethis}{x}{e}} | |
| {\sigma} | |
| } | |
| \sstext{A throw expression is well-typed at any type.}{} | |
| \axiom{\yieldsOk{\Phi, \Delta, \Gamma} | |
| {\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.}{} | |
| \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 | |
| context binds the variable at the declared type. | |
| } | |
| { | |
| Elaboration of declarations elaborates the underlying expressions. | |
| } | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\tau'} | |
| } | |
| {\declOk[d]{\Phi, \Delta, \Gamma} | |
| {\dvar{x:\tau}{e}} | |
| {\dvar{x:\tau'}{e'}} | |
| {\extends{\Gamma}{x}{\tau}} | |
| } | |
| \sstext{A simple variable declaration without a declared type is well-typed if the | |
| initializer for the declaration is well-typed at any type. The output context | |
| binds the variable at the synthesized type (a simple form of type inference).}{} | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\tau'} | |
| } | |
| {\declOk[d]{\Phi, \Delta, \Gamma} | |
| {\dvar{x:\_}{e}} | |
| {\dvar{x:\tau'}{e'}} | |
| {\extends{\Gamma}{x}{\tau'}} | |
| } | |
| \sstext{A function declaration is well-typed if the body of the function is well-typed | |
| with the given return type, under the assumption that the function and its | |
| parameters have their declared types. The function is assumed to have a | |
| contravariant (precise) function type. The output context binds the function | |
| variable only.}{} | |
| \infrule{\tau_f = \Arrow[-]{\many{\tau_a}}{\tau_r} \quad\quad | |
| \Gamma' = \extends{\Gamma}{f}{\tau_f} \quad\quad | |
| \Gamma'' = \extends{\Gamma'}{\many{x}}{\many{\tau_a}} \\ | |
| \stmtOk{\Phi, \Delta, \Gamma''}{s}{\tau_r}{s'}{\Gamma_0} | |
| } | |
| {\declOk[d]{\Phi, \Delta, \Gamma} | |
| {\dfun{\tau_r}{f}{\many{x:\tau_a}}{s}} | |
| {\dfun{\tau_r}{f}{\many{x:\tau_a}}{s'}} | |
| {\Gamma'} | |
| } | |
| \subsection*{Statement typing: $\stmtOk{\Phi, \Delta, \Gamma}{\mathit{s}}{\tau}{\mathit{s'}}{\Gamma'}$} | |
| \hrulefill\\ | |
| \sstext{The statement typing relation checks the well-formedness of statements and | |
| produces an output context which reflects any additional variable bindings | |
| introduced into scope by the statements. | |
| }{ | |
| Statement elaboration elaborates the underlying expressions. | |
| } | |
| \sstext{A variable declaration statement is well-typed if the variable declaration is | |
| well-typed per the previous relation, with the corresponding output context. | |
| }{} | |
| \infrule{\declOk[d]{\Phi, \Delta, \Gamma} | |
| {\mathit{vd}} | |
| {\mathit{vd'}} | |
| {\Gamma'} | |
| } | |
| {\stmtOk{\Phi, \Delta, \Gamma} | |
| {\mathit{vd}} | |
| {\tau} | |
| {\mathit{vd'}} | |
| {\Gamma'} | |
| } | |
| \sstext{An expression statement is well-typed if the expression is well-typed at any | |
| type per the expression typing relation.}{} | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\tau} | |
| } | |
| {\stmtOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\Gamma} | |
| } | |
| \sstext{A conditional statement is well-typed if the condition is well-typed as a | |
| boolean, and the statements making up the two arms are well-typed. The output | |
| context is unchanged.}{} | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\Bool}{e'}{\sigma} \\ | |
| \stmtOk{\Phi, \Delta, \Gamma}{s_1}{\tau_r}{s_1'}{\Gamma_1} \quad\quad | |
| \stmtOk{\Phi, \Delta, \Gamma}{s_2}{\tau_r}{s_2'}{\Gamma_2} | |
| } | |
| {\stmtOk{\Phi, \Delta, \Gamma} | |
| {\sifthenelse{e}{s_1}{s_2}} | |
| {\tau_r} | |
| {\sifthenelse{e'}{s_1'}{s_2'}} | |
| {\Gamma} | |
| } | |
| \sstext{A return statement is well-typed if the expression being returned is well-typed | |
| at the given return type. }{} | |
| \infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau_r}{e'}{\tau} | |
| } | |
| {\stmtOk{\Phi, \Delta, \Gamma}{\sreturn{e}}{\tau_r}{\sreturn{e'}}{\Gamma} | |
| } | |
| \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 soundly covariant in the type | |
| parameters (that is, all contravariant type parameters are replaced with | |
| $\Dynamic$, and hence all remaining type parameters occur in properly covariant | |
| positions). 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_i = | |
| \begin{cases} | |
| \Gamma_{\TApp{C}{\many{T}}} & \mbox{if $\mathit{vd}_i$ is a method} \\ | |
| \Gamma & \mbox{if $\mathit{vd}_i$ is a field} \\ | |
| \end{cases}\\ | |
| \declOk[ce]{\Phi, \Delta, \Gamma_i}{\mathit{vd}_i : \mathit{ce}_i}{\mathit{vd}'_i}{\Gamma'_i} \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 require two coherence conditions. As before, we | |
| 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 | |
| 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 overridden method must expect to be used at type | |
| $\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'}} | |
| } |