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

\begin{document}
  \title{Assignment 7: Subtyping and Labeled Variants}
  \author{15-312: Foundations of Programming Languages \\
    Tom Murphy 7 \\
    Modified by Kevin Watkins $\langle$kw@cmu.edu$\rangle$}
  \date{\begin{tabular}{l} Out: Thursday, April 7, 2005 \\
    Due: Thursday, April 14, 2005 \\
    \qquad {\bf but} hand in Tuesday, April 19, 2005 (10:30 a.m.) \\
    \end{tabular}\\[1ex]
    50 points total
    }
  \maketitle

  In this assignment you will be asked to investigate several aspects of
  subtyping. For each question, assume that we are employing the subset
  interpretation of subtyping.

  This assignment is nominally due in one week, on April 14, but since
  there's no class meeting then (owing to Carnival), you will actually be
  handing it in on the following Tuesday, April 19, in lecture (and that's
  when the late clock starts).  Be advised, though, that Assignment 8
  goes out on April 14.

  \section{Width Subtyping for Products}

  We've seen already (in lecture) some subtyping rules for records, namely
  width, depth, and permutation subtyping.  Now products and records are
  rather similar; essentially the only difference is that the constituents
  of a record are labeled.  So we might imagine carrying over some of these
  rules for records to the case of products.  (In this assignment, all
  products are binary---they will have exactly two components.)

  It's clear that permutation
  makes no sense for products; the labels are needed there.  And we already
  have ``depth'' subtyping for products, given by the rule
  >>{\rul t1 <= s1 \quad t2 <= s2
     \over {t1 * t2 <= s1 * s2}}
  from lecture.

  But what about a ``width'' subtyping rule for products?  Such a rule
  might look like
  >>{\ax {t1 * t2 <= t1}}
  
  \begin{question}{1.1}\points{10}
    Why would adding this rule to MinML be a bad idea?  What key property
    of MinML's static and dynamic semantics would be violated?  (``Key
    properties'' might include: type safety, progress, preservation, canonical
    forms, or determinism.  Be as specific as you can.)  Show a MinML term that illustrates the problem.
  \end{question}

  \section{Labeled Variants}

\kwd{in}\kwd{case}\kwd{of}
  By adding labels to
  our \emph{products}, we arrived at the useful notion of \emph{records}.
  What if we add labels to \emph{sums}?  Then we get what are called
  \emph{labeled variants}.  A labeled variant is like a sum type, except
  that it can contain any number of options (not necessarily two), and
  each option is labeled.  The >in (injection) and >case constructs then
  refer to these labels rather than referring to the various options by
  number.

  The syntax is as follows:
  >>{\begin{array}{lrcl}
    \hbox{Types} & t & ::= & \cdots | [l1 : t1, ..., ln : tn] \\
    \hbox{Terms} & e & ::= & \cdots | in_{l}@e \\
    & & & \qquad | (case~e~of~in_{l1}@x1 => e1 | \cdots | in_{ln}@xn => en) \\
    \hbox{Values} & v & ::= & \cdots | in_{l}@v \\
  \end{array}}

\kwd{intlist}\kwd{int}\kwd{roll}\kwd{unroll}\kwd{fail}
\vname{nil}\vname{cons}\vname{hd}
  So for instance, we could write the type of integer lists as:
  >>{intlist = (\mu a. [nil : 1, cons : int * a]),}
  and the list >{[1,2]} would be coded as:
  >>{roll@(in_{cons}@(1, roll@(in_{cons}@(2, roll@(in_{nil}@()))))),}
  and the operation >{hd@x} to get the first element of a list could be
  coded as
  >>{hd@x = (case~unroll@x~of~in_{cons}@y => y.1 | in_{nil}@\_ => fail).}

  \begin{question}{2.1}\points{10}
    Come up with typing rules for >{in_{l}} and >case on labeled variants.
    Explain in words why your rules are correct.  (It might help to go back
    and look at the rules for sums, and use them as a model.)
  \end{question}

  \begin{question}{2.2}\points{10}
    Come up with subtyping rules for labeled variant types.  You should
    have rules \emph{analogous} to width, depth, and permutation subtyping for
    records.  (But the rules will not be exactly the same!)  Explain
    in words why your rules are correct.
  \end{question}

  Thinking about how to do the type safety proof for the language extended
  with labeled variants, it turns out that we need a major change to
  the \emph{canonical forms lemma}.  Usually, this lemma is extremely
  easy to prove; in fact, it's usually just a single inversion step.
  With subtyping, though, it turns out that an inductive argument is needed.

  \begin{question}{2.3}\points{20}
    State a canonical forms lemma for labeled variants with subtyping,
    and prove it.
  \end{question}

  \paragraph{Hints}
  If you find the proof difficult, it may be that your typing rules or
  subtyping rules---the answers to questions 2.1 and 2.2---are wrong.
  Consider this possibility if you run into trouble.  Also, it's likely
  you'll need an extra lemma (with its own induction) saying something
  about subtyping.  It'll probably be easier to try the canonical forms
  proof first, and in the process of working it out, you'll find out
  what the other lemma you'll need is.

\end{document}
