\documentclass[wider]{kwart}

\usepackage{amssymb}
\usepackage{../notation}
\usepackage{../assign}
\usepackage{../proof}

\deftok{|}{\mathrel|}
\deftok{#}{\mathbin\#}
\deftok{=>}{\Rightarrow}
\deftok{|->}{\mathrel\mapsto}
\deftok{__}{\_}
\deftok{~}{\;}
\deftok{@}{\>}
\deftok{->}{\mathrel\rightarrow}
\deftok{...}{\ldots}
\deftok{.}{\mathpunct.}
\deftok{::}{::}
\deftok{*}{\mathbin\times}
\deftok{<<}{\mathrel{<\!\!<}}
\deftok{[]}{\Box}
\deftok{|>}{\mathrel\triangleright}
\deftok{|-}{\vdash}
\deftok{==>}{\Rightarrow}
\deftok{<==}{\Leftarrow}
\deftok{<=}{\sqsubseteq}
\defvariable{G}{\Gamma}
\defvariable{t}{\tau}
\defvariable{a}{\alpha}
\defvariable{b}{\beta}
\easynotation
\def\skp{\\[1ex]}

\begin{document}
  \title{Assignment 6: Coercion Elaboration}
  \author{15-312: Foundations of Programming Languages \\
    Kevin Watkins $\langle$kw@cmu.edu$\rangle$}
  \date{\begin{tabular}{l} Out: Tuesday, March 29, 2005 \\
    Due: Thursday, April 7, 2005 (11:59 p.m.) \\
    \end{tabular}\\[1ex]
    100 points total
    }
  \maketitle

  \section{Introduction}

  In this assignment you will modify an implementation of PolyMinML by
  adding a coercion-based notion of subtyping.  The language
  includes most of the constructs we've seen in the course, including
  universal, existential, and recursive types and references for
  mutable state.

\kwd{int}\kwd{float}\kwd{itof}
  The idea of \emph{coercion elaboration} is to take a program that typechecks
  with applications of the subsumption rule, and \emph{elaborate} it by
  inserting code at each
  point where subsumption is used, to actually perform the coercions.
  For example, the subsumption rule might allow an >int expression to
  be used where a >float was expected.  In that case the coercion
  elaboration would insert the primitive operation >itof to explicitly
  convert the >int to a >float.

  Once elaboration has been done to get rid of instances of the
  subsumption rule, the program can be fed to the operational semantics
  and evaluated.  If we tried to run a program without elaborating it
  first, it could get stuck.  For example, we might imagine that
  integers and floating-point numbers are stored in separate registers
  in the machine, according to its calling convention.  In that case
  the subsumption rule (which just says ``an >int is a >float'') needs
  to be replaced with actual work to move the value from one kind of
  register to the other.

  The static semantics of our language has also been refined to get
  rid of the typing annotations that were formerly needed on many of
  the expression constructs to ensure unique typing.  Instead, we
  use the \emph{bidirectional} system discussed in recitation to
  replace all these different kinds of typing annotations with a single
  construct.

  The text of the assignment is rather long; this is mostly because
  the topics here were only treated in recitation, and I also want to
  give you a ``reference card'' for almost all of the features we
  looked at in the static semantics of PolyMinML.

\kwd{type}
\kwd{bool}\kwd{ref}\kwd{cont}\kwd{let}
\kwd{case}\kwd{of}\kwd{in}\kwd{fun}\kwd{true}\kwd{false}
\kwd{if}\kwd{then}\kwd{else}\kwd{mod}\kwd{sqrt}\kwd{pack}\kwd{unpack}
\kwd{letcc}\kwd{throw}\kwd{to}\kwd{roll}\kwd{unroll}\kwd{try}\kwd{ow}\kwd{fail}
\kwd{as}\kwd{abort}
\deftok{!}{\mathord{!}}
\deftok{+.}{\mathbin{+.}}
\deftok{*.}{\mathbin{\times.}}
  \section{Syntax}
  The syntax of the variation of PolyMinML we'll be using is as follows:
  >>\begin{array}{rcl}
    t & ::= & a | int | bool | float | t1 -> t2 | 1 | t1 * \cdots * tn
            | 0 | t1 + \cdots + tn \\
      &     & \qquad | t@ref | t@cont
            | \forall a. t | \exists a. t | \mu a. t \\
    e & ::= & x | fun~f(x). e | e1@e2 \\
    & & \qquad | () | (e1,...,en) | e.i \\
    & & \qquad | in_{i}@e | (case~e~of~in_{1}@x1 => e1 | ... | in_{n}@xn => en) | abort@e \\
    & & \qquad | true | false | if~e~then~e1~else~e2 | e1=e2 | e1<e2 \\
    & & \qquad | n | e1+e2 | e1-e2 | e1*e2 | \tilde{}e | e1@mod@e2 \\
    & & \qquad | f | e1+.e2 | e1*.e2 | sqrt@e | itof@e \\
    & & \qquad | ref@e | !e | e1:=e2 | (e1; e2) \\
    & & \qquad | letcc~x~in~e | throw~e1~to~e2 \\
    & & \qquad | try~e1~ow~e2 | fail \\
    & & \qquad | \Lambda a. e | e[t] \\
    & & \qquad | pack(t,e)
               | unpack(a,x)=e1~in~e2 \\
    & & \qquad | roll@e | unroll@e \\
    & & \qquad | let~x=e1~in~e2 | let~type~a=t~in~e | (e : t) \\
    G & ::= & \cdot | G, (a@type) | G, (x:t) \\
  \end{array}
  (As you can see, we've put together pretty much all the concepts
  we've studied so far.  Once you've thrown coercion-based subtyping
  into the mix as part of doing this assignment, you will have implemented
  a language that's syntactically simple, but with more subtle features than
  any currently marketed language, and nearly every
  experimental language.)

  There is new syntax here, modeled on SML's, concerning references
  and imperative programming:
  >>\begin{array}{ll}
    ref@e       & \hbox{Make a new reference} \\
    !e          & \hbox{Get the value stored in $e$} \\
    e1:=e2      & \hbox{Store the value of $e2$ in $e1$} \\
    (e1;e2)     & \hbox{Evaluate $e1$, then $e2$} \\
  \end{array}
  
  We've also modified the syntax for product types and
  sum types to take any number >{n \geq 2} of arguments.
  Although syntax for unit types (>1) and void types (>0) is given
  above, in the implementation these are reduced by the parser to special cases
  (with >{n=0}) of the general product and sum types.  Similarly the unit
  expression >{()} is turned by the parser into just a >0-ary tuple, and the
  abort expression >{abort@e} is turned by the parser into a >case
  with no arms.  (You should think about why an >abort and a >case with
  no arms are the same thing.)  Thus, in what follows, I won't mention the
  unit and void types again, since the SML typechecker
  never has to deal with them explicitly.

\def\rep#1{\ulcorner#1\urcorner}
  The corresponding SML representations of these things now take lists:
  \begin{quote}
    \hfil\begin{tabular}{l}
      \verb/datatype exp =/ \\
      \verb/    .../ \\
      \verb/  | Tuple of exp list/ \\
      \verb/  | Proj of exp * int/ \\
      \verb/  | Inj of int * exp/ \\
      \verb/  | Case of exp * (bind * exp) list/ \\
    \end{tabular}
  \end{quote}
  So for instance
  >>\begin{array}{rcl}
    (e1,e2,e3) & \hbox{becomes}
    & \texttt{Tuple[}\rep{e1}\texttt{,}\rep{e2}\texttt{,}\rep{e3}\texttt{]} \\
    e.5 & \hbox{becomes}
    & \texttt{Proj(}\rep{e}\texttt{, 5)} \\
    in_{3}@e & \hbox{becomes}
    & \texttt{Inj(3, }\rep{e}\texttt{)} \\
    case~e~of~in_{1}@x1=>e1
    & \hbox{becomes}
    & \texttt{Case(}\rep{e}\texttt{, [(}\rep{x1}\texttt{,}\rep{e1}
      \texttt{),}\qquad \\
    | in_{2}@x2=>e2 &
    & \hfil\texttt{(}\rep{x2}\texttt{,}\rep{e2}\texttt{)])}\hfilneg \\
  \end{array}

  There is now a type >float and operations on it:
  >>\begin{array}{ll}
    f           & \hbox{A floating-point constant} \\
    e1+.e2      & \hbox{Floating-point addition} \\
    e1*.e2      & \hbox{Floating-point multiplication} \\
    sqrt@e      & \hbox{Square root} \\
  \end{array}
  An additional operation >{itof@e} is used internally to do the work
  of coercing {>int}s to {>float}s.  There's generally no reason to
  use it in the external language, because in the external language,
  an >int can be used whenever a >float is required.

  A new construct >{let~type~a=t~in~e} has been added, which lets
  you give a type a shorter name.  This should help you if you choose
  to do the following extra credit problem.
  The operational semantics is just
  >>{(let~type~a=t~in~e) |-> \{t/a\}e}
  and the static semantics is given below.

  \begin{question}{2.1}\extra
    Code up a few of your System F examples, or an abstract type
    (like queues) in PolyMinML.  Put them in a file \texttt{polytest.mml}
    and hand it in.
  \end{question}

  Finally, note that all of the type subscripts have been removed from
  the expression syntax.  The only remaining places types can occur
  within an expression are when applying a type function, {>pack}ing an
  existential (abstract) type, in the >{let~type} construct,
  and in a new expression form >{(e : t)} that explicitly \emph{ascribes}
  the type >t to the expression >e.

  The ASCII syntax for all these things should be pretty clear; consult
  the comments at the beginning of the parser in \texttt{parse.sml} for
  details.  As usual, a construct like >fun,
  >case, >if, >let, >letcc, >throw, >try, >pack, or >unpack extends as
  far to the right as possible \emph{except} that they all end at the
  colon in >{e : t} (which helps keep the parentheses for type
  ascriptions to a minimum).  So for example we can say
  \begin{quote}
    \hfil\verb/fun f(x) is x+1 : int -> int/
  \end{quote}
  You can look at the example PolyMinML files
  to see how this works.

  The universal, existential, and recursive types get ASCII syntax as
  follows:
  \begin{quote}
  \hfil\begin{tabular}{ll}
    \verb/!a a -> a/ & Read as >{\forall a. a -> a} \\
    \verb/?a a -> a/ & Read as >{\exists a. a -> a} \\
    \verb/#a a -> a/ & Read as >{\mu a. a -> a} \\
  \end{tabular}
  \end{quote}

  One other minor change in the ASCII syntax is that the expressions
  you type into the system (or put in a \texttt{.mml} file) have to
  be terminated with \texttt{;;} because a single \texttt{;} is now
  for sequencing imperative computations.

  \section{Bidirectional Checking}

  Now we'll consider how to typecheck in bidirectional style.
  The basic idea is to separate the single judgment >{G |- e : t} we
  had before into two judgments, >{G |- e <== t} for \emph{checking}
  an expression >e against a type >t, and >{G |- e ==> t} for
  \emph{synthesizing} (computing) a type >t by looking at the
  expression >e.  Thus we take into account that type information
  might flow \emph{downward} from an expression into its subexpressions,
  or \emph{upward} from the subexpressions to the whole expression.
  There is also, as usual, a judgment >{G |- t : type} declaring that
  the type >t is well-formed in context >G.  This doesn't need to be
  separated into two judgments, because we always know that we're
  checking >t as a \emph{type}.  There is also a judgment
  >{G |- t1 <= t2} for checking that one type is a subtype of another;
  here both >t1 and >t2 are inputs.

  In the notation of \emph{modes} we saw in recitation, we then have
  the following modes for the four basic type checking judgments:
  >>\begin{array}{lll}
    G^+ |- t^+ @type  & \texttt{tok g t}& \hbox{Check that $t$ is a type in $G$} \\
    G^+ |- e^+ <== t^+ & \texttt{ck g e t}& \hbox{Check $e$ against type $t$}     \\
    G^+ |- e^+ ==> t^- & \texttt{syn g e} & \hbox{Infer a type $t$ for $e$}       \\
    G^+ |- t1^+ <= t2^+ & \texttt{sub g t1 t2} & \hbox{Check $t1$ a subtype of $t2$}  \\
  \end{array}
  (Remember that a superscript >{{}^+} on a part of the judgment
  signifies that it is supplied as \emph{input} when we read the
  judgment as an algorithm, while the superscript >{{}^-} means that
  the part is generated as \emph{output}.)
  In the following rules, you should check for yourself that the
  modes are correct.  The names of the functions that implement the
  algorithm in the SML code are also shown.

  \paragraph{Type Validity}
  First, we have the rules for the well-formedness of a type.  In
  lecture we summarized this by saying that all the free variables
  of the type should be in the context.  In the SML implementation
  of the language, a function \verb/tok/ (``type okay'') performs this check.
  Since both type variables and term (value) variables are
  represented by de Bruijn indices, it's necessary
  to go through the type, looking each de Bruijn index up in the context
  and seeing that it corresponds to a type variable, not a value variable.
  There are also conditions as usual saying that whenever we put a
  variable in the context, it's not there already; I'll take those as
  understood without being written explicitly.
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \ax{G,(a@type),G' |- a @type} \\
    \ax{G |- int @type} \qquad
    \ax{G |- bool @type} \qquad
    \ax{G |- float @type} \\
    \rul G |- t1 @type \quad G |- t2 @type
    \over{G |- (t1 -> t2) @type} \qquad
    \rul G |- t @type
    \over{G |- (t@ref) @type} \qquad
    \rul G |- t @type
    \over{G |- (t@cont) @type} \\
    \rul G |- t1 @type \quad ... \quad G |- tn @type
    \over{G |- (t1 * \cdots * tn) @type} \qquad
    \rul G |- t1 @type \quad ... \quad G |- tn @type
    \over{G |- (t1 + \cdots + tn) @type} \\
    \rul G,(a@type) |- t @type
    \over{G |- (\forall a. t) @type} \qquad
    \rul G,(a@type) |- t @type
    \over{G |- (\exists a. t) @type} \qquad
    \rul G,(a@type) |- t @type
    \over{G |- (\mu a. t) @type} \\
  \end{array}}%

  \paragraph{Subtyping}
  Next, we consider the subtyping rules, checked by the SML function
  \texttt{sub}.  Generally, we think of the
  subtyping relation >{t1 \leq t2} as having transitivity, which
  wouldn't be mode correct (in checking that >{t1 \leq t2}, we might
  have to guess a type >{\sigma} and check >{t1 \leq \sigma} and
  >{\sigma \leq t2}).  Fortunately, we can write the rules in such a
  way that transitivity ends up being a \emph{theorem}, rather than
  needing to be added as a rule.  When we do subtyping this way, we
  write >{t1 <= t2} rather than >{t1 \leq t2} and call it
  \emph{algorithmic subtyping}.  We could also remove the reflexivity
  rule, but since it's okay as to mode correctness, it's fine to
  leave it in, too.

  One more thing is that generally, in order to prove any theorems
  about subtyping, it's necessary to have the contexts hanging around
  too.  (Otherwise, at various points in the proofs, it's hard to
  argue that the types involved are well-formed.  What context should
  they be well-formed in?)  So our algorithmic subtyping judgment will
  actually be written >{G |- t1 <= t2}.

  Without further ado, the subtyping rules:
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \ax{G |- t <= t} \qquad
    \ax{G |- int <= float} \qquad
    \rul G |- \sigma_{1} <= t1\quad G |- t2 <= \sigma_{2}
    \over{G |- (t1 -> t2) <= (\sigma_{1} -> \sigma_{2})} \\
    \rul G |- t1 <= \sigma_{1} \quad ... \quad G |- tn <= \sigma_{n}
    \over{G |- (t1 * \cdots * tn) <= (\sigma_{1} * \cdots * \sigma_{n})} \qquad
    \rul G |- t1 <= \sigma_{1} \quad ... \quad G |- tn <= \sigma_{n}
    \over{G |- (t1 + \cdots + tn) <= (\sigma_{1} + \cdots + \sigma_{n})} \\
    \rul G,(a@type) |- t <= \sigma
    \over{G |- (\forall a. t) <= (\forall a. \sigma)} \qquad
    \rul G,(a@type) |- t <= \sigma
    \over{G |- (\exists a. t) <= (\exists a. \sigma)} \\
  \end{array}}%
  By adding the reflexivity rule, we've been able to get away without
  a bunch of boring axioms like >{bool <= bool} or >{a <= a}.

  You'll note that nothing was said about the type constructors
  >{t@ref}, >{t@cont}, or >{\mu a. t}.  In the case of >ref, neither
  covariant nor contravariant subtyping would work, for the reasons
  discussed in lecture.  For >cont, we could have a contravariant
  subtyping rule, but the associated coercion is tricky enough that
  adding the >cont rule is left as an extra credit problem.
  Finally, we come to the recursive types >{\mu a. t}.  On last fall's
  version of this assignment, the following UNSOUND rule was given:
  >>\begin{array}{c}
    \hbox{?`}\quad\rul G,(a@type) |- t <= \sigma
    \over{G |- (\mu a. t) <= (\mu a. \sigma)}\quad\hbox{?}\\
  \end{array}
  It's worth thinking about why this rule doesn't work, and what
  a correct rule might look like.
  \begin{question}{3.1}\extra
    (Somewhat tricky.) Show how to use the bogus rule above to write a program of type
    >int that evaluates to >{3.14159}.
  \end{question}

  \paragraph{Checking}
  Next we come to the rules for checking an expression against
  a known input type: >{G |- e <== t}.  These are implemented by
  the SML function \texttt{ck}.  It turns out that there are
  three general classes of rules which fall into this category.
  First of all, we have rules for constructing things of all the various
  types for which things can be explicitly constructed:
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \ax{G |- n <== int} \qquad
    \ax{G |- f <== float} \\
    \ax{G |- true <== bool} \qquad
    \ax{G |- false <== bool} \\
    \rul G,(f:t1->t2),(x:t1) |- e <== t2
    \over{G |- (fun~f(x). e) <== (t1 -> t2)} \qquad
    \rul G |- e <== t
    \over{G |- (ref@e) <== (t@ref)} \\
    \rul G |- e1 <== t1\quad ... \quad G |- en <== tn
    \over{G |- (e1, ..., en) <== (t1 * \cdots * tn)} \qquad
    \rul G |- e <== ti
    \over{G |- in_{i}@e <== (t1 + \cdots + tn)} \\
    \rul G,(a@type) |- e <== t
    \over{G |- (\Lambda a. e) <== (\forall a. t)} \qquad
    \rul G |- t@type\quad G |- e <== \{t/a\}\sigma
    \over{G |- pack(t,e) <== (\exists a. \sigma)} \\
    \rul G |- e <== \{\mu a. t/a\}t
    \over{G |- roll@e <== (\mu a. t)} \\
  \end{array}}%
  Notice how nicely we can treat >pack and >roll, for instance,
  because we assume that the >pack or >roll is located at a position
  in the term in which we already know what existential or recursive
  type the result is supposed to have.  We also got rid of the
  big annotation on the injection >{in_{i}@e}.  You should verify
  to yourself that all these rules are mode correct.

\kwd{goto}\kwd{with}
  In the next category we have various rules for deconstructing
  things, where the type being deconstructed isn't related to the
  type of the whole expression.  Here there's mixing of the
  checking judgment (for the whole expression) and the synthesis
  judgment (for the part of the expression being deconstructed).
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \rul G |- e ==> bool\quad G |- e1 <== \sigma\quad G |- e2 <== \sigma
    \over{G |- (if~e~then~e1~else~e2) <== \sigma} \\
    \rul G |- e ==> (t1 + \cdots + tn)\quad G,(x1:t1) |- e1 <== \sigma
       \quad...\quad G,(xn:tn) |- en <== \sigma
    \over{G |- (case~e~of~in_{1}@x1 => e1 | ... | in_{n}@xn => en) <== \sigma} \\
    \rul G |- e1 ==> (\exists a. t)\quad G,(a@type),(x:t) |- e2 <== \sigma
    \over{G |- (unpack(a,x)=e1~in~e2) <== \sigma} \\
    \rul G |- e2 ==> (t@cont)\quad G |- e1 <== t
    \over{G |- (throw~e1~to~e2) <== \sigma} \\
  \end{array}}%
  In the third rule, we need the special condition that >a isn't free
  in >\sigma.  The last rule is only mode correct if we put the premises
  in ``backwards.''  This suggests that the syntax of >throw might have
  been better the other way around.  (Maybe >{goto~e2~with~e1}?)

  The third category is more of a catchall for rules that don't
  construct or deconstruct anything, really:
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \rul G |- e1 ==> t \quad G,(x:t) |- e2 <== \sigma
    \over{G |- (let~x=e1~in~e2) <== \sigma} \qquad
    \rul G |- t@type \quad G |- \{t/a\}e <== \sigma
    \over{G |- (let~type~a=t~in~e) <== \sigma} \\
    \rul G,(x:\sigma@cont) |- e <== \sigma
    \over{G |- (letcc~x~in~e) <== \sigma} \qquad
    \rul G |- e1 ==> t \quad G |- e2 <== \sigma
    \over{G |- (e1;e2) <== \sigma} \\
    \rul G |- e1 <== \sigma \quad G |- e2 <== \sigma
    \over{G |- (try~e1~ow~e2) <== \sigma} \qquad
    \ax{G |- fail <== \sigma} \\
    \rul G |- e ==> int
    \over{G |- itof@e <== float} \qquad
    \rul G |- e ==> t \quad G |- t <= \sigma
    \over{G |- e <== \sigma} \\
  \end{array}}%
  The rule for >itof looks a bit strange.  We could certainly give
  it different modes. (Actually, we could give it all four
  possible mode combinations, and it would still be mode correct).
  But since >itof is going to be inserted in place of a use of
  subsumption (the last rule) it had better have exactly the same
  modes as subsumption, or strange things could happen.  We want the
  result of the coercion elaboration to be well-typed without changing
  any of the modes around.

  \paragraph{Synthesis}
  Finally, we need to think about the rules for synthesizing a type for
  expressions
  for which this makes sense.  We will be quite restrictive about this,
  only giving synthesis rules for constructs for which there was
  not also a checking rule.  This seems restrictive, but in a
  realistically larger language, it becomes quite important.  One
  reason is that if there's only one mode in which any particular
  construct can be handled, there's no non-determinism in the
  algorithm.  All these rules are implemented by the SML function
  \texttt{syn}.

  Most of the synthesis rules are about deconstructing something:
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \rul G |- e1 ==> (\sigma -> t)\quad G |- e2 <== \sigma
    \over{G |- (e1@e2) ==> t} \qquad
    \rul G |- e ==> (t1 * \cdots * tn)
    \over{G |- e.i ==> ti} \\
    \rul G |- e ==> (t@ref)
    \over{G |- !e ==> t} \qquad
    \rul G |- e1 ==> (t@ref) \quad G |- e2 <== t
    \over{G |- (e1:=e2) ==> t} \\
    \rul G |- e ==> (\forall a. t) \quad G |- \sigma@type
    \over{G |- e[\sigma] ==> \{\sigma/a\}t} \qquad
    \rul G |- e ==> (\mu a. t)
    \over{G |- unroll@e ==> \{\mu a. t/a\}t} \\
  \end{array}}%

\deftok{opr}{\textit{opr}}
  The remaining synthesis rules handle variables, primitive operations
  such as (>+) and the like,
  and the type annotation construct:
  {\renewcommand{\arraystretch}{2.5}%
  >>\begin{array}{c}
    \rul (opr : t1 * \cdots * tn -> \sigma)\quad
      G |- e1 <== t1 \quad...\quad G |- en <== tn
    \over{G |- opr(e1,...,en) ==> \sigma} \\
    \ax{G,(x:t),G' |- x ==> t} \qquad
    \rul G |- t@type \quad G |- e <== t
    \over{G |- (e:t) ==> t} \\
  \end{array}}%
  The rule for variables makes sense because the modes for all of the
  judgments specify that the context >G is \emph{input}.  (If you look
  back at all the rules that put variables in the context, you'll see
  that in each case the type is known.)  Thus, when we come to a
  variable, we can find its type in the context and produce that type
  as output, so variables get a synthesis rule.

  A somewhat subtle point about the bidirectional system is that it
  lets us get away with fewer checks on the well-formedness of types,
  as long as we think about the algorithm correctly.  The general
  invariant is that we \emph{assume} that any types mentioned in
  >G or >t (if >t is an input) are already well-formed before the
  algorithm that decides the judgment runs.  Conversely, when the
  algorithm finishes, if it produces a type
  as output, it is responsible for \emph{guaranteeing} that the
  output type is well-formed.  With this invariant, pretty much the
  only time a type needs to be checked for well-formedness is when
  it's something that was mentioned explicitly in the expression
  being checked (like in the syntax for ascriptions, or for applying
  a type function).

  This completes the initial static semantics of our language.  In
  a later section we will extend it to generate coercions to replace
  instances of the subsumption rule.

  \section{De Bruijn Indices for Type Variables}
  Before we get to the rules for generating coercions, I want to
  mention an interesting phenomenon that occurs when you use de
  Bruijn indices for type variables.

\defvariable{b}{\beta}
  Looking at the rule for typing functions:
  >>{\rul G,(f:t1 -> t2),(x:t1) |- e <== t2
     \over{G |- (fun~f(x). e) <== (t1 -> t2)}}
  let's think about what it looks like in de Bruijn representation.
  To make this more concrete, let's pick a specific context and types:
  >>{\rul (a@type),(y:a),(f:a -> a*a),(x:a) |- (x,y) <== (a * a)
     \over{(a@type),(y:a) |- (fun~f(x). (x,y)) <== (a -> a * a)}}

  Now what should the de Bruijn version look like?  This is tricky
  because there are type variables hanging around in the context, and
  in order to give them numbers, we have to decide what how many
  ``nested binders'' to count.  We want to think of each item in the
  context as being a binder, the scope of which extends everywhere
  to its right, both within the context, and in the expression and
  type on the right side of the turnstile.

  Following this rule, we arrive at:
  >>{\rul (-@type),(-:#1),(-:#2 -> #2*#2),(-:#3) |- (#1,#3) <== (#4 * #4)
     \over{(-@type),(-:#1) |- (fun~-(-). (#1,#3)) <== (#2 -> #2 * #2)}}

  One way to check that this is right is to recall that we have the
  invariant that whenever the checking algorithm is invoked with
  >{G |- e <== t}, we should have >{G |- t@type}.  In this case, that
  means that we should have
  >>{(-@type),(-:#1) |- (#2 -> #2 * #2)@type}
  in the conclusion, which indeed checks out, and
  >>{(-@type),(-:#1),(-:#2 -> #2*#2),(-:#3) |- (#4 * #4)@type}
  in the premise, which also checks out.

  But this means that the \emph{same type} can have a \emph{different
  form} when it's carried from the conclusion into the premise, or
  when it moves into various places in the context.  In fact,
  the type >{(#2 -> #2 * #2)} in the conclusion takes \emph{three}
  different forms in the premise: it's used in the hypothesis
  for the type of the function name: >{(-:#2 -> #2*#2)}; part of
  it is used in the hypothesis for the type of the function
  argument: >{(-:#3)}; and part of it is used in the right-hand
  side of the premise as the type of the function's body: >{(#4*#4)}.

  All of these different forms arise by \emph{shifting} the indices
  in the type up by different amounts.  We want to summarize the
  outcome of this shifting process without getting drowned in numbers,
  so we'll use the notation >{t^{(n)}} for the result of taking a
  type >t in de Bruijn notation and shifting all its free indices
  by >n (so >{#1} becomes >{#(n+1)}, and so on).

  With this notation, we can restate the general form of the function
  typing rule for de Bruijn indices as follows:
  >>{\rul G,(f:t1 -> t2),(x:t1^{(1)}) |- e <== t2^{(2)}
     \over{G |- (fun~f(x). e) <== (t1 -> t2)}}
  Here the names >f and >x are only mnemonics---they don't
  actually occur in the de Bruijn representation.
  Nothing in >e itself needs to be shifted, because anything in >e is
  already in the scope of >G, >f, and >x in the conclusion,
  and is still in the scope of >G, >f, and >x in the premise---the
  number of binders hasn't changed.

  Certain laws help us reason about this shifting process.  For
  instance, if >{G |- t@type}, and >{G'} has length >n,
  then >{G,G' |- t^{(n)}@type}.  Also, whenever >{G,(x:t),G'}
  is well-formed, then >{G |- t@type}.

  There are two reasons I'm belaboring all this: first of all, the
  code you'll be working with has all of this shifting in it, and I
  don't want you to be confused.  Second, this is tricky stuff.
  The sample ``solution'' handed out last fall for this assignment got
  all this totally wrong.  I think the only reason the
  problems with it weren't discovered was that, amusingly, all the various
  de Bruijn index bugs in it had mostly canceled each other out.

  So although initially this assignment was to have had you writing part
  of the code for the bidirectional checker yourselves, it seemed
  cruel and unusual punishment to make you do it when not even the
  teaching staff got it right last fall.

  \section{Generating Coercions}
  Now we've almost come---finally!---to the actual questions.

  The initial code for this assignment is able to typecheck certain
  programs that it can't run.  For example, using \verb/Top.itype()/
  you can verify that
    >>{(fun~f(x). sqrt(x +. 3{.}14159) : float -> float) (1 : int) : float}
  typechecks, but
  if you try to run it with \verb/Top.ieval_noelab()/, the machine gets stuck.
  The reason is that the type system allows subsumption to silently convert
  an >int to a >float, but the operational semantics can't do that. (Remember
  that {>int}s and {>float}s might need to be in different registers, or
  something.)

  What we want is for all the uses of subsumption to be \emph{elaborated}
  into explicit
  coercions.  If we're just subsuming >int to >float, the corresponding
  coercion will be the primitive operation >itof.  With more complicated
  uses of subsumption, though, the coercions will be more complex.

  Stubs for the code to do this are already given in \texttt{typing.sml};
  if you fill them in, then the \texttt{Top.ieval()} function will use
  them to elaborate terms before sending them to the evaluator, and thus
  the function above should run properly rather than getting stuck.

\deftok{~~>}{\rightsquigarrow}
  The basic idea is that you'll instrument the static semantics above
  with extra outputs giving the elaborated form of the expressions being
  checked:
  >>\begin{array}{ll}
    G^+ |- e^+ <== t^+ ~~> e'^- & \texttt{elck g e t} \\
    & \hfil\hbox{Check $e$ against type $t$ returning $e'$}\hfilneg \\
    G^+ |- e^+ ==> t^- ~~> e'^- & \texttt{elsyn g e} \\
    & \hfil\hbox{Infer a type $t$ for $e$ and return $e'$}\hfilneg \\
    G^+ |- t1^+ <= t2^+ / e^+ ~~> e'^- & \texttt{elsub g t1 t2 e} \\
    & \hfil\hbox{Check $t1$ a subtype of $t2$ and convert $e$ to $e'$}\hfilneg \\
  \end{array}

  Thus, there will be a written part, where you give the rules for these
  judgments, and a programming part, where you implement them.

  To get you started, here is the rule, alluded to above, for converting
  an >int to a >float:
  >>{\ax{G |- int <= float / e ~~> (itof@e)}}

  And here is the subsumption rule instrumented with elaborations:
  >>{\rul G |- e ==> t1 ~~> e' \quad G |- t1 <= t2 / e' ~~> e''
     \over{G |- e <== t2 ~~> e''}}
  The mode correctness is now a bit tricky.  First, in the conclusion,
  we get >G and >e and >t2 as inputs.  Next, by invoking the algorithm
  for the first premise, we get >t1 and >{e'} as outputs.  Then,
  invoking the algorithm for the second premise, we get >{e''} as
  output.  Finally, we return >{e''} in the conclusion as output to
  our caller.

  As another example, here's the rule for applications:
  >>{\rul G |- e1 ==> (\sigma -> t) ~~> e1' \quad G |- e2 <== \sigma ~~> e2'
     \over{G |- (e1@e2) ==> t ~~> (e1'@e2')}}

  The rule for >{let~type} we'll be using is the following:
  >>{\rul G |- t@type \quad G |- \{t/a\}e <== \sigma ~~> e'
     \over{G |- (let~type~a=t~in~e) <== \sigma ~~> e'}}
  This is the only elaboration rule where some kind of ``evaluation''
  happens; that is, the >{let~type} is no longer present in the result >{e'}
  of the elaboration.  In general, it's hard to see how >{e'} could be
  put back into the form >{let~type~a=t~in~...}, at least not in a
  uniquely determined way.

  And a final example, the rule for annotations:
  >>{\rul G |- e <== t ~~> e'
     \over{G |- (e:t) ==> t ~~> (e':t)}}
  (The annotation is still there in the output; otherwise, the output
  wouldn't typecheck.)

  In general, we'd like the following theorems to be true (though you
  don't have to write up the proofs).

  \begin{quote}
  1. If >{G |- e <== t}, then >{G |- e <== t ~~> e'} for some >{e'},
  and furthermore >{G |- e' <== t} \emph{without} any
  subsumptions (other than reflexivity).

  2. If >{G |- e ==> t}, then >{G |- e ==> t ~~> e'} for some >{e'},
  and furthermore >{G |- e' ==> t} without
  subsumptions other than reflexivity.

  3. If >{G |- t1 <= t2}, and >{G |- e ==> t1}, then
  >{G |- t1 <= t2 / e ~~> e'} for some >{e'}, and furthermore
  >{G |- e' <== t2} without any non-trivial subsumptions
  (assuming >e doesn't use any non-trivial subsumptions).
  \end{quote}

  Take particular note of the modes in part 3.  They ensure that 
  the coercion from >{e} to >{e'} fits into the same slot that
  the original use of the subsumption rule did, because the modes are
  the same as for the subsumption rule.

  Conversely, we don't want the system instrumented with elaborations
  to type any \emph{more} programs than the original system:

  \begin{quote}
  1. If >{G |- e <== t ~~> e'}, then >{G |- e <== t}.

  2. If >{G |- e ==> t ~~> e'}, then >{G |- e ==> t}.

  3. If >{G |- t1 <= t2 / e ~~> e'}, then >{G |- t1 <= t2}.
  \end{quote}

  Finally, although we won't make the notion precise here, the original
  expression and the elaborated one should ``do the same thing'' in
  the operational semantics.  You shouldn't elaborate >true into >false,
  for instance.  (The difficulty in making this precise is that part
  of the point is that the original term and the elaborated term don't
  do \emph{exactly} the same thing, because one gets stuck and the other
  doesn't!)

  \begin{question}{5.1}\points{45}
    Write up instrumented versions of all the typing rules (the named-form
    rules, not the de Bruijn ones) given in
    Section 3 of the assignment.  This includes the rules for
    >{G |- e ==> t ~~> e'}, for >{G |- e <== t ~~> e'}, and for
    >{G |- t1 <= t2/e ~~> e'}. The theorems above should
    hold for your rules, but you don't have to prove them.
    Turn your work in in lecture, or email it to me by 11:59 p.m.
    (If you do it by hand, you can always scan it and email me the scans.)
  \end{question}

  The final part of the assignment is to implement your elaboration rules.
  For this, you should fill in the stubs of \texttt{elsyn}, \texttt{elck},
  and \texttt{elsub} in the file \texttt{typing.sml}.  The code for
  \texttt{syn}, \texttt{ck}, and \texttt{sub} should be your model, except
  that you will need to add extra outputs (and an input, for \texttt{elsub})
  to return the result of the elaboration.

  You should not need to do any de Bruijn shifting, or call the functions
  for substitution, on the elaborated terms
  that you construct (although the part that you inherit from \texttt{ck}
  will still have to).

  \begin{question}{5.2}\points{45}
    Write code for the \texttt{elsyn}, \texttt{elck}, and \texttt{elsub}
    functions in \texttt{typing.sml}.  Turn your modified file in to the
    handin directory in AFS.
  \end{question}

  Finally, you should check that \texttt{Top.ielab()}, which calls your
  elaboration functions, returns sensible results, and that \texttt{Top.ieval()},
  which elaborates before evaluating, doesn't get stuck on some examples
  you cook up for which the unelaborated version \verb/Top.ieval_noelab()/
  does.

  \begin{question}{5.3}\points{10}
    Put your test examples in a file \texttt{testelab.mml}, and hand
    it in to your AFS handin directory.
  \end{question}

\end{document}
