Core static semantics

doc/definition/strong-dart.tex

-\documentclass[fleqn]{article}
-\usepackage{proof, amsmath}
+\documentclass[fleqn, draft]{article}
+\usepackage{proof, amsmath, amssymb, ifthen}
+\input{macros.tex}
 
 % types
-\newcommand{\Arrow}[2]{#1 \rightarrow #2}
+\newcommand{\Arrow}[3][-]{#2 \overset{#1}{\rightarrow} #3}
 \newcommand{\Bool}{\mathbf{bool}}
 \newcommand{\Bottom}{\mathbf{bottom}}
 \newcommand{\Dynamic}{\mathbf{dynamic}}
 \newcommand{\Null}{\mathbf{Null}}
 \newcommand{\Num}{\mathbf{num}}
 \newcommand{\Object}{\mathbf{Object}}
 \newcommand{\TApp}[2]{#1\mathrm{<}#2\mathrm{>}}
 \newcommand{\Type}{\mathbf{Type}}
 
 % expressions
-\newcommand{\eapp}[2]{#1(#2)}
+\newcommand{\eassign}[2]{#1 = #2}
 \newcommand{\eas}[2]{#1\ \mathbf{as}\ #2}
-\newcommand{\eassign}[2]{#1 = #2}
+\newcommand{\echeck}[2]{\kwop{check}(#1, #2)}
+\newcommand{\ecall}[2]{#1(#2)}
+\newcommand{\edcall}[2]{\kwop{dcall}(#1, #2)}
+\newcommand{\edload}[2]{\kwop{dload}(#1, #2)}
 \newcommand{\eff}{\mathrm{ff}}
 \newcommand{\eis}[2]{#1\ \mathbf{is}\ #2}
-\newcommand{\elambda}[2]{(#1) \Rightarrow #2}
+\newcommand{\elambda}[3]{(#1):#2 \Rightarrow #3}
+\newcommand{\eload}[2]{#1.#2}
+\newcommand{\eset}[3]{\eassign{#1.#2}{#3}}
 \newcommand{\enew}[3]{\mathbf{new}\,\TApp{#1}{#2}(#3)}
 \newcommand{\enull}{\mathbf{null}}
-\newcommand{\eprimapp}[2]{\eapp{#1}{#2}}
-\newcommand{\eproj}[2]{#1.#2}
-\newcommand{\esend}[3]{\eapp{\eproj{#1}{#2}}{#3}}
+\newcommand{\eprimapp}[2]{\ecall{#1}{#2}}
+\newcommand{\esend}[3]{\ecall{\eload{#1}{#2}}{#3}}
 \newcommand{\esuper}{\mathbf{super}}
 \newcommand{\ethis}{\mathbf{this}}
+\newcommand{\ethrow}{\mathbf{throw}}
 \newcommand{\ett}{\mathrm{tt}}
 
 % keywords
-\newcommand{\kwclass}{\mathbf{class}}
-\newcommand{\kwextends}{\mathbf{extends}}
-\newcommand{\kwelse}{\mathbf{else}}
-\newcommand{\kwif}{\mathbf{if}}
-\newcommand{\kwin}{\mathbf{in}}
-\newcommand{\kwlet}{\mathbf{let}}
-\newcommand{\kwreturn}{\mathbf{return}}
-\newcommand{\kwthen}{\mathbf{then}}
-\newcommand{\kwvar}{\mathbf{var}}
+\newcommand{\kwclass}{\kw{class}}
+\newcommand{\kwextends}{\kw{extends}}
+\newcommand{\kwelse}{\kw{else}}
+\newcommand{\kwif}{\kw{if}}
+\newcommand{\kwin}{\kw{in}}
+\newcommand{\kwlet}{\kw{let}}
+\newcommand{\kwreturn}{\kw{return}}
+\newcommand{\kwthen}{\kw{then}}
+\newcommand{\kwvar}{\kw{var}}
 
 % declarations
 \newcommand{\dclass}[3]{\kwclass\ #1\ \kwextends\ #2\ \{#3\}}
-\newcommand{\dfun}[4]{#1\ #2(#3)\ #4}
+\newcommand{\dfun}[4]{#2(#3):#1 = #4}
 \newcommand{\dvar}[2]{\kwvar\ #1\ =\ #2}
 
 % statements
 \newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
 \newcommand{\sreturn}[1]{\kwreturn\ #1}
 
 % programs
 \newcommand{\program}[2]{\kwlet\ #1\ \kwin\ #2}
 
 % relational operators
-\newcommand{\sub}{\mathop{<:}}
+\newcommand{\sub}{\mathbin{<:}}
 
 % utilities
 \newcommand{\many}[1]{\overrightarrow{#1}}
 \newcommand{\alt}{\ \mathop{|}\ }
+\newcommand{\opt}[1]{[#1]}
 
 % inference rules
-\newcommand{\axiom}[1]{\infer{#1}{}}
-\newcommand{\infrule}[2]{\infer{#2}{#1}}
-
-% relations
+\newcommand{\infrulem}[3][]{
+  \begin{array}{c@{\ }c}
+    \begin{array}{cccc}
+      #2 \vspace{-2mm} 
+    \end{array} \\
+    \hrulefill & #1 \\
+    \begin{array}{l}
+      #3
+    \end{array}
+  \end{array}
+  }
+
+\newcommand{\axiomm}[2][]{
+  \begin{array}{cc}
+    \hrulefill & #1 \\
+    \begin{array}{c}
+      #2
+    \end{array}
+  \end{array}
+  }
+
+\newcommand{\infrule}[3][]{
+  \[ 
+  \infrulem[#1]{#2}{#3}
+  \]
+  }
+
+\newcommand{\axiom}[2][]{
+  \[ 
+  \axiomm[#1]{#2}
+  \]
+  }
+
+% judgements and relations
+\newboolean{show_translation}
+\setboolean{show_translation}{false}
+\newcommand{\iftrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}{}}
+
+\newcommand{\blockOk}[4]{#1 \vdash #2 \, : \, #3\iftrans{\, \Uparrow\, #4}}
+\newcommand{\declOk}[5][]{#2 \vdash_{#1} #3 \, \Uparrow\, \iftrans{#4\, :\,} #5}
 \newcommand{\extends}[4][:]{#2[#3\ #1\ #4]}
+\newcommand{\fieldLookup}[4]{#1 \vdash #2.#3\, \leadsto\, #4}
+\newcommand{\hastype}[3]{#1 \vdash #2 \, : \, #3}
+\newcommand{\stmtOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow \iftrans{#4\, :\,} #5}
 \newcommand{\subst}[2]{[#1/#2]}
-\newcommand{\subtypeOf}[3]{#1 \vdash\ #2 \sub\ #3}
-
+\newcommand{\subtypeOfOpt}[5][?]{#2 \vdash\ #3 \sub^{#1} #4\, \Uparrow\, #5}
+\newcommand{\subtypeOf}[4][]{#2 \vdash\ #3 \sub^{#1} #4}
+\newcommand{\yieldsOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow\, \iftrans{#4\, :\,} #5}
 \title{Dart strong mode definition}
 
 \begin{document}
 
+\textbf{\large PRELIMINARY DRAFT}
+
 \section*{Syntax}
 
 
+Terms and types.  Note that we allow types to be optional in certain positions
+(currently function arguments and return types, and on variable declarations).
+Implicitly these are either inferred or filled in with dynamic.

[vsm, 2015/07/13 22:36:56]

Is there a benefit to modeling inference here?  It feels like it could be a
'pre-pass'.  

[Leaf, 2015/07/14 22:39:50]

Maybe.  I need to think about whether it can be separated out.

+
+There are explicit terms for dynamic calls and loads, and for dynamic type
+checks.

[Siggi Cherem (dart-lang), 2015/07/10 00:20:58]

I admit, this surprised me a bit. I was expecting that \ecall and \eload would
encode both normal and dynamic cases, and the only distinction would be what the
type system does when it knows the receiver type.

For example,

  var e = dload(o, m);
  dcall(e, arg);

would be equivalent to:

  dynamic o2 = o;
  var e = o2.m;
  dynamic e2 = e;
  e2(arg);


What is the intention behind these 2 explicit constructs?

[Leaf, 2015/07/14 22:39:50]

See my reply to Vijay's comment on dcall in the static semantics for details
about this.  Basically when I add the runtime checks in I want to distinguish
between field loads/method calls which cannot fail, and ones which can.  The
latter turn into dcall/dload.  The proof burden if we decide to prove soundness
is to show that after elaboration, none of the remaining field loads can fail.

+
+Fields can only be set within a method via a reference to this, so no dynamic
+set operation is required (essentially dynamic set becomes a dynamic call to a
+setter).  This just simplifies the presentation a bit.

[vsm, 2015/07/13 22:36:56]

Perhaps worth doing the same with loads for simplicity / consistency?

[Leaf, 2015/07/14 22:39:50]

Done.

[Leaf, 2015/07/14 22:39:50]

Acknowledged.

+
 \[
 \begin{array}{lcl}
 \text{Type identifiers} & ::= &  C, G, T, S, \ldots \\
 %
+\text{Arrow kind ($k$)} & ::= &  +, -\\
+%
 \text{Types $\tau, \sigma$} & ::= &
- T \alt \Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \alt \Bool \\ &&
-   \alt \Arrow{\many{\tau}}{\sigma} \alt \TApp{C}{\many{\tau}} \\
+ T \alt \Dynamic \alt \Object \alt \Null \alt \Type \alt \Num \\ &&
+   \alt \Bool
+   \alt \Arrow[k]{\many{\tau}}{\sigma} \alt \TApp{C}{\many{\tau}} \\
+%
+\text{Optional type ($[\tau]$)} & ::= &  \_ \alt \tau \\
 %
 \text{Term identifiers} & ::= & a, b, x, y, m, n, \ldots \\
 %
 \text{Primops ($\phi$)} & ::= & \mathrm{+}, \mathrm{-} \ldots \mathrm{||} \ldots \\

[Siggi Cherem (dart-lang), 2015/07/10 00:20:58]

not sure we get much from using a $\phi$ for ops :). How about simply $op$ or
{\em op} instead? 

[Leaf, 2015/07/14 22:39:50]

Done.

 %
-\text{lhs ($l$)} & ::= & x \alt \eproj{e}{m} \\
-%
 \text{Expressions $e$} & ::= & 
- x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \alt \esuper
-   \alt \elambda{\many{x:\tau}}{e} \alt \enew{C}{\many{\tau}}{\many{e}} \\&&
-   \alt \eprimapp{\phi}{\many{e}} \alt \eapp{e}{\many{e}} 
-   \alt \eproj{e}{m} \alt \eassign{l}{e} \\&&
-   \alt \eas{e}{\tau} \alt \eis{e}{\tau} \\
+ x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&&
+   \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{e} 
+   \alt \enew{C}{\many{\tau}}{} \\&&
+   \alt \eprimapp{\phi}{\many{e}} \alt \ecall{e}{\many{e}} 

[Siggi Cherem (dart-lang), 2015/07/10 00:20:58]

is \eprimapp only when you know it's a primitive type receiver (e.g.
int.operator+) or also for any user operator (e.g. Vector.operator+)?

[Leaf, 2015/07/14 22:39:50]

The +/- etc syntax is just sugar, and I'm not modeling.  These model the
underlying operations on the primitive types that cannot be expressed in Dart
itself (they are part of the underlying machine model).  So + would operate on
primitive integers, || on primitive bools, etc.

+   \alt \edcall{e}{\many{e}}  \\&&
+   \alt \eload{e}{m} \alt \edload{e}{m} \\&&
+   \alt \eassign{x}{e} \alt \eset{\ethis}{m}{e} \\&&
+   \alt \ethrow \alt \eas{e}{\tau} \alt \eis{e}{\tau} \alt \echeck{e}{\tau}\\
 %
 \text{Declaration ($\mathit{vd}$)} & ::= &
-   \dvar{x}{e} \alt \dvar{x:\tau}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{b} \\
-%
-\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{b_1}{b_2} 
+   \dvar{x:\opt{\tau}}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{s} \\
+%
+\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{s_1}{s_2} 
    \alt \sreturn{e} \alt s;s \\
 %
-\text{Blocks ($b$)} & ::= & \{s;\} \\
-%
 \text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{vd}}} \\

[vsm, 2015/07/13 22:36:56]

Do you think we'll need to model implements as well?  These will add
requirements wrt covariant checks as well:

class MyList implements List<int> { ... }

and might get interesting in the presence of conflicts:

class MyList extends ListBase<dynamic> implements List<int> { ... }

[Leaf, 2015/07/14 22:39:50]

Not sure that it's essential for the first pass.  I don't think it adds anything
deep, but it's true that it adds all sorts of unpleasant corner cases to work
out.  I can think about adding it in future if we want.

 %
 \text{Toplevel decl ($\mathit{td}$)} & ::= & \mathit{vd} \alt \mathit{cd}\\
 %
-\text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{b}
+\text{Program ($P$)} & ::= & \program{\many{\mathit{td}}}{s}

[vsm, 2015/07/13 22:36:56]

s here is effectively the body of main?

[Leaf, 2015/07/14 22:39:50]

yes.

 \end{array}
 \]
 
 
+Type contexts map type variables to their bounds.
+
+Class signatures describe the methods and fields in an object, along with the
+super class of the class.  There are no static methods or fields.
+
+The class hierararchy records the classes with their signatures.
+
+The term context maps term variables to their types.  I also abuse notation and
+allow for the attachment of an optional type to term contexts as follows:
+$\Gamma_\sigma$ refers to a term context within the body of a method whose class
+type is $\sigma$.
 
 \[
 \begin{array}{lcl}
+\text{Type context ($\Delta$)} & ::= &  \epsilon \alt \Delta, X \sub \tau \\

[vsm, 2015/07/13 22:36:56]

Define what X is in your list above?

[Leaf, 2015/07/14 22:39:50]

Should be type variable T.  Fixed.

 \text{Class signature ($\mathit{Sig}$)} & ::= &  \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{x:\tau}} \\
-\text{Type context ($\Delta$)} & ::= &  \epsilon \alt \Delta, X \sub \tau \\
-\text{Class hierarchy ($\Phi$)} & ::= &  \epsilon \alt \Phi, C\ :\ \mathit{Sig}
+\text{Class hierarchy ($\Phi$)} & ::= &  \epsilon \alt \Phi, C\ :\ \mathit{Sig} \\
+\text{Term context ($\Gamma$)} & ::= &  \epsilon \alt \Gamma, x\ :\ \tau
 \end{array}
 \]
 
 
 \section*{Subtyping}
-\[
-\begin{array}{ccc}
-\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Dynamic}} &
-\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Object}} \\\\
-%
-\axiom{\subtypeOf{\Phi, \Delta}{\Bottom}{\tau}} &
-\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\tau}} \\\\
-%
-\infrule{\Delta = \extends[\sub]{\Delta'}{S}{\sigma} & 
+
+\subsection*{Variant Subtyping}
+
+We include a special kind of covariant function space to model certain dart
+idioms.  An arrow type decorated with a positive variance annotation ($+$)
+treats $\Dynamic$ in its argument list covariantly: or equivalently, it treats
+$\Dynamic$ as bottom.  This variant subtyping relation captures this special
+treatment of dynamic.

[vsm, 2015/07/13 22:36:56]

Do you need an explicit $-$?  This is just standard / dynamic as top, right?

[Leaf, 2015/07/14 22:39:50]

I'm defining two different relations: variant subtyping which is indexed by
variance, and regular subtyping.  I could make the - implicit, but then it
becomes ambiguous which one I mean (albeit in a way that doesn't matter).  Bit
of a matter of taste, but I think the third rule in variant subtyping becomes
very confusing if you leave it off.  Also note that the function subtyping rule
in the regular subtyping relation is parametric in the variance, so implicitly
you do have the "-" indexed version of the rule as a hypothesis.

+
+\axiom{\subtypeOf[+]{\Phi, \Delta}{\Dynamic}{\tau}}
+
+\infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau} \quad \sigma \neq \Dynamic}
+        {\subtypeOf[+]{\Phi, \Delta}{\sigma}{\tau}}
+
+\infrule{\subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
+        {\subtypeOf[-]{\Phi, \Delta}{\sigma}{\tau}}
+
+\subsection*{Invariant Subtyping}
+
+Regular subtyping is defined in a fairly standard way, except that generics are
+uniformly covariant, and that function argument types fall into the variant
+subtyping relation defined above.
+
+\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Dynamic}}
+
+\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\Object}} 
+
+\axiom{\subtypeOf{\Phi, \Delta}{\Bottom}{\tau}}
+
+\axiom{\subtypeOf{\Phi, \Delta}{\tau}{\tau}} 
+
+\infrule{(S\, :\, \sigma) \in \Delta \quad
          \subtypeOf{\Phi, \Delta}{\sigma}{\tau}}
-        {\subtypeOf{\Phi, \Delta}{S}{\tau}} \\\\
-%
-\infrule{\subtypeOf{\Phi, \Delta}{\sigma_i}{\tau_i} & i \in 0, \ldots, n &
-         \subtypeOf{\Phi, \Delta}{\tau_r}{\sigma_r}}
+        {\subtypeOf{\Phi, \Delta}{S}{\tau}} 
+
+\infrule{\subtypeOf[k_1]{\Phi, \Delta}{\sigma_i}{\tau_i} \quad i \in 0, \ldots, n \quad\quad
+         \subtypeOf{\Phi, \Delta}{\tau_r}{\sigma_r} \\
+         \quad (k_0 = \mbox{-}) \lor (k_1 = \mbox{+})
+        } 
         {\subtypeOf{\Phi, \Delta}
-                   {\Arrow{\tau_0, \ldots, \tau_n}{\tau_r}}
-                   {\Arrow{\sigma_0, \ldots, \sigma_n}{\sigma_r}}} \\\\
-%
+                   {\Arrow[k_0]{\tau_0, \ldots, \tau_n}{\tau_r}}
+                   {\Arrow[k_1]{\sigma_0, \ldots, \sigma_n}{\sigma_r}}} 
+
 \infrule{\subtypeOf{\Phi, \Delta}{\tau_i}{\sigma_i} & i \in 0, \ldots, n}
         {\subtypeOf{\Phi, \Delta}
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
-          {\TApp{C}{\sigma_0, \ldots, \sigma_n}}}\\\\
-%
-\infrule{\Phi = \extends{\Phi'}{C}{\dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}} \\
+          {\TApp{C}{\sigma_0, \ldots, \sigma_n}}}
+
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}) \in \Phi \\
          \subtypeOf{\Phi, \Delta}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}}{\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
         {\subtypeOf{\Phi, \Delta}
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
-\end{array}
-\]
+
+\section*{Typing}
+\input{static-semantics}
+
+\section*{Translation}
+
+These are the same rules, extended with a translated term which corresponds to
+the original term with the additional dynamic type checks inserted to reify the
+static unsoundness as runtime type errors.
+
+\setboolean{show_translation}{true}
+%\input{static-semantics}
+
 
 \end{document}