| \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'}} |
| } |
