Static semantics v0.1

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 520d2bf08cddfaff8798f20b092536e83f49d204..046f797dbe2be953ce9a3c69569eb8480b8300ac 100644
--- a/doc/definition/strong-dart.tex
+++ b/doc/definition/strong-dart.tex
@@ -12,6 +12,8 @@
 \newcommand{\Object}{\mathbf{Object}}
 \newcommand{\TApp}[2]{#1\mathrm{<}#2\mathrm{>}}
 \newcommand{\Type}{\mathbf{Type}}
+\newcommand{\Weak}[1]{\mathbf{\{#1\}}}
+\newcommand{\Sig}{\mathit{Sig}}
 
 % expressions
 \newcommand{\eassign}[2]{#1 = #2}
@@ -54,7 +56,7 @@
 
 
 \newcommand{\fieldDecl}[2]{\kwvar\ #1 : #2}
-\newcommand{\methodDecl}[2]{\kwfun\ #1 : #2}
+\newcommand{\methodDecl}[3]{\kwfun\ #1 : \iftrans{#2 \triangleleft} #3}
 
 % statements
 \newcommand{\sifthenelse}[3]{\kwif\ (#1)\ \kwthen\ #2\ \kwelse\ #3}
@@ -109,20 +111,28 @@
 \newboolean{show_translation}
 \setboolean{show_translation}{false}
 \newcommand{\iftrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}{}}
+\newcommand{\ifnottrans}[1]{\ifthenelse{\boolean{show_translation}}{#1}}
 
 \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{\methodLookup}[5]{#1 \vdash #2.#3\, \leadsto_m\, \iftrans{#4 \triangleleft} #5}
+\newcommand{\fieldAbsent}[3]{#1 \vdash #3 \notin #2}
+\newcommand{\methodAbsent}[3]{#1 \vdash #3 \notin #2}
 \newcommand{\hastype}[3]{#1 \vdash #2 \, : \, #3}
 \newcommand{\stmtOk}[5]{#1 \vdash #2 \, : \, #3\, \Uparrow \iftrans{#4\, :\,} #5}
 \newcommand{\subst}[2]{[#1/#2]}
 \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{\programOk}[3]{#1 \vdash #2\iftrans{\, \Uparrow\, #3}}
+\newcommand{\ok}[2]{#1 \vdash #2\, \mbox{\textbf{ok}}}
+\newcommand{\overrideOk}[4]{#1 \vdash #2\,\kwextends\, #3 \Leftarrow\, #4}
 
-
+\newcommand{\down}[1]{\ensuremath{\downharpoonleft\!\!#1\!\!\downharpoonright}}
+\newcommand{\up}[1]{\ensuremath{\upharpoonleft\!\!#1\!\!\upharpoonright}}
+\newcommand{\sigof}[1]{\mathit{sigof}(#1)}
 \newcommand{\sstext}[2]{\ifthenelse{\boolean{show_translation}}{#2}{#1}}
 
 
@@ -168,7 +178,7 @@ closurized functions).
 %
 \text{Expressions $e$} & ::= & 
  x \alt i \alt \ett \alt \eff \alt \enull \alt \ethis \\&&
-   \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{e} 
+   \alt \elambda{\many{x:\opt{\tau}}}{\opt{\sigma}}{s} 
    \alt \enew{C}{\many{\tau}}{} \\&&
    \alt \eprimapp{\eprim}{\many{e}} \alt \ecall{e}{\many{e}} 
    \alt \edcall{e}{\many{e}}  \\&&
@@ -182,7 +192,7 @@ closurized functions).
 \text{Statements ($s$)} & ::= & \mathit{vd} \alt e \alt \sifthenelse{e}{s_1}{s_2} 
    \alt \sreturn{e} \alt s;s \\
 %
-\text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{S}}}{\many{\mathit{vd}}} \\
+\text{Class decl ($\mathit{cd}$)} & ::= & \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{vd}}} \\
 %
 \text{Toplevel decl ($\mathit{td}$)} & ::= & \mathit{vd} \alt \mathit{cd}\\
 %
@@ -207,10 +217,10 @@ type is $\sigma$.
 \begin{array}{lcl}
 \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} \\
+  \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
+\text{Class signature ($\Sig$)} & ::= &
+  \dclass{\TApp{C}{\many{T}}}{\TApp{G}{\many{\tau}}}{\many{\mathit{ce}}} \\
+\text{Class hierarchy ($\Phi$)} & ::= &  \epsilon \alt \Phi, C\ :\ \Sig \\
 \text{Term context ($\Gamma$)} & ::= &  \epsilon \alt \Gamma, x\ :\ \tau
 \end{array}
 \]
@@ -271,48 +281,46 @@ subtyping relation defined above.
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\TApp{G}{\sigma_0, \ldots, \sigma_m}}}
 
-\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}
 
+\pagebreak
 \section*{Elaboration}
+\setboolean{show_translation}{true}
 
-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.
+Elaboration is a type driven translation which maps a source Dart term to a
+translated term which corresponds to the original term with additional dynamic
+type checks inserted to reify the static unsoundness as runtime type errors.
+For the translation, we extend the source language slightly as follows.
+\[
+\begin{array}{lcl}
+\text{Expressions $e$} & ::= & \ldots 
+   \alt \edcall{e}{\many{e}} \alt \edload{e}{m} \alt \echeck{e}{\tau}\\
+\end{array}
+\]
+
+The expression language is extended with an explicitly checked dynamic call
+operation, and explicitly checked dynamic method load operation, and a runtime

[vsm, 2015/07/28 15:44:32]

"dynamic method load operation" -> "dynamic load operation"?

[Leaf, 2015/07/28 20:34:29]

The syntax is a little deceptive - there are really two load operations in this
core language: loading a method (e.m) and loading a field (this.x).  The syntax
is ambiguous in that "this" is an expression, so you can (for example) say
this.m to load a method named "m" from the expression "this", or to load a field
name "m" from "this".  Think of their being two different AST nodes that happen
to pretty-print the same.  I informally distinguish them by using the
metavariables m and x for methods and fields.  Perhaps I should make this less
ambiguous, but it's a little convenient.

+type test.  Note that while a user level cast throws an exception on failure,
+the runtime type test term introduced here produces a hard type error which
+cannot be caught programmatically.
+
+We also extend typing contexts slightly by adding an internal type to method signatures.
+\[
+\begin{array}{lcl}
+\text{Class element ($\mathit{ce}$)} & ::= & 
+  \fieldDecl{x}{\tau} \alt \methodDecl{f}{\tau}{\sigma} \\
+\end{array}
+\]
+A method signature of the form $\methodDecl{f}{\tau}{\sigma}$ describes a method
+whose public interface is described by $\sigma$, but which has an internal type
+$\tau$ which is a subtype of $\sigma$, but which is properly covariant in any
+type parameters.  The elaboration introduces runtime type checks to mediate
+between the two types.  This is discussed further in the translation of classes
+below.
 
-\setboolean{show_translation}{true}
 \input{static-semantics}