\documentclass[letterpaper]{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}
\defvariable{G}{\Gamma}
\defvariable{t}{\tau}
\easynotation
\def\skp{\\[1ex]}

\begin{document}
  \title{Assignment 4: Adding exceptions and continuations to MinML}
  \author{15-312: Foundations of Programming Languages \\
    Kevin Watkins $\langle$kw@cmu.edu$\rangle$}
  \date{\begin{tabular}{l} Out: Thursday, February 17, 2005 \\
    Due: Thursday, March 3, 2005 (11:59 p.m.) \\
    \end{tabular}\\[1ex]
    100 points total
    }
  \maketitle

  In this programming assignment, your task will be to extend the MinML
  typechecker and evaluator of Assignment~2 to work with sum types,
  product types, exceptions and continuations.  The code you'll start
  with is mostly the starter code for Assignment~2, except that syntax,
  parsing and printing for all the new features have been added.  Your
  job will be to start with either your solution or the model solution
  to Assignment~2, and extend the type checker and evaluator for all
  the new features.  (This time, I've done the de Bruijn translator for
  you.)

  As before, you can find the starter code in \[
    \texttt{/afs/andrew/scs/cs/15-312/handout/4/},
  \] and you'll be handing your solution in by copying it to \[
    \texttt{/afs/andrew/scs/cs/15-312/handin/}\textit{you}\texttt{/4/}.
  \]
  The files you will be handing in are:
  \ln{\tt\hfil\begin{tabular}{ll}
    typing.sml & 1.mml \\
    eval.sml   & 2.mml \\
    fail.mml   & 3.mml \\
  \end{tabular}}

  If you don't remember all the advice regarding submitting your
  solution, grading criteria for programming assignments, and all that
  jazz, now would be a good time to go back to the
  problem statement for Assignment~2 and refresh your memory.

\kwd{fail}
\code{type}\code{datatype}\code{of}
\code{exp}\code{stack}\code{state}\code{int}
\code{Eval}\code{Return}\code{Fail}\code{Exit}\code{Stack}
\code{step}\code{DBMinML}\code{exp}
  \section*{The C machine}
  One thing that's changed since Assignment~2 is that we're using the
  C machine rather than the M machine.  So our >step function is now
  going to take a state and return another state, rather than taking
  an expression and returning another expression.

\def\rep#1{\ulcorner#1\urcorner}
  So how should we represent states in SML?  It seems reasonable to
  have a datatype with a separate constructor for each kind of state,
  so we'd end up with something like
  >>\begin{array}{l@{\qquad}l}
    datatype~state ={} \\
    \qquad \phantom{{}|{}} Eval~of~stack * exp & \rep{k > e} = Eval(k,e) \\
    \qquad {}| Return~of~stack * exp           & \rep{k < v} = Return(k,v) \\
    \qquad {}| Fail~of~stack                   & \rep{k << fail} = Fail(k) \\
  \end{array}
  where on the right I've written the \emph{representation function}
  >{\rep{{-}}} showing how each state of the C machine is represented in
  SML.

  Now we have to figure out how to represent stacks.  Probably the most
  straightforward solution would be to have a separate datatype constructor
  for each kind of stack frame.  But there are so many kinds of frames
  that it would be pretty tedious to list them all.  And the different
  kinds of frames all seem to have pretty much the same structure; they
  all represent some kind of postponed work that has to be done to finish
  evaluating an expression.  It would be great if we could represent the
  postponed work as an SML function, and just call the function to do
  whatever the stack frame is supposed to do.

  One way to think about stacks is to consider what kinds of things we'll
  be doing when we need to look at the stack.  In fact, the C machine
  only looks at the stack when it's trying to take a step in one of
  the situations >{k < v} or >{k << fail}.  If we know what to do in
  both of those situations, we're set.

