\documentclass{article}
\usepackage{latexsym}
\usepackage{lcom}
\usepackage{cdsty}
\input{minml-defns}
\newcommand{\mua}{\mu\alpha .\,}
%\newcommand{\mua}[1]{\mu \alpha .\, {#1}}
\newcommand{\nat}{\mua{\unit + \alpha}}
\newcommand{\unit}{\mbox{$\mathbf{1}$}}
\newcommand{\fold}{\mbox{\textbf{fold}}}
\newcommand{\foldt}{\mbox{\textbf{fold}}^{\mua{\tau}}}
\newcommand{\unfold}{\mbox{\textbf{unfold}}^{\mua{\tau}}}
\newcommand{\unfoldn}{\mbox{\textbf{unfold}}^{nat}}
\newcommand{\apply}{\mbox{\textbf{apply}}}
\newcommand{\pair}[1]{\langle #1 \rangle}
\newcommand{\ep}{\pair{}}
\newcommand{\inl}[1]{\mbox{\textbf{inl}}^{#1}}
\newcommand{\inlt}{\mbox{\textbf{inl}}^{\tau_1+\tau_2}}
\newcommand{\inrt}{\mbox{\textbf{inr}}^{\tau_1+\tau_2}}
\newcommand{\inr}[1]{\mbox{\textbf{inr}}^{#1}}
\newcommand{\fun}[3]{\mbox{\textbf{fun }} {#1} {#2} \mbox{\textbf{ is }}
 { #3}\mbox{ \textbf{end} }}
\newcommand{\case}[5]{\mbox{\textbf{case }} {#1}\mbox{\textbf{ of }}
  {#2}\Rightarrow {#3}\mid {#4} \Rightarrow  {#5}} 
\newcommand{\caset}{\mbox{\textbf{case }} e \mbox{\textbf{ of }}
  \inl{} \ x_1\hastype\tau_1\Rightarrow e_1\mid \inr{} \ x_2\hastype\tau_2 \Rightarrow  e_2}

\begin{document}

\begin{center}
{\Large CS 15-312 Assignment \#2 \\
Extending \minml with Products, Sums\\ and Recursive Types
\vsk
{\large Assigned: Friday, February 11 \\
Due: Friday, February 25, 6 PM \\} }
\end{center}

\section{Introduction}
In this assignment we extend \minml with Products, Sums and Recursive
Types; you are asked to:
\ben
\item
Prove preservation and progress for the overall extended language;
\bit
\item
Preservation: assume $e\mapsto e'$; then if $e\hastype \tau$, then $e\hastype
\tau'$.
\item
Progress: if $e\hastype\tau$, then either $e$ is a value or there exists
$e'$ such that $e\mapsto e'$.
\enit
\item Implement static and dynamic semantics for it.
\enen

\noindent
\textbf{Note:} recursive types are \textbf{extra} credit. Here's the
breakdown:
\bit
\item Products and Sums: preservation 30 pts, progress 30 pts,
  implementation 40 pts.
\item Recursive types:   preservation 10 pts, progress 10 pts,
  implementation 30 pts.
\enit

\section{Product Types}
\label{ssec:prod}
Think of products as the type of ML tuples.  However, in our extension
to \minml, we will only add binary tuples (pairs), though they can be
nested. For pair destructor,  i.e.\ expression that takes apart a
value of type product, we introduce a \mathcd{bind} expression for
pairs that uses a limited form of pattern matching. As a special case
(the $0$-ary product) we introduce the type \unit\ which has only one
value, namely $\ep$.

\[
\begin{array}{rrcl}
\mathit{Types} & \tau &  \bnfas &\dots\bnfalt\tau_1 * \tau_2\bnfalt\unit\\
\mathit{Expressions}& e & \bnfas & \dots\bnfalt \pair{e_1,e_2}\bnfalt
\Bind{p}{e_1}{e_2}\bnfalt \ep\\
\mathit{Patterns} & p &\bnfas & \WildPat \bnfalt \VarPat{x}{\tau} \bnfalt
\Pair{p_1}{p_2}\bnfalt\ep\\
\mathit{Values} & v &\bnfas & \dots \bnfalt \Pair{v_1}{v_2}\bnfalt\ep
\end{array}
\]
We have four kinds of patterns: wild card patterns which
can take any type, variable patterns which can take only the specified
type, empty patterns of type \unit\ and pair patterns which take the product of the types of their
constituent patterns. We need to define a new typing judgment on patterns
of the form $\Gamma\vdash p : \tau \gens \Gamma'$.  This
judgment will essentially
do pattern matching on $p$ to determine whether it can be given
type $\tau$, and if so, add the variables contained in $p$ to
the context $\Gamma$ with their respective types, producing $\Gamma'$.

\[\begin{array}{c}
\ianc{}{\Gamma \vdash \WildPat \hastype \tau \gens \Gamma}{[WildPat]} \qquad
\ianc{}{\Gamma \vdash (x\oftp\tau) \hastype \tau \gens \Gamma[x\oftp\tau]}{[VarPat]}
\vsk
\ianc{}{\Gamma \vdash \ep \hastype \unit \gens \Gamma}{[EmptyPat]} \qquad
\ianc        {\typpatJ{\Gamma}{p_1}{\tau_1}{\Gamma'} \quad
         \typpatJ{\Gamma'}{p_2}{\tau_2}{\Gamma''}}
{\typpatJ{\Gamma}{\Pair{p_1}{p_2}}{\Times{\tau_1}{\tau_2}}{\Gamma''}}
{[PairPat]}
\end{array}
\]

Typing rules:
\[
\begin{array}{c}
\ianc{}{\GG\vd \ep\hastype\unit}{[UnitTyp]}\qquad
\ianc    {\typingJ{\Gamma}{e_1}{\tau_1} \quad
        \typingJ{\Gamma}{e_2}{\tau_2}}{\typingJ{\Gamma}{\Pair{e_1}{e_2}}{\Times{\tau_1}{\tau_2}}}
{[PairTyp]}
\vsk
\ianc {\typingJ{\Gamma}{e_1}{\tau_1} \quad
        \typpatJ{\Gamma}{p}{\tau_1}{\Gamma'} \quad
        \typingJ{\Gamma'}{e_2}{\tau}}{\typingJ{\Gamma}{\Bind{p}{e_1}{e_2}}{\tau}}
{[BindTyp]}
\end{array}\]

The evaluation rules are as expected.  The only ones that
are a little tricky are those involving {\tt bind} because we need to do
pattern matching on the pattern in the {\tt bind} and, if it is a pair
pattern, break the expression into two nested {\tt bind}'s.
Aside from that, left-to-right evaluation prevails as usual.

Evaluation Rules:

\[\begin{array}{c}
\ianc   {\stepsJ{e_1}{e_1'}}{\stepsJ{\Pair{e_1}{e_2}}{\Pair{e_1'}{e_2}}}
{[PairLeft]}
\qquad
\ianc   {\stepsJ{e_2}{e_2'}}{\stepsJ{\Pair{v_1}{e_2}}{\Pair{v_1}{e_2'}}}
{[PairRight]}
\vsk
\ianc   {\stepsJ{e_1}{e_1'}}{\stepsJ{\Bind{p}{e_1}{e_2}}{\Bind{p}{e_1'}{e_2}}}
{[BindRHS]}
\qquad
\ianc{}{\stepsJ{\Bind{\ep}{v}{e}}{e}}{[BindEmpty]}

\vsk
\ianc{}{\stepsJ{\Bind{\WildPat}{v}{e}}{e}}{[BindWild]}
\qquad
\ianc{}{\stepsJ{\Bind{\VarPat{x}{\tau}}{v}{e}}{[v/x]e}}{[BindVar]}
\vsk
%\ianc{}{\Bind{p_1}{v_1}{\Bind{p_2}{v_2}{e}}
%{\stepsJ{\Bind{\Pair{p_1}{p_2}}{\Pair{v_1}{v_2}}{e}}}{[BindPair]} 
\ianc{}{\stepsJ{\Bind{\Pair{p_1}{p_2}}{\Pair{v_1}{v_2}}{e}}
        {\Bind{p_1}{v_1}{(\Bind{p_2}{v_2}{e})}}}{[BindPair]}
\end{array}
\]


\section{Sum Types}
\label{ssec:sum}
Think of \emph{sum} types as (non-recursive) ML datatype; for now we
will restrict only to \emph{binary datatypes} with fixed constructors
$\inlt e$ and $\inrt e$ (pronounced ``inleft'' and ``inright'') as the
datatype constructors.  We annotate those constructors with
the type they are injecting in to retain uniqueness of typing.  For type
destructor, we use a \mathcd{case} expression for sums.

\[
\begin{array}{rrcl}
\mathit{Types} & \tau &  \bnfas &\dots\bnfalt\tau_1 + \tau_2\\
\mathit{Expressions}& e & \bnfas & \dots\bnfalt \inlt e
\bnfalt \inrt e\bnfalt \caset\\
\mathit{Values} & v &\bnfas & \dots \bnfalt \inlt v\bnfalt\inrt v
\end{array}
\]

For example:
\beq
bool & = & \unit + \unit\\
True & = & \inl{\unit+\unit}\ep\\
False & = & \inr{\unit+\unit}\ep\\
If\ e\ Then\ e_1\ Else\  e_1 & = &\CaseT{e}{\ep}{\unit}{e_1}{\ep}{\unit}{e_2}
\eneq
Type rules:
\[
\begin{array}{c}
\ianc{\GG\vd e\hastype \tau_1}{\GG\vd\inlt e\hastype
  \tau_1+\tau_2}{[InlType]}\qquad
\ianc{\GG\vd e\hastype \tau_2}{\GG\vd\inrt e\hastype
  \tau_1+\tau_2}{[InrType]}
\vsk
\ianc{\GG\vd e\hastype \tau_1+\tau_2\qquad
\GG[x_1\oftp \tau_1]\vd e_1\hastype \tau_1\qquad
\GG[x_2\oftp \tau_2]\vd e_2\hastype \tau_2}{\GG\vd\caset\hastype\tau_1+\tau_2}{[CaseTyp]}
\end{array}\]

Evaluation rules:
\[\begin{array}{c}
\ianc{ e\mapsto e'}{\inlt e\mapsto \inlt e'}{[Inl]}
\qquad
\ianc{ e\mapsto e'}{\inrt e\mapsto \inrt e'}{[InR]}
\vsk
\ianc{}{\stepsJ{\CaseT{\inl{\tau_2}{v}}{x_1}{\tau_1+\tau_2}
{e_1}{x_2}{\tau_2}{e_2}}{[v/x_1]e_1}}{[CaseLeft]}
\vsk
\ianc{}{\CaseT{\inr{\tau_1+\tau_2}{v}}{x_1}{\tau_1}{e_1}{x_2}
{\tau_2}{e_2}\mapsto [v/x_2]e_2}{[CaseRight]}
\vsk
\ianc{e\mapsto e'}{\stepsbrJ{\CaseT{e}{x_1}{\tau_1}{e_1}{x_2}
{\tau_2}{e_2}}{\CaseT{e'}{x_1}{\tau_1}{e_1}{x_2}{\tau_2}{e_2}}}{[CaseTest]}
\end{array}\]

\section{Recursive Types}
\label{ssec:rec}

\textbf{Extra Credit.}
We have seen as \emph{sum} types can be used to define finitary data
types, as booleans, but we lack the ability to introduce types as
integers which are typically infinite. One way is to introduce
\emph{recursive} types. Recall that $\unit + \unit$ is isomorphic to the type 
of 
the boolean; similarly a finite type with $n$ values is isomorphic
to:
$$\underbrace{\unit+\dots+\unit}_{n \mbox{ times}}$$
  By analogy the
  natural numbers would be an infinite sum: this can be expresses by
  the recursive type $\mua{\unit + \alpha}$. 
%Its meaning should be
%  invariant under unrolling of recursion:

%\beq 
%nat & = & \nat\\
%& = & [(\nat)/\alpha]\unit + \alpha\\
%& = & \unit +( \nat)\\
%& = & \unit + nat
%\eneq

Recursive types are built via type variables $\alpha$ and the $\mu$
operator; they are equipped with a constructor $\foldt$ and a destructor
$\unfold$.
For example:

%\begin{Example}
\beq 
Nat & = & \nat\\
Zero & = & \fold^{Nat}(\inl{\unit+Nat} \ep)\\
One  & = & \fold^{Nat}(\fold^{Nat}(\inr{\unit+Nat)}(\inl{\unit+Nat} \ep)))\\
Succ & = & \fun{succ}{(x\hastype Nat)\hastype
  Nat}{(\fold^{Nat}(\inr{\unit+Nat}  x))}\\
Pred & = &\fun{pr}{(x\hastype Nat)\hastype Nat}{
\textbf{case } \unfoldn x \textbf{ of } Zero\Rightarrow Zero\mid Succ(y)\Rightarrow y}
%Plus & = & \fun{plus}{(\pair{x,y}\hastype Nat*Nat)\hastype Nat}
%\case{\unfold x}{\inl{}\ep}{Zero}{\inr{} w  }{\apply(Succ,\apply(Plus,\pair{w,y}))}
\eneq

You can think of $\fold$ as a map (a `predecessor' pointer) $Nat\Leftarrow
\unit + Nat$, while $\unfoldn$ is its inverse $Nat\Rightarrow \unit+Nat$.

\[
\begin{array}{rrcl}
\mathit{Types} & \tau &  \bnfas &\dots\bnfalt\alpha\bnfalt\mua{\tau}\\
\mathit{Expressions}& e & \bnfas & \dots\bnfalt \fold^{\mua {\tau}} e
\bnfalt \unfold e\\
\mathit{Values} & v &\bnfas & \dots \bnfalt \foldt v
\end{array}
\]

Typing rules:
\beq
\ianc{\GG\vd e\hastype [\mua \tau/ \alpha]\tau}{\GG\vd\fold^{\mua{\tau}}
  e\hastype \mua{\tau}}{[FoldTyp]}\qquad
\ianc{\GG\vd e\hastype \mua{\tau}}{\GG\vd\unfold
  e\hastype [\mua{\tau}/\alpha]\tau}{[UnfoldTyp]}
\eneq
%\end{document}

Evaluation rules:
\[\begin{array}{c}
\ianc{}{\unfold(\fold^{\mua{\tau}} e)  \mapsto e}{[FoldBeta]}\vsk
\ianc{e\mapsto e'}{\foldt e\mapsto e'}{[FoldTest]}\qquad
\ianc{e\mapsto e'}{\unfold e\mapsto e'}{[UnfoldTest]}
\end{array}\]

Another example is lists of natural numbers:
\beq
List & = & \mua{\unit+(nat*\alpha)}\\
Nil & = & \fold^{List}(\inl{\unit+List} \ep)\\
Cons & = & \fun{cons}{(x\hastype nat*List)\hastype
  List}{(\fold^{List}(\inr{\unit+List}  x))}\\
\eneq

Thus $Cons$ takes a number and a list and return the list with the
number as its head. To check your understanding, give a typing
derivation for $Cons(\pair{Zero,\pair{One,Nil}})$. Next define a
function \texttt{length} with tale a list and return its length via
\textbf{case} and $\unfold$.


\section{Implementation}

What you hand in: files \texttt{typed.sml}, \texttt{eval.sml} and
\texttt{parse.sml}.

\subsection{Parsing}
The parser is already provided in \texttt{parse.sml}; to check
 your understanding, you are asked to add
rules for the empty pair and only if you choose so for recursive types.


\subsection{Typing}

File \texttt{typing-sig.sml}  contains the signature, while 
\texttt{typing.sml} will contain the structure. You
 are given a \texttt{datatype pat =\dots}.  You need to define a
 function for pattern matching:
\texttt{match : env*pat*typ -> env}

\subsection{Evaluation} As in the previous assignment.

\subsection{Recursive types--extra credit} 
You also need to update the parser to allow
 recursive types and related constructor. You'll need
  a way to create fresh type variable:

\begin{verbatim}
 (* creates a fresh type variable *)
  val fresh_tyvar : unit -> tyvar
  (* resets the type variable generator *)
  val reset_tyvar : unit -> unit
  (* converts a type variable to a string *)
  val tyvar2string : tyvar -> string
\end{verbatim}
 An implementation is in \texttt{minml.sml}. 
You also need to provide a substitution function for \emph{types}, say 
\texttt{tsubst sub*typ -> typ}. 
\end{document}