\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}
\defvariable{G}{\Gamma}
\defvariable{t}{\tau}
\defvariable{a}{\alpha}
\defvariable{b}{\beta}
\easynotation
\def\skp{\\[1ex]}

\begin{document}
  \title{Assignment 5: Universal, Existential, and Recursive Types}
  \author{15-312: Foundations of Programming Languages \\
    Kevin Watkins $\langle$kw@cmu.edu$\rangle$}
  \date{\begin{tabular}{l} Out: Tuesday, March 15, 2005 \\
    Due: Tuesday, March 22, 2005 (10:30 a.m.) \\
    \end{tabular}\\[1ex]
    50 points total
    }
  \maketitle

  \section{Encodings in System F}

  It turns out that (if we ignore side effects for a moment), there are
  encodings of all the type constructs we've seen so far in terms of
  just function (>->) and universal (>\forall) types.  This was first
  noticed by a logician, Jean-Yves Girard, in his 1972 Ph.D. thesis, where
  he proposed a pure language based on just these two type constructors,
  called System F.  (Actually, his thesis has many different variations in
  it, some of which have other type constructors, and the language
  wasn't originally called System F, although everyone calls it that
  now.)  Girard wanted to use his language to investigate certain
  questions in constructive logic, although he also pointed out that it
  could be thought of as a programming language.  Girard was the first
  to prove that every well-typed program in System F terminates.

  At nearly the same time, John Reynolds was investigating polymorphism
  in programming languages, and came up with a system identical to one
  of Girard's, which he published in 1974 in the paper ``Towards a theory
  of type structure.''  In that paper Reynolds also investigated data
  abstraction and showed how polymorphic types could be used to enforce it.

  The point of this question is to investigate some of these encodings
  of various type constructors in terms of functions and universal
  types.  For our purposes, ``System F'' will mean the fragment of
  MinML with just the following type constructors:
  >>{t ::= a | t1 -> t2 | \forall a. t}
  and without any side effects or recursive functions.  It turns out
  then that every well typed expression evaluates to a value in finitely many
  steps.

  \subsection{Encoding Pairs}

  Still working in System F, let's introduce the type >{t1 * t2} by
  \emph{defining} it to be
  >>{t1 * t2 = \forall a. (t1 -> t2 -> a) -> a}
  where >a is some type variable not free in >t1 or >t2 (to avoid
  capture).

  Think about what the values of type >{t1 * t2} could be.  Since
  it is a >\forall-type, a value of this type must have the form
  >{\Lambda a. e} where >e is an expression of type >{(t1 -> t2 -> a) -> a} for
  \emph{arbitrary} >a.  So the value of >e has to be a function
  >{\lambda x:(t1 -> t2 -> a). e'}, where >{e'} has type >a.  But the only
  way we have of making a value of type >a is by applying >x to a
  couple of arguments.  So the value of >{e'} must be of the form >{x@e1@e2}, where
  >e1 has type >t1 and >e2 has type >t2.  So inside any value of type
  >{t1 * t2} there will be embedded expressions of type >t1 and >t2, which
  is why it acts like a product type.

\kwd{mkpair}\kwd{fst}\kwd{snd}
  \begin{question}{1.1}\points{5}
  Write System F functions having the types
  >>\begin{array}{rcl}
    mkpair &:& \forall b1. \forall b2. b1 -> b2 -> b1 * b2 \\
    fst    &:& \forall b1. \forall b2. b1 * b2 -> b1 \\
    snd    &:& \forall b1. \forall b2. b1 * b2 -> b2 \\
  \end{array}
  that implement the basic operations on these encoded pairs.  The
  function >mkpair should take a value of type >b1 and a value of type >b2
  and return something in type >{b1 * b2} that acts like a pair.
  (Remember that >{b1 * b2} means the definition above!)
  The functions >fst and >snd should extract the components of a
  simulated pair.
  \end{question}

\kwd{unit}
  \begin{question}{1.2}\points{5}
  (a) We can make an analogy from pair types to unit types by thinking of
  pairs as the 2-ary and units as the 0-ary case of the same idea.
  Following this analogy, propose a definition for unit types
  >>{unit = ?} in System F.

  (b) Your encoding of the unit type should
  contain \emph{exactly} one System F value.  What is it?
  \end{question}

\kwd{pack}\kwd{unpack}\kwd{as}\kwd{in}
  \subsection{Encoding Existential Types}

  In lecture, we saw a similar encoding of existential types:
  >>{\exists a. t = \forall b. (\forall a. t -> b) -> b}
  where >b is some type variable not free in >t (to avoid capture).

  \begin{question}{1.3}\points{5}
    Figure out and describe how to translate the constructs
    >{pack~(t', e)~as~\exists a. t} and >{unpack~(\alpha, x)=e1~in~e2}
    from lecture into System F programs that have the same meaning,
    but use the \emph{definition} of >{\exists a. t} given above.
    That is, you should give definitions for >pack and >unpack that
    expand them into the constructs of System F. Your translation should
    have the property that if a >pack or >unpack is well-typed in MinML,
    its encoding into System F should be well-typed in System F and
    ``do the same thing''.
  \end{question}

  \subsection{A Mystery Encoding}

  Consider the following definition: >>{t1 \mathbin\heartsuit t2 = \forall a.
  (t1 -> a) -> (t2 -> a) -> a}
  where again >a is not free in >t1 or >t2.
  This is an encoding into System F of a very familiar type
  constructor from MinML.

  \begin{question}{1.4}\points{5}
    Which MinML type constructor is it?
    For all of the MinML expression constructs involving this type
    (there are three of them),
    give encodings into System F in the style of Question 1.1.
  \end{question}

\kwd{foo}\kwd{bar}
  \begin{question}{1.5}\extra
    Discover which MinML types are represented by the following System
    F types: >>{foo = \forall a. a} >>{t@bar = \forall a. t -> a}
  \end{question}

  \subsection{Simulation Theorem}

  Actually proving that the encoding of MinML constructs into System F
  works is a bit tricky.  For example, we might guess the following
  correctness theorem:

\def\rep#1{\ulcorner#1\urcorner}
  \begin{quote}
    Let >e be a MinML expression involving product types, and let
    >{\rep{e}} be its translation into System F.  Then if >{e |-> e'}
    in the M-machine for MinML, we have >{\rep{e} |-> \rep{e'}} in the
    M-machine for System F, where >{\rep{e'}} is the System F
    translation of >{e'}.
  \end{quote}

  \begin{question}{1.6}\points{5}
    Find a counterexample to the supposed theorem.
  \end{question}



  \section{Existential and Recursive Types}

  For this part of the assignment, we are going back to using MinML
  constructs and syntax, not System F.

  Consider the following SML datatype for bitstrings:
  \begin{quote}\tt
    datatype bits \verb+=+ Empty \verb+|+ Zero of bits \verb+|+ One of bits
  \end{quote}
  The idea is that a bitstring such as {\tt 1011} will be represented as
  {\tt One (Zero (One (One Empty)))} (so the representation is big-endian).

  \begin{question}{2.1}\points{5}
    Represent the {\tt bits} datatype in MinML as a recursive (>\mu) type.
  \end{question}

\kwd{or}\kwd{bits}\kwd{fail}
  \begin{question}{2.2}\points{5}
    Write a MinML function >{or : bits * bits -> bits} using your
    definition of >bits as a recursive type.  Your >or function should
    compute the bitwise OR of its two arguments; for example, the
    bitwise OR of {\tt 11000} and {\tt 01010} is {\tt 11010}.
    If the two arguments to >or do not have the same length, it should
    use MinML's >fail operation to raise an exception.
  \end{question}

  \begin{question}{2.3}\points{5}
    Now use MinML's existential type (>\exists) to represent the {\tt bits}
    datatype as an \emph{abstract} type, exposing just the three constructors
    and the destructor.  (The destructor is just an operation that lets you
    do case analysis on values of type >bits.)
  \end{question}

  \begin{question}{2.4}\points{10}
    Revise your >or function from Question 2.2 to work with the abstract
    type instead of operating on the recursive type directly.
  \end{question}

\end{document}