\code{unit}
  This suggests that our representation for a stack >k should be a pair of
  SML functions >{(f1,f2)}.  The function >f1 says what to do when we're
  returning a value >{k < v} to the stack >k.  In that case, we'll call
  >{f1@v} and step to whatever state that is.  The other function >f2
  says what to do when we're returning failure >{k << fail} to the stack
  >k.  In that case, we'll just call >{f2@()}.  Finally, if we want to
  print states of the machine, it's impossible to print the SML functions
  >f1 and >f2, but if we store the number of frames with the stack, at
  least we can see how many there are.  With this in mind, we set
  >>{datatype~stack = Stack~of~int * (exp -> state) * (unit -> state).}
  (Actually, this is mutually recursive with >state and >exp, so the SML
  syntax makes us declare them all at the same time.)

  The disadvantage of this representation is that we have no way of
  printing out a stack so that we can see what exactly it looks like at
  each step of the C machine evaluation.  But the convenience of using
  SML functions for the stack seems to be worth more than the ability
  to print them out.

  These datatypes have been included in the starter code for this
  assignment.  The M machine evaluator from Assignment~2 has been converted to
  a C machine evaluator based on them.  You should look at the supplied code
  in \texttt{eval.sml} now, and make sure you understand how it works.
  In particular, you need to fully understand the functions \texttt{eval},
  \texttt{ret}, \texttt{fail}, \texttt{frame}, and \texttt{try}.  Only
  \texttt{eval}, \texttt{ret}, and \texttt{frame} are used in the
  starter code you've been given, but I provided \texttt{fail} and
  \texttt{try} in the hope that they will be useful to you when
  implementing exceptions.

  \section*{Syntax and parsing}
  Once again, the parser for the language we're dealing with has been
  provided for you.  Rather than include the grammar for the ASCII
  syntax here, I'll just mention that it's in the file \texttt{parse.sml}.

\kwd{end}\kwd{fun}\kwd{bool}\kwd{int}\kwd{is}\kwd{if}\kwd{then}\kwd{else}
  {\bf Note} that the syntax has changed slightly from what we used
  in Assignment~2.  I got fed up with the >{end}s everywhere, so now
  they're not necessary.  For example, >>{fun~f(x:bool):int~is~if~
    x~then~1~else~2} is now legal MinML syntax.  A construct like >fun or >if
  extends as far to the right as possible, consistent with the pairing
  of parentheses and so forth.

\kwd{letcc}
\kwd{in}\kwd{case}\kwd{abort}\kwd{of}
  Many constructs in the extended language we'll be working with need
  extra type information to ensure that types are unique.  The convention
  in such cases is that the type of the whole expression is written
  in brackets after the keyword starting the expression.  For example, in
  >{letcc[t]~x~in~e}, the type of the whole expression is >t.

  I also added comment syntax to the lexical analyzer; any line starting
  with the character `\texttt{\%}' is ignored.

  \section{Product and sum types}
  The first extensions to the language from Assignment~2 are product and
  sum types.  These have the syntax >>{t ::= ... | 1 | t1 * t2 | 0 | t1 + t2}
  The corresponding expressions are
  >>\begin{array}{rcl}
    e &::=& ... | () | e1 , e2 | e.1 | e.2 \\
      &   & \qquad | abort[t]@e | in1[t]@e | in2[t]@e | case~e~of~in1@x1 => e1 | in2@x2 => e2 \\
  \end{array}

\def\and{\qquad}
\rname{UnitTyp}\rname{PairTyp}\rname{FstTyp}\rname{SndTyp}
  First, the products.  They have static semantics given by the following
  typing rules:
  >>\begin{array}{c@{\qquad}c}
    \ax[UnitTyp] {G |- () : 1} & 
    \rul[PairTyp] G |- e1 : t1 \and G |- e2 : t2 
    \over        {G |- e1,e2 : t1 * t2} \skp
    \rul[FstTyp]  G |- e : t1 * t2
    \over        {G |- e.1 : t1} &
    \rul[SndTyp]  G |- e : t1 * t2
    \over        {G |- e.2 : t2} \\
  \end{array}

  We only treat binary and zero-ary products.  The unit type,
  written >1, is a zero-ary product.  Parentheses are optional around
  pairs >{e1,e2}; this means you can use
  the left-associativity of `>,' and `>*' together to write things like
  >{1,2,3 : int*int*int}.

