\documentclass[10pt]{article}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{ttquot}
\usepackage{611}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% CS611: Please fill in these macros as appropriate:
\newcommand{\homework}{6}      %%% Replace ? by homework number
\newcommand{\due}{December 7, 2001}    %%% Replace ??/??/?? by MM/DD/YY format
                               %%% due date
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\imp}{\Rightarrow}
\newcommand{\andd}{\wedge}
\newcommand{\orr}{\vee}
\newcommand{\ptj}[4]{\Delta#1;\Gamma#2 \vdash #3 : #4}
\newcommand{\pj}[2]{\Delta#1 \vdash #2}
\newcommand{\epack}[3]{"pack"~[#1=#2,#3]}
\newcommand{\eunpack}[4]{"unpack"~#1~"as"~[#2,#3]~"in"~#4}
\newcommand{\efold}[2]{"fold"_{#1}~#2}
\newcommand{\eunfold}[1]{"unfold"~#1}
\newcommand{\eLam}[2]{\Lambda #1.~#2}
\newcommand{\elam}[3]{\lambda #1:#2.~#3}
\newcommand{\eApp}[2]{#1~[#2]}
\newcommand{\eapp}[2]{#1~#2}
\newcommand{\FTV}[1]{\nm{FTV}\SB{#1}}
\newcommand{\FV}[1]{\nm{FV}\SB{#1}}
\newcommand{\DE}[1]{{\cal E}\SB{#1}}
\newcommand{\DEsum}[1]{{\cal E^{+}}\SB{#1}}
\newcommand{\DEprod}[1]{{\cal E^{*}}\SB{#1}}
\newcommand{\DD}[1]{{\cal D}\SB{#1}}
\newcommand{\DG}[1]{{\cal G}\SB{#1}}
\newcommand{\DGsum}[1]{{\cal G^{+}}\SB{#1}}
\newcommand{\DGprod}[1]{{\cal G^{*}}\SB{#1}}
\newcommand{\DT}[1]{{\cal T}\SB{#1}}
\newcommand{\DTsum}[1]{{\cal T^{+}}\SB{#1}}
\newcommand{\DTprod}[1]{{\cal T^{*}}\SB{#1}}
\newcommand{\DTt}[1]{{\cal T}_\tau\SB{#1}}
\newcommand{\DTs}[1]{{\cal T}_\sigma\SB{#1}}

\begin{document}
\hwheader

\section*{What to turn in}

Turn in the assignment during class on the due date.

\begin{enumerate}

\item "Strong normalization" (25 pts.)

\begin{enumerate}

\item (20 pts.)
Show that all expressions in the language $\lambda^{\to\times+}$
are strongly normalizing by extending the proof
of strong normalization for $\lambda^{\to}$.

\item (5 pts.)
Where does the proof fail if we add recursive types to the language?

\end{enumerate}


\item "Object encodings" (35 pts.)

In this problem we will examine two ways to encode object types.  These
formulations give some insight into sound subtyping rules for object types in
object-oriented languages.  Let us consider the typed lambda calculus extended
with pairs, records, recursive types, existential types, and subtyping:
\begin{align*}
e & ::= b \mid x \mid \lambda x : \tau . e \mid e_0~e_1 \mid
	<e_0,e_1> \mid "left"~e \mid "right"~e \mid
	\{ l_1 = e_1, \ldots, l_n = e_n \} \mid e.l \mid \\
  & \quad~~\, \epack{X}{\tau}{e} \mid \eunpack e X x {e'} \mid
	\efold{\mu X.\tau}{e} \mid \eunfold{e} \\
\tau & ::= B \mid X \mid \tau \to \tau' \mid \tau * \tau' \mid
	\{ l_1 : \tau_1, \ldots, l_n : \tau_n \} \mid \mu X.\tau \mid \exists X. \tau
\end{align*}
We define a context $\Delta$ to contain the type variables in scope:
\[
	\Delta ::= \emptyset \mid \Delta, X
\]
and augment this definition with the usual rules about the irrelevance of
ordering type variables in $\Delta$.
A judgment of the form $\Delta \vdash \tau$ asserts that $\tau$ is
well-formed in $\Delta$.  Thus, we have:
\[
	\infer{\Delta \vdash B}{}
	\qquad
	\infer{\Delta,X \vdash X}{}
	\qquad
	\infer{\Delta \vdash \tau \to \tau'}
	      {\Delta \vdash \tau & \Delta \vdash \tau'}
	\qquad
	\infer{\Delta \vdash \tau * \tau'}
	      {\Delta \vdash \tau & \Delta \vdash \tau'}
\]
\smallskip
\[
	\infer{\Delta \vdash \{ l_1 : \tau_1, \ldots, l_n : \tau_n \} }
	      {\Delta \vdash \tau_i^{\forall i \in \{1,\ldots,n\}}}
	\qquad
	\infer{\Delta \vdash \mu X.\tau}
	      {\Delta, X \vdash \tau}
	\qquad
	\infer{\Delta \vdash \exists X.\tau}
	      {\Delta, X \vdash \tau}
\]

"Encoding as recursive records"

One way to model objects is as recursive record types of the form $\mu
X.\{l_1:\tau_1,\ldots,l_n:\tau_n\}$.
For instance:
\begin{align*}
"point" &= \mu P. \{x : "real", y : "real"\} \\
"mvpoint" &= \mu Q. \{x : "real", y : "real", \mathit{move} : "real" \to "real" \to Q\}
\end{align*}
To construct a "point" object we might write the function:
\[
"make_point" =
	\lambda a : "real".~
	\lambda b : "real".~
	\efold{"point"}{\{x = a, y = b\}}
\]
The rules for subtyping in this language can be obtained by modifying the rules
given in class for type equivalence in the typed lambda calculus extended with
recursive types.  As with type equivalence, we define a context $E$ containing
a set of assumed subtype relations $\tau_1 \leq \tau_2$, and use the following
rule to terminate the unfolding of recursive types:
\[
\infer{\Delta; E, \tau_1 \leq \tau_2 \vdash \tau_1 \leq \tau_2}
      {}
	%{\Delta \vdash \tau_1 & \Delta \vdash \tau_2}
\]
Recall the subtyping rules for function types, pairs, and records:
\[
\infer{\Delta; E \vdash \tau_1 \to \tau_2 \leq \tau_1' \to \tau_2'}
      {\Delta; E \vdash \tau_1' \leq \tau_1 &
       \Delta; E \vdash \tau_2 \leq \tau_2'}
\qquad
\infer{\Delta; E \vdash \tau_1 * \tau_2 \leq \tau_1' * \tau_2'}
      {\Delta; E \vdash \tau_1 \leq \tau_1' &
       \Delta; E \vdash \tau_2 \leq \tau_2'}
\]
\smallskip
\[
\infer[\mbox{where } m \ge n]
      {\Delta; E \vdash \{ l_1 : \tau_1, \ldots, l_m : \tau_m \}
		   \leq \{ l_1 : \tau_1', \ldots, l_n : \tau_n' \}}
      {\Delta; E \vdash \tau_i \leq \tau_i'~^{\forall i \in \{1,\ldots, n\}}}
\]

\begin{enumerate}

\item (5 pts.) Give the inference rules defining the subtype judgments
$\Delta;E\vdash\mu X.\tau \leq \tau'$ and $\Delta;E\vdash\tau' \leq \mu X.\tau$,
where $\tau'$ does not have the form $\mu Y.\tau''$.

\item (5 pts.) Give the inference rule defining the subtype judgment
$\Delta;E\vdash\mu X.\tau \leq \mu Y.\tau'$.

\item (5 pts.) According to the rules you have given, we should have
$"mvpoint"\leq"point"$. Say whether each of the following putative
subtype relationships also holds. If the relationship holds, give a
subtype derivation (proof tree). If it does not hold, give a counter-example:
code demonstrating that the subtype relationship would be unsafe.

\begin{enumerate}
\item 
$\mu P.\{x: P\} \leq \mu Q.\{x: Q\}$
\item
$\mu P.\{mv: "int"\to P, y: "int"\} \leq \mu Q.\{mv: "int"\to Q\}$
\item
$\mu P.\{eq: P\to "bool", y: "int"\} \leq \mu Q.\{eq: Q\to "bool"\}$
\item
$\mu P.\{a: "ref"~P, y: "int"\} \leq \mu Q.\{a: "ref"~Q\}$\qquad
(Note that $"ref"~\tau\leq"ref"~\tau'$ iff $\tau\cong\tau'$).
\item
\label{tree-example}
$\mu P.\{l: P, r: P, v: "int"\} \leq \mu Q.\{l: Q, r: Q\}$
\end{enumerate}

\end{enumerate}

"Encoding as recursive records with existentials"

One problem with the recursive record encoding is that an object's
implementation is visible to its clients.  In languages such as Smalltalk,
Java, or C++, the implementation may be hidden by declaring some fields of the
object private; in fact, in Smalltalk, all class members are private and
clients can access the object only through its method interface.

To model this property, we hide the implementation of an object using
existential types.  We treat objects as a pair of a state, represented by the
type variable $X$, and a record of methods, each of which takes an argument of
type $X$.  This argument can be considered analogous to "this" in Java
or C++ or "self" in Smalltalk.  As an example, we might encode the "point"
type above as
\[
"point" = \mu P.~\exists X.X * \{x : X \to "real", y : X \to "real" \}
\]
Note that we are no longer constrained to implement a "point" as a record of
two "real"s with named $x$ and $y$.  For instance, we might implement a
"point" as a pair using polar coordinates and define the following function to
create a new "point" from its Cartesian coordinates:
\begin{align*}
"make_point" &= \lambda a : "real".~\lambda b : "real".~ \\
    & \qquad \qquad "letrec"~m : \{x : ("real" * "real") \to "real", y : ("real" * "real") \to "real" \} = \{ \\
    & \qquad \qquad \qquad 
	  x = \lambda s : ("real" * "real").~
			("left"~s)*"cos"("right"~s), \\
      & \qquad \qquad \qquad 
	  y = \lambda s : ("real" * "real").~
			("left"~s)*"sin"("right"~s) \}~"in" \\
    & \qquad \qquad "let"~r = "sqrt"(a*a+b*b)~"in"~ \\
    & \qquad \qquad "let"~\theta = "arcsin"(b/r)~"in"~ \\
	& \qquad \qquad
	\efold{"point"}{(\epack{X}{"real" * "real"}{<<r, \theta>, m>})}
\end{align*}

Now, to call the method $x$ on a point $p$, we do:
\begin{align*}
& \eunpack {(\eunfold p)} X o { \\
& \qquad "let"~s:X = ("left"~o)~"in" \\
& \qquad "let"~m:\{x : X \to "real", y : X \to "real"\} = ("right"~o)~"in" \\
& \qquad (m.x~s)}
\end{align*}
Observe that the caller does not know the implementation of the state $X$.

\begin{enumerate}
\setcounter{enumii}{3}

\item (3 pts.) Using this encoding, what is the type encoding of "mvpoint"?

\item (5 pts.) Define a function "make_mvpoint" which, given two "real"s,
returns a new "mvpoint" representing that point.
The $\mathit{move}$ method should take two
real numbers $\mathit{dx}$ and $\mathit{dy}$ and return a new
"mvpoint" where the $x$ and $y$ coordinates of the original point
are offset by $\mathit{dx}$ and $\mathit{dy}$, respectively.
You are free to implement an "mvpoint"'s state in any way you choose.

\item (10 pts.) Give the inference rule defining the subtype judgment
$\Delta; E \vdash \exists X.\tau \leq \exists X.\tau'$.
The rule should not require that the types be
equivalent; however, if the subtype relation holds in both directions,
the rule should enforce equivalence of the two types.

\item (2 pts.) Show that $\emptyset; \emptyset \vdash "mvpoint" \leq "point"$.

\end{enumerate}

\item "Encoding sum and product types in the polymorphic lambda calculus"
(40 pts.)

Sum types and product types, as seen in $\lambda^{\to\times+}$, are
important features in programming languages.  In this problem, we will
show that by using some insights from the Curry-Howard isomorphism,
sum types in $\lambda^{\to\times+}$ can be encoded using product types
and universal types in the polymorphic lambda
calculus.  Similarly, we can encode product types as sum types.

Our source language will consist of the simply typed language extended with sum
and product types.
\begin{align*}
\tau & ::= B \mid \tau_1 \to \tau_2  
	\mid \tau_1 + \tau_2 \mid \tau_1 * \tau_2\\
e & ::= b \mid x \mid \lam{x\ty\tau}{e} \mid e_1~e_2 \mid
	 "inl"_{\tau_1 + \tau_2} e 
	\mid "inr"_{\tau_1 + \tau_2} e
	\mid "case"~e_0~"of"~e_1|e_2
	\mid <e_1, e_2> \mid "left"~e \mid "right"~e
\end{align*}

The typing rules for this language are the same as defined in lecture 30.

The target-sum language is the polymorphic lambda calculus extended
with only sum types.
\begin{align*}
\tau & ::= B \mid X \mid \tau_1 \to \tau_2 \mid
	\forall X. \tau \mid \tau_1 + \tau_2\\
e & ::= b \mid x \mid \lam{x\ty\tau}e \mid e_1~e_2 \mid
    \Lambda X.e \mid e[\tau] \mid "inl"_{\tau_1 + \tau_2} e 
	\mid "inr"_{\tau_1 + \tau_2} e
	\mid "case"~e_0~"of"~e_1|e_2
\end{align*}

The target-product language is the polymorphic lambda calculus extended
with only product types.
\begin{align*}
\tau & ::= B \mid X \mid \tau_1 \to \tau_2 \mid
	\forall X. \tau \mid \tau_1 * \tau_2\\
e & ::= b \mid x \mid \lam{x\ty\tau}e \mid e_1~e_2 \mid
    \Lambda X.e \mid e[\tau] \mid <e_1, e_2> \mid "left"~e \mid "right"~e
\end{align*}

The target languages have the same typing rules as the source language,
extended with two rules for supporting polymorphism:
\begin{center}
\begin{tabular}{ccc}
\infer{\ptj{}{}{\Lambda X.e}{\forall X.\tau}}%
    {\ptj{,X}{}{e}{\tau} & X\notin\Delta} & &
\infer{\ptj{}{}{e[\tau']}{\tau\{\tau'/X\}}}%
    {\ptj{}{}{e}{\forall X.\tau} & \pj{}{\tau'}}\\
\end{tabular}
\end{center}

Note that the rule for type abstraction requires that the
new type variable $X$ be fresh, to prevent capture of type variables
appearing in $\Gamma$.

Both target languages have the usual
rules for well-formed type expressions:
\begin{center}
\begin{tabular}{ccccccc}
 \infer{\pj{,X}{X}}{} & & 
 \infer{\pj{}{B}}{} & & 
 \infer{\pj{}{\tau_1 \to \tau_2}}{\pj{}{\tau_1} & \pj{}{\tau_2}} \\
\\
\infer{\pj{}{\tau_1 * \tau_2}}{\pj{}{\tau_1} &
\pj{}{\tau_2}} & &
\infer{\pj{}{\tau_1 + \tau_2}}{\pj{}{\tau_1} &
\pj{}{\tau_2}} & &
\infer{\pj{}{\forall X. \tau}}{\pj{,X}{\tau}}
\end{tabular}
\end{center}

Your goal in this problem is to provide typed translations from the
source language to each of the two target languages, 
and to show that these translations work. 
Each typed translation will convert type judgments in the source
language into type judgments in the target language, in such a way that
a translated program will automatically have a target language
type derivation if its source had a type derivation in the source language.

The Curry-Howard isomorphism will assist you in constructing these
translations. We know that the type $\tau_1 + \tau_2$ corresponds to the
formula $T_1 \orr T_2$ and the type $\tau_1 * \tau_2$ corresponds
to the formula $T_1 \andd T_2$. From De Morgan's rules in classical logic,
we know that $T_1 \orr T_2 \equiv \neg (\neg T_1 \andd \neg T_2)$, and vice
versa.

To help you in your efforts, we have provided on the course web page an
interpreter for the polymorphic lambda calculus.  See the file "test.poly" for
example syntax.

\begin{enumerate}
\item (5 pts.)
As mentioned in class, 
types whose formulae contain negation can be generated by
using continuations, but our target language has no continuations. Give
a formula that is equivalent to $A \andd B$ but contains only
logical operators for which there is a target-sum language equivalent.
Give a formula that is equivalent to $A \orr B$ but contains only
logical operators for which there is a target-product language equivalent.

\item (5 pts.)
We translate a source language type $\tau$ into a target-sum language type
$\DTsum\tau$ and into a target-product language type $\DTprod\tau$. 
What logically equivalent target-sum language type should
$\DTsum\cdot$ map $\tau_1 * \tau_2$ to? 
What logically equivalent target-product language type should
$\DTprod\cdot$ map $\tau_1 + \tau_2$ to? 

\item (10 pts.) \label{sum}
In this part, you will define the important parts of a translation function
$\DEsum\cdot$, which when applied to a source language type judgment
$\ptj{}{}e\sigma$, produces a provable target-sum language 
type judgment $\Delta'; \Gamma'\vdash e' : \DTsum{\sigma}$. 
It will be useful to have a
semantic function $\DGsum\cdot$ that simply maps all the types of variables in
$\Gamma$ into the target language: $\DGsum\emptyset = \emptyset$,
$\DGsum{\Gamma, x\ty\sigma} = \DGsum\Gamma, x\ty{\cal T}\SB\sigma$.
\medskip

Complete the translation of type checking rules for 
$<e_1, e_2>$, $"left"~e$, and $"right"~e$ into
type checking rules for target-sum languages. You will need to
introduce new variables; add any premises needed to control the
selection of variable names.

\item (10 pts.) \label{prod}
Similarly, you can define $\DEprod\cdot$ (and $\DGprod\cdot$) to translate a
source language type judgment into a target-product language type judgment.

Complete the translation of type checking rules for $"inl"_{\tau_1+\tau_2} e$,
$"inr"_{\tau_1+\tau_2} e$, and $"case"~e_0~"of"~e_1|e_2$ into type checking
rules for target-product languages.

\item (10 pts.)
Show that the expressions that are your translations in 
\ref{sum} and \ref{prod} are well-formed.  For each translated expression,
give a type derivation in which the tops of the proof tree are either
axioms or are judgments that you are assured of having because the
source-language expression is well-formed.

\end{enumerate}

\end{enumerate}

\end{document}
