\documentclass{article}
\usepackage{latexsym}
\usepackage{lcom}
\usepackage{cdsty}
%\newcommand{\new}[2]{\mbox{\textbf{new} $#1$ \textbf{in} $#2$}}
%\newcommand{\try}[2]{\mbox{\textbf{try} $#1$ \textbf{ow} $#2$}}
%\newcommand{\test}[4]{\mbox{\textbf{test} $#1$ \textbf{is } $#2$
%    }\Rightarrow #3\mid \_ \Rightarrow #4 }
%x\newcommand{\rais}[1]{\mbox{\textbf{raise} $#1$ }}
\title{Section C: Informal Quiz}

\author{Alberto Momigliano}
\newcommand{\al}{\alpha}
\begin{document}
\pagestyle{plain}
\maketitle
\newcommand{\ift}[3]{\mbox{\textbf{if } ${#1}$ \textbf{then }${#2}$
    \textbf{else} $#3$}}
\newcommand{\apply}{\mbox{\textbf{apply}}}
\renewcommand{\PI}[1]{\forall #1\,.\,}
\section{Polymorphism}
Find expression $e$ and types $\tau_i$ such that the following are well-typed:
\ben
\item  $\vd e\hastype\PI{\alpha}(\al\Imp\al)\Imp(\al\Imp\al)$.
\vspace{3cm}
%Can you think of a different one?
%\vspace{2cm}
\item $\vd \lamb{x}{(\PI{\alpha}\al\Imp\al)}x[\tau_1]
  (x[\tau_2])\hastype \tau_3$.
\vspace{4cm}
\item $\vd \lamb{x}{(\PI{\alpha}\al\Imp\al)} (x[\tau_4])
\  x\hastype \tau_5$.
\vspace{4cm}
% \item Let $f$ be the following expression:
% $$\Lambda\al\,.\,\lamb{x}{\al}\Lambda\al\,.\,x\hastype\PI{\al}(\al\Imp\PI{\al}\al)
% $$
% Is it well-typed? Consider $(f\ [int])\  3\ [bool]$; what is its type and the result of
% its evaluation?
% \vspace{4cm}
\item Let $Id$ be the polymorphic identity function: evaluate
$$(\lamb{x}{(\PI{\alpha}\al\Imp\al)} (x[\PI{\alpha}\al\Imp\al]
\  x) Id $$
\vspace{3cm}
\item We can \emph{define} \texttt{Bool} as $\Lambda\al\,.\,
  \al\Imp(\al\Imp\al)$. Define the following constants:
\beq
True & = & \Lambda\al\,.\,\lamb{x}{\al}\lamb{y}{\al}x\\
False & = & \mbox{}\\
Not & = & \lamb{p}{Bool}\\
Cond & = & \lamb{t}{Bool}\lamb{e_1}{\tau}\lamb{e_2}{\tau}
\eneq
\enen

\end{document}