\fname{dom}
\rname{AbortTyp}\rname{CaseTyp}\rname{InlTyp}\rname{InrTyp}
  Now, the sums.  They have static semantics given by the following
  typing rules:
  >>\begin{array}{c}
    \rul[AbortTyp] G |- e : 0
    \over         {G |- abort[t]@e : t} \skp
    \rul[CaseTyp^{1}]  G |- e : t1 + t2 \and
                   G,(x1:t1) |- e1 : t \and
                   G,(x2:t2) |- e2 : t
    \over         {G |- case~e~of~in1@x1=>e1 | in2@x2=>e2 : t} \skp
    \rul[InlTyp]   G |- e : t1
    \over         {G |- in1[t1+t2]@e : t1+t2} \qquad
    \rul[InrTyp]   G |- e : t2
    \over         {G |- in2[t1+t2]@e : t1+t2} \skp
    {}^{1}\enspace x1,x2\notin dom@G \\
  \end{array}

  The void type, written >0, is a zero-ary sum.  This
  can come in handy when we're programming with complicated control
  structures---continuations or what have you---because we can express
  the invariant that certain code never returns by giving it a type
  involving >0.  The only expression associated with the void type
  is >abort, which is just like >case except that it has zero arms
  instead of two.

  Now, for the dynamic semantics.  The values for products and sums are
  >>{v ::= ... | () | v1,v2 | in1[t]@v | in2[t]@v}
  The C machine rules for products and sums are as follows:
  >>\begin{array}{l}
    k > () |-> k < () \skp

    k > e1,e2 |-> k |> [],e2 > e1 \\
    k |> [],e2 < v1 |-> k |> v1,[] > e2 \\
    k |> v1,[] < v2 |-> k < v1,v2 \skp

    k > e.1 |-> k |> [].1 > e \\
    k |> [].1 < v1,v2 |-> k < v1 \\
    k > e.2 |-> k |> [].2 > e \\
    k |> [].2 < v1,v2 |-> k < v2 \skp

    k > abort[t]@e |-> k |> abort[t]@[] > e \skp

    k > in1[t]@e |-> k |> in1[t]@[] > e \\
    k |> in1[t]@[] < v |-> k < in1[t]@v \\
    k > in2[t]@e |-> k |> in2[t]@[] > e \\
    k |> in2[t]@[] < v |-> k < in2[t]@v \skp

    k > case~e~of~in1@x1=>e1|in2@x2=>e2 \\
    \qquad {}|-> k |> case~[]~of~in1@x1=>e1|in2@x2=>e2 > e \\
    k |> case~[]~of~in1@x1=>e1|in2@x2=>e2 < in1[t]@v \\
    \qquad {}|-> k > \{v/x1\}e1 \\
    k |> case~[]~of~in1@x1=>e1|in2@x2=>e2 < in2[t]@v \\
    \qquad {}|-> k > \{v/x2\}e2 \\
  \end{array}

  Note that the first rule for >abort is analogous to the first rule for
  >case, but whereas >case has two more rules, >abort has zero.  Funny how
  that works out.

