dart / sdk.git / refs/tags/2.2.0-dev.2.0 / . / pkg / dev_compiler / 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{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'}} | |

} |