Static semantics v0.1

doc/definition/strong-dart.tex

 \documentclass[fleqn, draft]{article}
 \usepackage{proof, amsmath, amssymb, ifthen}
 \input{macros.tex}
 
 % types
 \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}}
+\newcommand{\Weak}[1]{\mathbf{\{#1\}}}
+\newcommand{\Sig}{\mathit{Sig}}
 
 % expressions
 \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}
@@ skipping 22 matching lines @@
 \newcommand{\kwthen}{\kw{then}}
 \newcommand{\kwvar}{\kw{var}}
 
 % declarations
 \newcommand{\dclass}[3]{\kwclass\ #1\ \kwextends\ #2\ \{#3\}}
 \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}
+\newcommand{\methodDecl}[3]{\kwfun\ #1 : \iftrans{#2 \triangleleft} #3}
 
 % 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}{\mathbin{<:}}
@@ skipping 34 matching lines @@
 \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{\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}}
 
 
 
 \title{Dart strong mode definition}
 
 \begin{document}
 
 \textbf{\large PRELIMINARY DRAFT}
 
@@ skipping 25 matching lines @@
    \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{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}}  \\&&
    \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:\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{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}\\
 %
 \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{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}
 \]
 
 
 \section*{Subtyping}
 
 \subsection*{Variant Subtyping}
 
 We include a special kind of covariant function space to model certain dart
@@ skipping 40 matching lines @@
         {\subtypeOf{\Phi, \Delta}
           {\TApp{C}{\tau_0, \ldots, \tau_n}}
           {\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}}}
 
-\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}
+\]
 
-\setboolean{show_translation}{true}
+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.
+
 \input{static-semantics}
 
 
 \end{document}