\documentclass{article}
\usepackage{fullpage}
\usepackage{mathpartir}

\newcommand \arr \rightarrow

\newcommand \bnfdef {\mathrel{::=}}
\newcommand \bnfalt {\mathrel{{|}}}

\newcommand \A {\alpha}
\newcommand \B {\beta}
\newcommand \T {\tau}
\newcommand \G {\Gamma}
\newcommand \D {\Delta}
\newcommand \C {\cdot}

\newcommand \lam[2] {\lambda{#1}.\ {#2}}

\newcommand \Ac{\mathsf{A}}
\newcommand \Bc{\mathsf{B}}

\newcommand \eval[4] {{#1};{#2}\rightarrow{#3};{#4}}
\newcommand \subst[3] {{#1}[{#2}/{#3}]}
\newcommand \tc[3]{{#1} \vdash {#2} : {#3}}
\newcommand \intty {\mathsf{int}}
\newcommand \fnty[2] {{#1}\rightarrow {#2}}
\newcommand \Lam[2] {\Lambda{#1}.\ {#2}}
\newcommand \letin[3] {\mathsf{let}\ {#1}={#2}\ \mathsf{in}\ {#3}}
\newcommand \tru {\mathsf{true}}
\newcommand \fls {\mathsf{false}}
\newcommand \ifelse[3] {\mathsf{if}\ {#1}\ \mathsf{then}\ {#2}\
  \mathsf{else}\ {#3}}

\newcommand \refty[1] {{#1}\ \mathsf{ref}}
\newcommand \Ref[1] {\mathsf{ref}\ {#1}}
\newcommand \boolty {\mathsf{bool}}

\newcommand \muty[2] {\mu{#1}.{#2}}
\newcommand \roll[2]   {\mathsf{roll}_{#2}\ {#1}}
\newcommand \unroll[1] {\mathsf{unroll}\ {#1}}
\newcommand \kc[2] {{#1}\vdash{#2}}
\newcommand \tcF[4]{{#1};{#2} \vdash {#3} : {#4}}

\parindent 0pt
\parskip 1.5ex

\begin{document}

\centerline{\textbf{\Large Graduate Programming Languages, Extra
    Homework Problems}}
\centerline{\textbf{\Large (These All Fit Between Assignments 3 and 5)}}

\medskip

%Last updated: Summer 2012

\medskip

Associated Caml files are in {\tt hw\_extra\_code.tar}.

\begin{enumerate}
  
\item (The CPS Transformation) Extend the CPS transformation from
  lecture 13 to include the translation for pairs and sums as
  introduced in lecture 11.

\bigskip

\item (Continuation-Passing Style) In this problem you will
  reimplement the large-step, environment-based interpreter and the
  type-checker from homework 3.  Your reimplementations should always
  use a constant amount of stack space regardless of how big a program
  they evaluate or type-check.  To do so, use the idiom of
  continuation passing.  Note that you are manually using
  continuation-passing style to implement the interpreter and
  type-checker; you are \emph{not} applying a CPS transformation to
  the program being type-checked and evaluated.
\begin{itemize}
\item In the provided code, complete the definition of {\tt
    problem2/interpret}, which should have type\\
  \verb|exp -> (exp * heap) option| where the result 
  \verb|Some (v,h)| carries the final value and heap and the result
  \verb|None| indicates a run-time error occurred.  Two cases of the
    tail-recursive helper function are provided to you.  This helper
    function should never raise an exception: it should return
    \verb|None| or invoke the continuation it is passed.  Hints:
\begin{itemize}
\item There is no reason to use the \verb|Some| constructor in this
  helper function.
\item It is probably easiest to copy parts of your solution to homework 3 and
  then modify them.
\end{itemize}
\item In the provided code, complete the definition of {\tt
    typecheck}, which should have type 
  \verb|exp -> typ option| where the result \verb|Some typ| carries
    the type of the entire program and \verb|None| indicates a
    type-error was found.  You need to define a helper function that,
    like the helper function in part (a), takes a function as an extra
    argument that serves as a continuation.
\end{itemize}

\bigskip

\item (Machines and Continuations) You are given an untyped
  lambda-calculus and part of a low-level abstract machine.  The
  machine uses explicit evaluation contexts and environments, much
  like the last and most efficient interpreter in lecture 14 ({\tt
    interp\_closure}).  The definition of syntax and contexts ({\tt
    problem3/ast.ml}) is somewhat different to support more easily the
  fact that, unlike in lecture, we have several types of values.
  \begin{enumerate}
  \item Complete the definition of {\tt Main.interp} to support pairs,
    conditionals, and first-class continuations.  You must maintain
    tail-recursion.  Note the kinds of contexts you need are already
    defined for you in {\tt ast.ml}, along with comments about their
    purpose.  You can do continuations last; the provided testing
    program ({\tt adder}) doesn't use them.
 \item Change \texttt{Main.allow\_halt} such that:
  \begin{itemize}
  \item It takes an expression $e$ and returns an expression $e'$.
  \item $e$ can have free occurrences of the variable \verb|halt| and
  call it as a \emph{function} taking one argument, i.e., \verb|halt| $e''$.
  \item If $e$ evaluates to $v$ without ever calling \verb|halt|, then
  $e'$ evaluates to $(\mathsf{true},v)$.
  \item If $e$ evaluates after some number of steps to $E[$\verb|halt|
  $v]$, then $e'$ evaluates to $(\mathsf{false},v)$.
  \item $e'$ contains $e$ as a subexpression -- that is, do not
  examine $e$, just wrap it with some outer code.
  \end{itemize}
  Sample solution is 3 lines.  Advice: Work out your solution on paper first.
  Put $e$ in a function that takes
  \verb|halt| as an argument.  Pass this function a function that
  contains a $\mathsf{throw}$.  
  \end{enumerate}

\bigskip

\item (Sums and Subtyping) Consider a typed $\lambda$-calculus with a
  more flexible version of sum types than considered in lecture:
  \begin{itemize}
  \item There are an infinite number of constructors, not just $\Ac$
    and $\Bc$.  Let $C$ range over constructors. So an example
    expression is $C_7\ (\lam{x}{x})$.
  \item A single sum type $+\{C_1{:}\T_1,\dots,C_n{:}\T_n\}$ can list any
  finite number of constructors and the types of the values they carry.
  So one example type would be $+\{C_3{:}\intty,
  C_7{:}\fnty{\intty}{\intty}, C_2{:}\intty\}$.  Like in Caml, the
  order of constructors is not significant.  Unlike in Caml,
  we are using structural typing and different types can use the
  same constructors (with possibly different types they carry).
  \item As you should expect, a match expression can have any finite
  number of branches, with a different constructor for each branch.
  Informally (it can be formalized), a match expression has type $\T$
  if (1) the matched expression has type
  $+\{C_1{:}\T_1,\dots,C_n{:}\T_n\}$, (2) for each $C_i$ in the type there is a
  branch of the form $C_i\ x_i \rightarrow e_i$ where $e_i$ has type
  $\T$ assuming $x_i$ has type $\T_i$.
  \item The typing rule for constructor expressions can just be:
    \[\infer{\tc{\G}{e}{\T}}{\tc{\G}{C\ e}{+\{C\ \T\}}}\]
    If that seems odd, read on.
  \end{itemize}
  
  Come up with three sound and generally useful \emph{subtyping rules}
  for these sum types and \emph{justify informally} why each rule is
  sound.  Write the rules formally.

  \textbf{Note:} We already have rules like reflexivity and
  transitivity.  Your rules should specifically deal with the new
  sum types.

\bigskip

\item (Recursive types) In this problem, we show that a typed
  lambda-calculus with recursive types and \emph{explicit roll and
    unroll coercions} is as powerful as the untyped lambda-calculus.
  We give this language the following syntax, operational semantics,
  and typing rules (where for the sake of part (c) we allow evaluation
  of the right side of an application even if the left side is not yet
  a value):
\[\begin{array}{rcl}
\T &\bnfdef& \A \bnfalt \fnty{\T}{\T} \bnfalt \muty{\A}{\T} \\
e  &\bnfdef& x \bnfalt \lam{x{:}\T}{e} \bnfalt e\ e 
             \bnfalt \roll{e}{\muty{\A}{\T}} \bnfalt \unroll{e}\\
v  &\bnfdef& \lam{x{:}\T}{e} \bnfalt \roll{v}{\muty{\A}{\T}}
\end{array}\]
\begin{mathpar}
\infer{e\arr e'}
      {e\ e_2\arr e'\ e_2}
\and\infer{e\arr e'}
          {e_1\ e\arr e_1\ e'}
\and\infer{e\arr e'}
      {\roll{e}{\muty{\A}{\T}}\arr \roll{e'}{\muty{\A}{\T}}}
\and\infer{e\arr e'}
      {\unroll{e}\arr \unroll{e'}}
\\\infer{ }{(\lam{x}{e})\ v \arr \subst{e}{v}{x}}
\and\infer{ }{\unroll{(\roll{v}{\muty{\A}{\T}})}\arr v}
\\
\infer{ }{\tcF{\D}{\G}{x}{\G(x)}}
\and\infer{\tcF{\D}{\G,x{:}\T_1}{e}{\T_2}\\ \kc{\D}{\T_1}}
        {\tcF{\D}{\G}{\lam{x{:}\T_1}{e}}{\fnty{\T_1}{\T_2}}}
\and\infer{\tcF{\D}{\G}{e_1}{\fnty{\T_2}{\T_1}}\quad
       \tcF{\D}{\G}{e_2}{\T_2}}
     {\tcF{\D}{\G}{e_1\ e_2}{\T_1}}
\and\infer{\tcF{\D}{\G}{e}{\subst{\T}{(\muty{\A}{\T})}{\A}}}
      {\tcF{\D}{\G}{\roll{e}{\muty{\A}{\T}}}{\muty{\A}{\T}}}
\and\infer{\tcF{\D}{\G}{e}{\muty{\A}{\T}}}
           {\tcF{\D}{\G}{\unroll{e}}{\subst{\T}{(\muty{\A}{\T})}{\A}}}
\end{mathpar}

\newcommand \trans[1]{\mathit{trans}({#1})}
\begin{enumerate}
\item Define a translation from the pure, untyped, call-by-value
  lambda-calculus to the language above.  Naturally, your translation
  should preserve meaning (see part (c)) and produce well-typed terms
  (see part (b)).  Use $\trans{e}$ to mean the result of translating
  $e$.  You just need to write down how to translate variables,
  functions (notice the target language has explicit argument types),
  and applications.  The translation must insert roll and unroll
  coercions exactly where needed.  The key trick is to make sure every
  subexpression of $\trans{e}$ has type $\muty{\A}{\fnty{\A}{\A}}$.
\item Prove this theorem, which implies that if $e$ has no free
  variables, then $\trans{e}$ type-checks: If
  $\G(x)=\muty{\A}{\fnty{\A}{\A}}$ for all $x\in FV(\trans{e})$, then
  $\tcF{\C}{\G}{\trans{e}}{\muty{\A}{\fnty{\A}{\A}}}$.  (If the theorem is
  false, go back to part (a) and fix your translation.)
\item Prove this theorem, which, along with determinism of the target
  language (not proven, but true), implies that $\trans{e}$ preserves
  meaning: If $e\arr e'$ then $\trans{e}\arr^2\trans{e'}$ (notice the
  2!).  (If the theorem is false, go back to part (a) and fix your
  translation.)  Note: A correct proof will require you to state and
  prove an appropriate lemma about substitution.
\item Explain briefly why the theorem in part(c) is false if
we replace $\infer{e\arr e'}{e_1\ e\arr e_1\ e'}$ with 
$\infer{e\arr e'}{v\ e\arr v\ e'}$.
\end{enumerate}  

\bigskip

\item (Data Races) Consider these two code fragments in a
  shared-memory multithreaded language:\vspace{-0.5ex}
\begin{itemize}
\item \verb|while(f()) { y = (x+1)*g(); }| 
\item \verb|int t = x+1; while(f()) { y = t * g(); }|
\end{itemize}
Note that, like in C/C++/Java, the variable \verb|t| is thread-local.
Assume functions \verb|f| and \verb|g| are known to not read or write
global integers \verb|x| or \verb|y| (nor \verb|t|) and to not perform
any synchronization, but nothing else is known about them statically.
\begin{enumerate}
\item Sketch how, given an operational semantics for the
  language, you could prove that it would be meaning preserving to
  replace the first fragment with the second one \emph{if there is only
  one thread}.  
\item There are situations with multiple threads where replacing the
  first fragment with the second one introduces data races into a
  previously data-race-free program.  Fully
  describe such a situation.  (Therefore, in a language in which data
  races allow more behaviors, which might include ``catch-fire
  semantics,'' this transformation would be illegal.)  Note: A
  situation need not be something we expect programmers to do often.
\item Come up with a slightly more sophisticated transformation for
  the first fragment such that:
\begin{itemize}
\item If the original program has no data races, then neither will the
  transformed program.
\item It has the same single-threaded semantics.
\item Each time the transformed program fragment executes, \verb|x+1|
  is evaluated no more than once.
\end{itemize}
\end{enumerate}

\end{enumerate}

\end{document}