% -*- mode: LaTeX; compile-command: "mk" -*- \documentclass{tufte-handout} %include polycode.fmt %\arrayhs \usepackage{../../hshw} \usepackage{mathpartir} \title{\thecourse\ problem set 6} \date{\small Revision 1: compiled \today\ at \currenttime} \author{Due Tuesday, March 1} \begin{document} \maketitle \section{Rubric} \label{sec:rubric} For full credit, your solutions should demonstrate a proficient understanding of the following topics: \begin{itemize} \item Simply typed lambda calculus: 4 points \item $Y$ combinator: 4 points \item Type inference: 4 points \item Curry-Howard isomorphism: 4 points \end{itemize} An extra 4 points will be awarded for completeness. \section{The Simply-Typed Lambda Calculus} This section provides a reference for the simply-typed $\lambda$-calculus extended with product and sum types, as discussed in class. \subsection{Syntax} \label{sec:syntax} Types are denoted by the metavariables $\varphi$ or $\psi$\marginnote{or occasionally $\chi$ or whatever other lowercase Greek letter I feel like using} and are defined by the following recursive grammar: $\varphi,\psi ::= A \mid \varphi \to \psi \mid \varphi \times \psi \mid \varphi + \psi$ That is, a type is either a base type (denoted by a capital letter like $A$, $B$, \dots), a function type $\varphi \to \psi$, a product type $\varphi \times \psi$, or a sum type $\varphi + \psi$. \newcommand{\cons}[1]{\mathsf{#1}} \newcommand{\newcons}[1]{% \expandafter\providecommand\csname s#1\endcsname{}\expandafter\renewcommand\csname s#1\endcsname{\cons{#1}}} \newcons{fst} \newcons{snd} \newcons{left} \newcons{right} \newcons{case} \newcons{of} \newcommand{\lft}[1]{\app{\sleft}{#1}} \newcommand{\rgt}[1]{\app{\sright}{#1}} \newcommand{\fst}[1]{\app{\sfst}{#1}} \newcommand{\snd}[1]{\app{\ssnd}{#1}} \newcommand{\case}[5]{\scase\;#1\;\sof\;\{\lft #2 \to #3;\; \rgt #4 \to #5 \}} \newcommand{\tlam}[3]{\lam{#1\!:\!#2}{#3}} The syntax of terms is given by \begin{align*} t ::&= x \mid \tlam x \varphi t \mid \app{t_1}{t_2} \\ & \mid (t_1, t_2) \mid \fst t \mid \snd t \\ & \mid \lft t \mid \rgt t \mid \case t {x_1} {t_1} {x_2} {t_2} \end{align*} Formally, this syntax requires that the argument of a $\lambda$ must be annotated with a type ($\tlam x \varphi t$). However, we will sometimes omit the type annotation ($\lam x t$), either because the type can be easily understood from the context, or because it is up to you to deduce what its type annotation should be. \subsection{Typing} \label{sec:typing} The typing rules for this version of the simply-typed $\lambda$-calculus are shown below. \newcommand{\shows}{\vdash} \newcommand{\nrule}[3]{\inferrule{#2}{#3} \quad \text{#1}} \begin{mathpar} \nrule{Var (Ax)}{x : \varphi \in \Gamma}{\Gamma \shows x : \varphi} \\ \nrule{Lam ($\to$I)}{\Gamma, x : \varphi \shows t : \psi}{\Gamma \shows \tlam x \varphi t : \varphi \to \psi} \and \nrule{App ($\to$E)}{\Gamma \shows t_1 : \varphi \to \psi \and \Gamma \shows t_2 : \varphi}{\Gamma \shows \app{t_1}{t_2} : \psi} \\ \nrule{Pair ($\times$I)}{\Gamma \shows t_1 : \varphi \and \Gamma \shows t_2 : \psi}{\Gamma \shows (t_1, t_2) : \varphi \times \psi} \\ \nrule{Fst ($\times$E$_1$)}{\Gamma \shows t : \varphi \times \psi}{\Gamma \shows \fst t : \varphi} \and \nrule{Snd ($\times$E$_2$)}{\Gamma \shows t : \varphi \times \psi}{\Gamma \shows \snd t : \psi} \\ \nrule{Left ($+$I$_1$)}{\Gamma \shows t : \varphi}{\Gamma \shows \lft t : \varphi + \psi} \and \nrule{Right ($+$I$_2$)}{\Gamma \shows t : \psi}{\Gamma \shows \rgt t : \varphi + \psi} \\ \nrule{Case ($+$E)}{\Gamma \shows t : \varphi + \psi \and \Gamma, x_1 : \varphi \shows t_1 : \chi \and \Gamma, x_2 : \psi \shows t_2 : \chi}{\Gamma \shows \case t {x_1} {t_1} {x_2} {t_2} : \chi} \end{mathpar} \subsection{Reduction} \label{sec:reduction} Finally, the reduction rules are as follows: \newcommand{\red}{\rightsquigarrow} \newcommand{\subst}[3]{[#1 \mapsto #2]#3} \begin{mathpar} \nrule{$\beta$}{ }{\app {(\tlam x \varphi {t_1})}{t_2} \red \subst x {t_2}{t_1}} \\ \nrule{Cong-AppL}{t_1 \red t_1'}{\app{t_1}{t_2} \red \app{t_1'}{t_2}} \and \nrule{Cong-AppR}{t_2 \red t_2'}{\app{t_1}{t_2} \red \app{t_1}{t_2'}} \\ \nrule{$\beta$-Fst}{ }{\fst {(t_1, t_2)} \red t_1} \and \nrule{$\beta$-Snd}{ }{\snd {(t_1, t_2)} \red t_2} \\ \nrule{Cong-Fst}{t \red t'}{\fst t \red \fst {t'}} \and \nrule{Cong-Snd}{t \red t'}{\snd t \red \snd {t'}} \\ \nrule{$\beta$-CaseL}{ }{\case {(\lft t)} {x_1}{t_1}{x_2}{t_2} \red \subst {x_1} t {t_1}} \and \nrule{$\beta$-CaseR}{ }{\case {(\rgt t)} {x_1}{t_1}{x_2}{t_2} \red \subst {x_2} t {t_2}} \\ \nrule{Cong-Case}{t \red t'}{\case t {x_1}{t_1}{x_2}{t_2} \red \case {t'} {x_1}{t_1}{x_2}{t_2}} \end{mathpar} \exercise Give a formal typing derivation (\ie\ a proof tree) which assigns a type to the following term (note there are multiple correct answers): $\lam p {\case {(\fst p)} {x_1} {\rgt {x_1}} {x_2} {\app {x_2} {(\lam z z)}}}$ \exercise If $\Gamma \shows t : \varphi$ and $t \red t'$, will it always be the case that $\Gamma \shows t' : \varphi$ (for the \emph{same} type $\varphi$)? Explain how you would go about structuring a proof of this statement. Which parts are easy? Which parts would be more difficult? \exercise Recall that in the untyped $\lambda$-calculus, we can define the $Y$ combinator by $Y = \lam f {\app {(\lam x {\app f {(\app x x)}})} {(\lam x {\app f {(\app x x)}})}}.$ Explain why it is not possible\marginnote{\emph{Hint}: note that, as with anything defined inductively/recursively, infinite types are not allowed.} to give a type to $Y$ in the simply-typed $\lambda$-calculus. \exercise Of course, just showing that $Y$ does not have a type is not a proof that we have ruled out infinite recursion! Maybe there is some other tricky thing we can do that has a type but acts like $Y$. We would like to \emph{prove} that any well-typed term will only reduce for a finite number of steps. If a term $t$ does not reduce infinitely we say $t$ \term{terminates}. Otherwise we say $t$ \term{diverges}. \newcommand{\size}{\mathsf{size}} \newcommand{\N}{\mathbb{N}} One obvious approach would be to prove the following statement by (strong\footnote{The strong induction principle for natural numbers says that in order to prove that $P$ holds for all natural numbers, we must prove that $P$ holds for an arbitrary number $m$ under the assumption that $P$ holds for \emph{all} numbers $k < m$. Note this also means we must prove $P(0)$ without any assumptions, since there are no $k < 0$. This is equivalent in power to the usual induction principle for natural numbers, but often feels'' more powerful, since the inductive hypothesis lets you assume that $P$ holds for \emph{all} numbers smaller than $m$ instead of just the predecessor.}) induction on the size\footnote{The $\size$ of a $\lambda$-calculus term is defined as the number of constructors it contains, \ie\ each $\lambda$ contributes $1$ to the size, as does each application, pair, and so on. For example, $\size(\lam x {(\fst {(y,z)})}) = 5$.} of $\lambda$-calculus terms: $\forall n \in \N. \forall t. (\size(t) = n) \implies t\text{ terminates}.$ Unfortunately, this does not work. Explain why not. \newthought{This turns out to} actually be true, but proving it is nontrivial---much too nontrivial to include on this homework, but not so nontrivial that you would not be able to understand the proof. If you are interested, you can consult Chapter 12 of Pierce\cite[0.1in]{pierce2002types} (you are welcome to borrow my copy). \newcons{Y} \newcommand{\Y}[1]{\app \sY {#1}} Now that we have cut out unrestricted recursion, suppose we want to add it back in, but in a principled way.\footnote{Why would we go to all the trouble of getting rid of recursion if we are just going to add it back in again? Although adding $\sY$ gives us unrestricted recursion again, it's now easy to tell just by looking at a term whether it could possibly be infinitely recursive: just see whether it contains $\sY$ or not. If it doesn't, then it will definitely terminate. Also, as we discussed in class, there are many benefits to having a type system besides just getting rid of infinite recursion.} The idea is to explicitly add a new term constructor $\sY$ to the syntax of $\lambda$-calculus terms, \ie\ in addition to $\lambda$, application, \etc, a term $t$ can now also be of the form $\Y t'$ for some other term $t'$. Note that in contrast to the $Y$ from the untyped $\lambda$-calculus, which we just defined to be a certain $\lambda$-calculus term, this new $\sY$ is just a piece of syntax with no \emph{a priori} meaning. \exercise Write down a typing rule for $\Y t$, that is, a rule of the form \begin{mathpar} \inferrule{ \dots }{ \Gamma \shows \Y(t) : \dots } \end{mathpar} where you fill in the dots appropriately. (\emph{Hint}: think about the type of |fix| in Haskell.) \exercise Write down an appropriate reduction rule for $\Y$. \newthought{Consider the following} Haskell definitions: \begin{spec} data Ty where BaseTy :: String -> Ty Arr :: Ty -> Ty -> Ty deriving (Eq, Show) data Tm where Var :: String -> Tm Lam :: String -> Ty -> Tm -> Tm App :: Tm -> Tm -> Tm deriving Show \end{spec} |Ty| represents types of the STLC, and |Tm| represents terms. I have provided you with the file |STLC.hs|, which contains the above definitions along with utilities to parse and pretty-print terms and types (that is, convert between |String| representations and the above algebraic data types). \exercise Implement a function\marginnote{\emph{Hint}: you may find the |Data.Map| module useful.} $|inferType :: Tm -> Maybe Ty|$ which infers the type of a term. You can use the provided parsers and pretty-printers to test your function. For example, \begin{verbatim} ghci> let tm = readTmU "\\y:D -> A -> B. \\z:D. \\x:(A -> B) -> ((C -> D) -> E). x (y z)" ghci> fmap ppTy (inferType tm) Just "(D -> A -> B) -> D -> ((A -> B) -> (C -> D) -> E) -> (C -> D) -> E" ghci> fmap ppTy (inferType (readTmU "\\x:A. x x")) Nothing \end{verbatim} \section{The Curry-Howard isomorphism} \exercise Some of the following propositions are provable in propositional logic, and some are not. \begin{itemize} \item For those that are provable, demonstrate it \emph{by giving a term of the STLC with a corresponding type} (you need not give a formal typing derivation, though you may find it helpful to do so). Equivalently, you may write a Haskell function with a corresponding type, as long as you are careful not to use recursion or any other Haskell features which are not part of STLC. \item For those that are not provable, explain why not. \end{itemize} \begin{enumerate}[label=(\alph*)] \item $\varphi \implies \varphi$ \item $(\varphi \implies \varphi) \implies \varphi$ \item $((\varphi \implies \varphi) \implies \varphi) \implies \varphi$ \item $(\varphi \land (\psi \lor \chi)) \implies ((\varphi \land \psi) \lor (\varphi \land \chi))$\marginnote{D\'ej\`a vu?} \item $(\varphi \implies (\psi \land \chi)) \implies ((\varphi \implies \psi) \land (\varphi \implies \chi))$ \end{enumerate} % \exercise What sort of types correspond to the propositions $\top$ and % $\bot$? What terms might we add to STLC to represent evidence for % their introduction and elimination rules, respectively? \bibliographystyle{plainnat} \bibliography{STLC} \end{document}