Core static semantics

doc/definition/strong-dart.tex

Index: doc/definition/strong-dart.tex
diff --git a/doc/definition/strong-dart.tex b/doc/definition/strong-dart.tex
index 3da3ca40c7dced4a19b35d7a9e898b4cb51c728f..520d2bf08cddfaff8798f20b092536e83f49d204 100644
--- a/doc/definition/strong-dart.tex
+++ b/doc/definition/strong-dart.tex
@@ -1,8 +1,9 @@
-\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}}
@@ -13,37 +14,48 @@
 \newcommand{\Type}{\mathbf{Type}}
 
 % expressions
-\newcommand{\eapp}[2]{#1(#2)}
-\newcommand{\eas}[2]{#1\ \mathbf{as}\ #2}
 \newcommand{\eassign}[2]{#1 = #2}
+\newcommand{\eas}[2]{#1\ \mathbf{as}\ #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{\eprim}{\kwop{op}}
+\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{\kwfun}{\kw{fun}}
+\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}
 
+
+\newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2}
+\newcommand{\methodDecl}[2]{\kwfun\ #1 : #2}
+
 % statements
 \newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
 \newcommand{\sreturn}[1]{\kwreturn\ #1}
@@ -52,106 +64,256 @@
 \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}}
+\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}{}}
 
-% relations
+\newcommand{\blockOk}[4]{#1 \vdash #2 \col #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_f\, #4}
+\newcommand{\methodLookup}[4]{#1 \vdash #2.#3\, \leadsto_m\, #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}
+
+
+\newcommand{\sstext}[2]{\ifthenelse{\boolean{show_translation}}{#2}{#1}}
+
+
 
 \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.
+
+There are explicit terms for dynamic calls and loads, and for dynamic type
+checks.
+
+Fields can only be read or 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.  Methods may be
+externally loaded from the object (either to call them, or to pass them as
+closurized functions).
+
 \[
 \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 \\
 %
-\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{\eprim}{\many{e}} \alt \ecall{e}{\many{e}} 
+   \alt \edcall{e}{\many{e}}  \\&&
+   \alt \eload{e}{m} \alt \edload{e}{m} \alt \eload{\ethis}{x} \\&&
+   \alt \eassign{x}{e} \alt \eset{\ethis}{x}{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} \\
+   \dvar{x:\opt{\tau}}{e} \alt \dfun{\tau}{f}{\many{x:\tau}}{s} \\
 %
-\text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{b_1}{b_2} 
+\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}}} \\
 %
 \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}
 \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{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{Type context ($\Delta$)} & ::= &  \epsilon \alt \Delta, T \sub \tau \\
+\text{Class element ($\mathit{ce}$)} & ::= & 
+  \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau} \\
+\text{Class signature ($\mathit{Sig}$)} & ::= &
+  \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{ce}}} \\
+\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.
+
+\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*{Field and Method lookup}
+
+\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} \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}}
+        }
+
+\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}
+        }
+        {\methodLookup{\Phi}{\TApp{C}{\tau_0, \ldots, \tau_n}}{m}{\subst{\tau_0, \ldots, \tau_n}{T_0, \ldots, T_n}{\tau}}
+        }
+
+
+
+\section*{Typing}
+\input{static-semantics}
+
+\section*{Elaboration}
+
+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}