\code{step}\code{NoStep}
  \begin{question}{1.1}\points{45}
  Following the rules above, extend the typing function in
  \texttt{typing.sml} and the >step function in \texttt{eval.sml}
  to handle products and sums (including the unit and void constructs).

  Note that the C machine implemented in \texttt{eval.sml} uses
  SML functions to represent the stack, rather than explicit syntax.
  Still, the syntax for frames in the rules above should suggest to
  you what SML functions to use to implement them.

  As usual, the >step function must satisfy the following specification:
  \begin{quote}
    If >s is a closed C machine state, and >{\rep{s}} is its SML
    representation as a >state, and >{s |-> s'}, then >{step(\rep{s}) =
    \rep{s'}}, where >{\rep{s'}} is the SML representation of the 
    C machine state >{s'}.

    If >s is a closed C machine state, and >{\rep{s}} is its SML
    representation, and >s cannot take a C machine step, then
    >{step(\rep{s})} must raise exception >NoStep.
  \end{quote}

  {\bf Note} that the specification says nothing about the states
  involved being well typed.
  \end{question}


  \section{Exceptions}
  The next extension to the language introduces exceptions and
  exception handling.  As in lecture, the exceptions you'll be
  implementing don't carry any values along with them, unlike
  SML exceptions.

\kwd{try}\kwd{ow}
\rname{FailTyp}\rname{TryTyp}
  The syntax for exceptions is as follows:
  >>{e ::= ... | try~e1~ow~e2 | fail[t]}
  No new types or values are introduced.  The static semantics is
  based on the rules
  >>{
  \ax[FailTyp] {G |- fail[t] : t} \qquad
  \rul[TryTyp] G |- e1 : t \and G |- e2 : t
  \over       {G |- try~e1~ow~e2 : t}
  } and the C machine dynamic semantics is based on the rules
  >>\begin{array}{l}
    k > try~e1~ow~e2 |-> k |> try~[]~ow~e2 > e1 \\
    k |> try~[]~ow~e2 < v |-> k < v \\
    k |> try~[]~ow~e2 << fail |-> k > e2 \\
    k |> f << fail |-> k << fail\quad\hbox{if }f \not= try~[]~ow~e2 \\
    k > fail[t] |-> k << fail \\
  \end{array}

  \begin{question}{2.1}\points{20}
    As before, extend \texttt{typing.sml} and \texttt{eval.sml} to
    treat the new constructs.
  \end{question}


\kwd{cont}\kwd{throw}\kwd{stack}
\kwd{to}
\rname{LetccTyp}\rname{ThrowTyp}\rname{ContTyp}
  \section{First-class continuations}
  The last extension to the language adds first-class continuations
  in the style we saw in lecture.  The new types are >>{t ::= ... | t@cont}
  while the new expressions are >>{e ::= ... | letcc[t]~x~in~e |
  throw[t]~e1~to~e2 | cont(k)}
  The static semantics is given by the rules
  >>\begin{array}{c}
    \rul[LetccTyp^{1}] G,(x:t@cont) |- e:t
    \over         {G |- letcc[t]~x~in~e:t} \qquad
    \rul[ThrowTyp] G |- e1 : t' \and G |- e2 : t'@cont
    \over         {G |- throw[t]~e1~to~e2:t} \\
    \rul[ContTyp]  \cdot |- k : t@stack
    \over         {\cdot |- cont(k) : t@cont} \\
    {}^{1}\enspace x \notin dom@G \\
  \end{array}
  Now since stacks >k are represented by SML functions, there is no way,
  really, to typecheck an expression of the form >{cont(k)}.  Thus, you
  do not have to implement the rule >ContTyp.  You will need to implement
  the other two typing rules.

  Now for the dynamic semantics.  There is a new value, namely,
  >{cont(k)}, where >k is a stack.  The C machine rules are
  >>\begin{array}{l}
    k > letcc[t]~x~in~e |-> k > \{cont(k)/x\}e \\
    k > throw[t]~e1~to~e2 |-> k |> throw[t]~[]~to~e2 > e1 \\
    k |> throw[t]~[]~to~e2 < v1 |-> k |> throw[t]~v1~to~[] > e2 \\
    k |> throw[t]~v1~to~[] < cont(k') |-> k' < v1 \\
  \end{array}

  \begin{question}{3.1}\points{30}
    As before, extend \texttt{typing.sml} and \texttt{eval.sml} to
    treat the new constructs.  You do not have to implement the
    rule >ContTyp, however.
  \end{question}


  \section{Test cases}
  You are responsible for creating some test cases to help verify that
  your implementation is working.  Your test cases should include comments
  describing what is being tested and what the expected results are.

  \begin{question}{4.1}\points{5}
    Create four test cases that exercise these new constructs. Exactly
    one, \texttt{fail.mml}, should fail to typecheck, for an
    ``interesting'' reason.  All of the others must be well typed.
    None of the test cases can loop forever.  Name your test cases
    \texttt{1.mml},
    \texttt{2.mml}, \texttt{3.mml}, and \texttt{fail.mml}.  The test
    cases should be handed in together with your other files.
  \end{question}
\end{document}
