
Consider the following term $t$ from the untyped
$\lambda$-calculus: 
$((\lambda x. \lambda y. y\, y) ((\lambda w. w\, w) (\lambda w. w\, w)))
(\lambda w. w) $

For each of call-by-name (CbN) and call-by-value (CbV), reduce $t$.
Either show the full reduction steps, or the partial reduction steps
that get you to a setting where further reduction would not terminate.

%%%%%

Here are the call-by-name reduction rules for pairs and 
projections. Give the call-by-value reductions rules for pairs
and projections (hint: there are more for CbV than for CbN). Explain
the differences.
\begin{mathpar}
  \inferrule
  { }
  { \mathrm{fst}\ (e_1, e_2) \to e_1 }
  \qquad
  \inferrule
  { }
  { \mathrm{snd}\ (e_1, e_2) \to e_2 }
\end{mathpar}

%%%%%

The following are rules for $\mathrm{and}$ that are not coherent with the CbV
evaluation of other features (such as pairs) with respect to CbV evaluation.
Fix them and explain your fixes.  Note that some rules might need to be added.
\begin{mathpar}
  \inferrule
  { e_1 \to e_1' }
  { \mathrm{and}\ e_1\ e_2 \to \mathrm{and}\ e_1'\ e_2 }
  \qquad
  \inferrule
  { }
  { \mathrm{and}\ e_1\ \mathrm{true} \to e_1}
  \qquad
  \inferrule
  { }
  { \mathrm{and}\ e_1\ \mathrm{false}\to \mathrm{false}}
\end{mathpar}

%%%%%

Give the function that \emph{Church encodes} a pair, i.e.
\begin{lstlisting}
data Pair a b = Pair a b
\end{lstlisting}

%%%%%

Give the function that \emph{Church encodes} the Either type, i.e.
\begin{lstlisting}
data Either a b = Left a | Right b
\end{lstlisting}

%%%%%

Give the function that \emph{Church encodes} a list, i.e.
\begin{lstlisting}
data List a = Nil | Cons a (List a)
\end{lstlisting}
Hint: it is a generalization of the Church encoding of the type of
natural numbers.

%%%%%

Give the function that \emph{Church encodes} a tree, i.e.
\begin{lstlisting}
data Tree a = Leaf a | Branch (Tree a) (Tree a)
\end{lstlisting}
Hint: it is a generalization of the Church encoding of the type of
natural numbers.

%%%%%

Give an example of an expression which evaluates fully under both
CbV and CbN but takes more reduction steps under \emph{call by value}.
Justify that your example is correct.

%%%%%

Give an example of an expression which evaluates fully under both
CbV and CbN but takes more reduction steps under \emph{call by name}.
Justify that your example is correct.

%%%%%

Give an example of an expression which evaluates for exactly $2$
steps under both CbV and CbN but then gets stuck.
Justify that your example is correct.
Bonus if the evaluations steps are different.

%%%%%

Explain why the Y combinator ($\lambda x. x\ x$), using CbN, does not lead to a
terminating evaluation.

%%%%%

For deep, shallow and tagless embeddings of DSLs, give (in point-form) the
key differences between them, and when each is appropriate to use.

%%%%%

What is the point of having an evaluation strategy?

%%%%%

What differentiates CbV and CbN? 

%%%%%

The ``fundamental ingredients'' of functional programs and logic programs
differ. Mathematically, what are these ingredients? In what situation do
they coincide?

%%%%%

Give a short explanation of how free and bound variables differ.

%%%%%

 When writing lambda terms for humans, we implicitly
use a particular convention with respect to bound variables. Explain that
convention. Show how that convention is also used in mathematics.

%%%%%

Assume that $a, b, c, d, e$ are variables and $\intT$ and $\boolT$ types.
\begin{enumerate}
\item unify $a \rightarrow \intT$ and $\boolT \rightarrow b$
\item unify $a \rightarrow a$ and $\boolT \rightarrow b$
\item explain why $a$ and $a \rightarrow a$ cannot be unified.
\item unify $a -> (a -> b)$ and $(c -> d) -> (b -> b)$.
\item unify $a -> a$ and $(b -> c) -> (d -> e)$ and $(d -> c) -> a$.
\end{enumerate}
Show your steps.

%%%%%
What constraints are generated by the following Haskell codes:
\begin{enumerate}
\item h f x = f x x
\item c f g = \x -> g (f x)
\item d f g = \x -> g x (f x)
\item l f = let g h x = h (h x) in g f
\item k x = x x
\end{enumerate}
Solve them, and show the resulting type and substitution, or show
that it can't be solved.
%%%%%

State the \emph{progress} and \emph{preservation} properties. In your
own words, explain what they mean.

%%%%%

Subtyping of function types illustrates both covariance and
contravariance - explain those terms.

%%%%%

Why are the semantics of if-then-else in a CbV language weird? Why is this
inevitable? Why are the semantics fine in CbN?

%%%%%

Why are the semantics of case-of (for sums) in a CbV language weird? Why is
this inevitable? Why are the semantics fine in CbN? Contrast this with
`either` in Haskell.

%%%%%

Subtyping of function types involves _contravariance_. Explain what that is
and give an example.

%%%%%
(Bonus) Given an example of the failure of \emph{preservation}. Define
everything you need to illustrate this.

%%%%%
Further bonus question could involve more subtle questions about
- subtyping+FJ 
- bad interactions between various features that we've defined separately
- showing the failure of typing of complex versions of 'fix'
