The exercises below can be done in any order, and you should try to complete the non-optional exercises if you can before the deadline. Sections containing mandatory exercises are indicated in blue, sections containing optional ones in red, and sections containing a mix of both in purple.
You should not use any external libraries, but it is okay to import functions from the standard library.
Download the template file Lab4.hs, put all your solutions in this file, and upload it to Moodle before the deadline. Make sure that you submit a working Haskell file!
This lab is about both untyped and simply-typed lambda calculus. In addition to reviewing the slides from Lecture 3, you may find it helpful to read parts of Peter Selinger’s lecture notes on the lambda calculus for background.
The aim of the first part of this lab is to get a better understanding of how type inference works in Haskell (and in similar languages like OCaml and SML), by considering a few examples of simple type inference for lambda terms. For reference, let’s recall the formal typing rules of simply-typed lambda calculus (STLC):
\[ \frac{x:A \in \Gamma}{\Gamma \vdash x:A}var \qquad \frac{\Gamma,x:A \vdash e : B}{\Gamma \vdash \lambda x.e : A \to B}lam \qquad \frac{\Gamma \vdash e_1 : A \to B \quad \Gamma \vdash e_2 : A}{\Gamma \vdash e_1\ e_2 : B}app \]
Remember that we write \(\Gamma \vdash e:B\) to indicate that an expression \(e\) with free variables \(x_1,\dots,x_n\) has type \(B\) in a typing context where its free variables are assigned types \(\Gamma = x_1:A_1,\dots,x_n:A_n\). For example, we can use these rules to derive that \(\vdash \lambda f.\lambda x. f\ x : (a \to a) \to (a \to a)\). Here is the explicit derivation tree:
\[ \frac{ \frac{ \frac{ \frac{\displaystyle f : a \to a \in f : a \to a,x : a}{\displaystyle f : a \to a,x : a \vdash f : a \to a}\qquad \frac{\displaystyle x:a \in f : a \to a,x : a}{\displaystyle f : a \to a,x : a \vdash x : a} } {\displaystyle f : a \to a,x : a \vdash f\ x : a}} {\displaystyle f : a \to a \vdash \lambda x. f\ x : a \to a}} {\displaystyle\lambda f.\lambda x. f\ x : (a \to a) \to (a \to a)} \]
An important property of simple typing is that if a term is typable then it has a “best” type, called its principal type. Formally, the principal type of a term is its most general type in the following sense: to check whether the term has any other type, it is necessary and sufficient to check whether that type is an instance of the principal type (under some substitution for type variables). For example, the term \(\lambda f.\lambda x. f\ x\) has principal type \((a \to b) \to (a \to b)\), and we can see that the typing above is recovered by substituting \(a\) for \(b\).
Let’s consider two more examples:
In both cases, we can get the GHC interpreter to quickly give us this information using the :t (a.k.a. :type) command:
*Main> :t \x y z -> x (y z)
\x y z -> x (y z) :: (t1 -> t2) -> (t3 -> t1) -> t3 -> t2
*Main> :t (\x -> x x) (\x -> x x)
<interactive>:1:22: error:
• Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
• In the first argument of ‘x’, namely ‘x’
In the expression: x x
In the first argument of ‘\ x -> x x’, namely ‘(\ x -> x x)’
• Relevant bindings include
x :: t0 -> t (bound at <interactive>:1:15)Let’s take a moment to understand the process that GHC goes through in order to compute these results.
Since \(\lambda xyz.x\ (y\ z)\) is a lambda abstraction, for it to be typed using the \(lam\) rule, it would need to have a type \(A\) of the form \(A = X_1 \to B\) where \(x:X_1 \vdash \lambda yz.x\ (y\ z) : B\). By the same argument repeated twice, \(B\) must be of the form \(B = X_2 \to (X_3 \to X_4)\) where \(x:X_1, y:X_2, z:X_3 \vdash x\ (y\ z) : X_4\). Now, since \(x\ (y\ z)\) is an application, and the variable \(x\) being applied is assumed to have type \(X_1\), to use the \(app\) rule we must have \(X_1 = X_5 \to X_4\) for some \(X_5\) with \(y\ z : X_5\). Repeating the argument, since the variable \(y\) being applied in \(y\ z\) is assumed to have type \(X_2\) while the argument \(z\) is assumed to have type \(X_3\), we must have \(X_2 = X_3 \to X_5\). Combining all of these constraints \[
A = X_1 \to B \qquad
B = X_2 \to X_3 \to X_4 \qquad
X_1 = X_5 \to X_4 \qquad
X_2 = X_3 \to X_5
\] and simplifying them, we derive that the most general type for \(\lambda xyz.x\ (y\ z)\) is \[
A = (X_5 \to X_4) \to (X_3 \to X_5) \to (X_3 \to X_4)
\] which indeed is equivalent up to renaming and parenthesization with \((b \to c) \to (a \to b) \to (a \to c)\) and (t1 -> t2) -> (t3 -> t1) -> t3 -> t2.
On the other hand, for \((\lambda x.x\ x)(\lambda x.x\ x)\) to be typed using the \(app\) rule, we need to first type the subexpression \(\lambda x.x\ x\). Since it is a lambda abstraction, we can try to assign it some type \(A \to B\) where \(x : A \vdash x\ x : B\). Now, the variable \(x\) is both the function and the argument of the application \(x\ x\). Since the argument is assumed to have type \(A\), for the result to have type \(B\) we need that \(A = A \to B\). But this equation is impossible to satisfy with finite types, and so the subexpression \(\lambda x.x\ x\) is not simply-typable, and hence neither is the larger expression \((\lambda x.x\ x)(\lambda x.x\ x)\).
For a more detailed description of a type inference algorithm for STLC, you can read Section 9 of Selinger’s notes, as well as the Wikipedia article on the Hindley-Milner type system.
For each of the untyped λ-expressions below, \[ e_1 = \lambda fx. x \quad e_2 = \lambda fx. f\ (f\ x) \quad e_3 = \lambda x.x\ (\lambda y.y) \] \[ e_4 = \lambda x y.x\ y\ y \quad e_5 = \lambda xy.x\ (y\ y) \quad e_6 = \lambda xy.x\ (y\ x) \] determine:
Whether it has a simple type, and
If so, determine its most general type.
You should try to do this first without asking the GHC interpreter, and then verify your answer using GHC. Record your answers as comments below. (You do not need to give a full derivation, but try to understand for yourself why the answer is what it is.)
Conversely, we can also consider the problem backwards, and starting from a type try to find a corresponding term with that type. Often, knowing that a function has a polymorphic type can tell you a lot about that function. For example, the only pure lambda term that can be assigned polymorphic type \(a \to a\) is the identity function \(\lambda x.x\). Although in Haskell the type \(a \to a\) also admits some other less savory inhabitants (such as the expression undefined), in general we can nevertheless learn a lot about a function just by looking at its type.
Come up with Haskell functions with the polymorphic types below. There may be more than one valid answer, but we do not accept undefined as an answer.
Is there a simply-typed λ-expression whose principal type is \((a \to a) \to a\)? Why or why not?
What about in Haskell? Is it possible to write a function in Haskell whose most general type is \((a \to a) \to a\), without using the expression undefined or throwing an exception? Show how, or explain why it is not possible.
The fact that the programmer can get away with placing very few type annotations in programming languages like Haskell and OCaml is both a benefit and a drawback. Besides being an important form of documentation, type annotations are one of the main mechanisms for a programmer to get across their intention to the programming environment, and in particular to allow the type checker to return better error messages when things go wrong.
Since pure type inference amounts to a global constraint solving problem, it can sometimes be difficult to localize the source of a type checking error. For example, consider the following code sample (adapted from the article Understanding beginners’ mistakes with Haskell), which was intended to define a recursive function multiplying the elements of a list:
When trying to load a file containing this definition, GHC returns the following somewhat inscrutable error message:
• Occurs check: cannot construct the infinite type:
t
~
[(Integer -> Integer -> Integer) -> t -> t0 -> Integer] -> Integer
• Relevant bindings include prod :: t (bound at Lab4Sols.hs:135:1)
|
135 | prod [] = 1
| ^^^^^^^^^^^...
Failed, no modules loaded.Notice that GHC complains about the first clause of the definition prod [] = 1, although the real source of the bug is the second clause prod (x:xs) = x (*) prod xs, where the programmer has written (*) instead of *. If we preface the definition by a type declaration:
then GHC produces a somewhat better error message (at least it correctly identifies the second clause),
• Occurs check: cannot construct the infinite type:
a
~
(Integer -> Integer -> Integer)
-> ([Integer] -> Integer) -> [a] -> a
• The function ‘x’ is applied to three arguments,
but its type ‘a’ has none
In the expression: x (*) prod xs
In an equation for ‘prod’: prod (x : xs) = x (*) prod xs
• Relevant bindings include
xs :: [a] (bound at Lab4Sols.hs:137:9)
x :: a (bound at Lab4Sols.hs:137:7)
prod :: [a] -> a (bound at Lab4Sols.hs:136:1)
|
137 | prod (x:xs) = x (*) prod xs
| ^^^^^^^^^^^^^although it might still take the programmer some time to understand how to fix the bug.
Here is another example of a slightly buggy function:
The programmer had in mind the slick definition of list reversal using fold-left (reverse = foldl (flip (:)) []), but used list concatenation (++) in place of the cons’ing operation (:). However, the type checker mislocates the error, complaining about the type of the argument s:
• Couldn't match type ‘Char’ with ‘[Char]’
Expected type: [[Char]]
Actual type: String
• In the third argument of ‘foldl’, namely ‘s’
In the expression: foldl (flip (++)) [] s
In an equation for ‘revString’:
revString s = foldl (flip (++)) [] s
|
2 | revString s = foldl (flip (++)) [] s
| ^The reason is because the type checker is able to satisfy all of the necessary constraints to find a principal type for the subexpression foldl (flip (++)) [], up until the point where it is applied to an argument of type String.
Much research has been carried out on the design of type systems to maximize expressivity and ease-of-use while still providing robust error messages, but it remains an open problem. In this exercise, we will explore another corner of the design space known as bidirectional typing, which in general requires more type annotations on the part of the programmer, but has the advantage of better localizing type errors.
To define a bidirectional type system for STLC, we begin by introducing a pair of checking and synthesis judgments that refine the basic typing judgment \(\Gamma \vdash e : A\) from above:
a checking judgment \(\Gamma \vdash e \Leftarrow A\), which given a typing context \(\Gamma\), a λ-expression \(e\), and a type \(A\), determines whether \(e\) has the type \(A\) in the typing context \(\Gamma\).
a synthesis judgment \(\Gamma \vdash e \Rightarrow A\), which given a typing context \(\Gamma\) and a λ-expression \(e\), returns the most general type \(A\) for \(e\) in the typing context \(\Gamma\), if it exists (i.e., if \(e\) is typable in \(\Gamma\)).
For each of the different kinds of λ-expressions we either have a checking rule or a synthesis rule,
\[ \frac{x:A \in \Gamma}{\Gamma \vdash x \Rightarrow A} \qquad \frac{\Gamma \vdash e_1 \Rightarrow A \to B \quad \Gamma \vdash e_2 \Leftarrow A}{\Gamma \vdash e_1\ e_2 \Rightarrow B} \qquad \frac{\Gamma,x:A \vdash e \Leftarrow B}{\Gamma \vdash \lambda x.e \Leftarrow A \to B} \] which can be read as follows:
We also need to include a rule for passing from synthesis to checking:
\[ \frac{\Gamma \vdash e\Rightarrow A \quad A = B}{\Gamma \vdash e \Leftarrow B} \]
In words, this says that to check \(e\) against a type \(B\) (in a given context Γ), we can try to synthesize a type \(A\) for \(e\) (in the same context) and check that \(A = B\).
Finally, we add a rule that allows to synthesize a type for a term with an explicit type annotation:
\[ \frac{\Gamma \vdash e\Leftarrow A}{\Gamma \vdash (e:A) \Rightarrow A}\qquad \]
An elegant property of the bidirectional type system is that such type annotations are only ever needed at β-redices.
The goal of this (optional) exercise will be to write a bidirectional type checker for STLC in Haskell. We are not going to implement any fancy parsing or pretty-printing, and instead just work with raw data types of types and expressions.
Let’s begin by introducing a data type of simple types:
A simple type (represented by a value of type Ty) is either a type variable (built using the constructor TV) or a function type (built using the constructor Fn). Note we make the choice to use integers to stand for the names of type variables.
Next we’ll introduce a data type of λ-expressions with embedded type annotations:
That is, an expression is either a variable (V), an application (A), a lambda abstraction (L), or a type annotation. Again we make the choice to use integers to stand for the names of (expression) variables.
For example, here is the representation of the expression \(\lambda xyz.x\ (y\ z)\):
and here is the representation of the annotated expression \((\lambda fx.f\ x : (a \to a) \to (a \to a))\ (\lambda x.x)\):
To define the checking and synthesis typing judgments, we’ll represent typing contexts as lists of pairs of an integer (denoting a variable name) together with a corresponding type. It is convenient to introduce a type synonym:
Finally, our goal is to define functions
satisfying the following specifications: check Γ e A should evaluate to True just in case \(\Gamma \vdash e \Leftarrow A\), and otherwise evaluate to False, while synth Γ e should evaluate to Just A just in case \(\Gamma \vdash e \Rightarrow A\), and otherwise evaluate to Nothing.
Based on the typing rules explained above, complete the definitions:
You will probably want to begin by pattern-matching…
Here are a few examples that you can use for testing, but you should also write your own tests!
> check [] (L 0 $ V 0) (Fn (TV 0) (TV 0))
True
> check [] (L 0 $ V 0) (Fn (TV 0) (TV 1))
False
> check [] bcomp (Fn (Fn (TV 0) (TV 0)) (Fn (Fn (TV 0) (TV 0)) (Fn (TV 0) (TV 0))))
True
> check [] bcomp (Fn (Fn (TV 1) (TV 2)) (Fn (Fn (TV 0) (TV 1)) (Fn (TV 0) (TV 2))))
True
> check [] bcomp (Fn (Fn (TV 0) (TV 1)) (Fn (Fn (TV 1) (TV 2)) (Fn (TV 0) (TV 2))))
False
> check [] oneid (Fn (TV 0) (TV 0))
TrueTo learn more about the history of bidirectional typing and its various applications, you may be interested in this survey article by Jana Dunfield and Neel Krishnaswami.
The last group of exercises will ask you to define various untyped lambda expressions computing different functions, and to test these definitions by running them on a few inputs. Of course the latter can be done by performing β-reduction by hand, but you might find it more fun to use one of the lambda calculus interpreters available online, such as George Kaye’s λ-term visualiser (demo’d in class), or Alec Minchington’s Lambster.
You should record your solutions as comments in your Haskell file in the format <name> = <λ-expression>. For example, the encodings of booleans and natural numbers and operations on them that we saw in class could be entered as follows:
-- Encodings of booleans and natural numbers from class
{-
true = \x.\y.x
false = \x.\y.y
not = \b.\x.\y.b y x
and = \b.\c.b c false
zero = \f.\x.x
one = \f.\x.f x
two = \f.\x.f (f x)
three = \f.\x.f (f (f x))
succ = \n.\f.\x.f (n f x)
add = \m.\n.m succ n
mult = \m.\n.m (add n) 0
isZero = \n.n (\b.false) true
-}You can refer to any of these definitions in the λ-expression you define below, and of course you can refer to any λ-expressions you define yourself.
Let’s start with some exercises to warm up…
Define a λ-expression isEven which given a Church-encoded natural number as input, returns true or false depending on whether or not the number is even. For example, isEven one should normalize to false (= \(\lambda xy.y\)), and isEven two should normalize to true (= \(\lambda xy.x\)).
Hint: remember that under the Church-encoding of natural numbers, the number \(n\) is represented as a “function composer”, which given a function \(f\) returns a new function corresponding to the \(n\)-fold composition of \(f\), that is, \(n = \lambda f.\lambda x.f^n x\). In this case, there is a simple function \(f\) that we can iterate \(n\) times on an appropriate initial value \(x\), in order to determine whether the number \(n\) is even.
Define a λ-expression exp which given two Church-encoded natural numbers as inputs, computes the first raised to the power of the second. For example, exp two three should normalize to the Church-numeral 8 = \(\lambda f x.f(f(f(f(f(f(f(f(x))))))))\).
Untyped lambda calculus does not have a built-in mechanism for defining pairs (or anything other than functions!), but like the booleans and the natural numbers, they can be encoded. The idea is that a pair is represented as a higher-order function that applies its argument to its two components. That is, we encode the tuple \((e_1, e_2)\) by: \[ (e_1, e_2) \mathbin{\overset{\mathrm{def}}=} \lambda f.f\ e_1\ e_2 \] Under this representation, the first and second projections are easily defined by application to the functions \(\lambda x.\lambda y.x\) and \(\lambda x.\lambda y.y\) respectively: \[ \pi_1 e \mathbin{\overset{\mathrm{def}}=} e\ (\lambda x.\lambda y.x) \qquad \pi_2 e \mathbin{\overset{\mathrm{def}}=} e\ (\lambda x.\lambda y.y) \]
For reference, let’s write down these encodings as comments:
-- Encodings of pairing and projections
{-
pair = \x.\y.\f.f x y
fst = \p.p (\x.\y.x)
snd = \p.p (\x.\y.y)
-}Define a λ-expression swap which swaps the components of a pair. For example, swap (pair true one) should be β-equivalent to pair one true.
Define a λ-expression swapIf, which swaps the components of its second (pair) argument just in case its first (boolean) argument is true. For example, swapIf true (pair true one) should be β-equivalent to pair one true, while swapIf false (pair true one) should be β-equivalent to pair true one.
For being such a simple operation, the predecessor function on natural numbers \[ n \mapsto \begin{cases} 0 & n = 0 \\ n-1 & n > 0 \end{cases} \] is surprisingly tricky to define in untyped lambda calculus, with Kleene reporting to have found the inspiration for a really clever trick at the dentist’s office. To understand the trick, it might help to first try to understand how a similar trick can be used to define a slightly more complicated function.
Without using a fixed point operator, define a λ-expression fib that given a Church-encoded natural number \(n\) as input, returns the \(n\)th Fibonacci number as output.
Hint: The idea is similar to the one we used to define a linear-time version of Fibonacci in Lecture 1 by first defining a function that takes an extra pair of accumulator parameters.
Now, using your experience defining the Fibonacci sequence, define the predecessor function as a λ-expression, and finally use that to define a function testing whether two natural numbers are equal.
Define a λ-expression pred which takes a Church-encoded natural number \(n\) as input, and returns \(n-1\) if \(n>0\), or else \(0\) if \(n=0\).
Define a λ-expression eqNat which takes two Church-encoded natural numbers \(m\) and \(n\) as input, and returns (the Church-encoded boolean) true just in case \(m = n\), or else false.
As we discussed in class, fixed point operators can be used to encode general recursive functions in untyped lambda calculus. The first fixed point combinator was discovered by Curry (the famous “Y combinator”, not to be confused with the startup accelerator), and another important one was introduced by Turing in his proof of the equivalence between λ-definability and Turing-machine computability:
-- Curry's and Turing's fixed point operators
{-
Y = \x.(\y.x(y y))(\y.x (y y))
Theta = (\x.\y.y (x x y)) (\x.\y.y (x x y))
-}The Collatz conjecture states that starting from any positive natural number \(n \ge 1\), iteratively applying the function \[ f(n) = \begin{cases}\frac{n}{2} & \text{if }n\text{ is even} \\ 3n+1 & \text{if }n\text{ is odd} \end{cases} \] will eventually reach the number 1. That is, for all \(n \ge 1\), there exists a \(k\) such that \(f^k(n) = 1\) (conjecturally).
Using a fixed point operator, write a λ-expression collatz that given a Church-encoded natural number \(n\), returns the smallest natural number \(k\) such that \(f^k(n) = 1\). If no such number exists (because the Collatz conjecture is false), your function is allowed to not terminate.