CSE301

This lab has a part about untyped lambda calculus, a part about simple type inference, and an optional part about “bidirectional” typing. It is suggested that you get a start on both Part 1 and Part 2 during the lab session (even if you do not finish them), in order to be able to ask questions about the basics of lambda calculus and typing.

Part 1 : Programming in untyped lambda calculus

The first 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).

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) zero
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.

(Note that we are not asking you to write any Haskell code for this part, although untyped lambda calculus expressions can be translated into Haskell without too much difficulty.)

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\)).

-- Exercise 1a
{-
isEven = <your definition here>
-}

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))))))))\).

-- Exercise 1b
{-
exp = <your definition here>
-}

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) \]

Define a λ-expression swap which swaps the components of a pair. For example, swap (pair true one) should be β-equivalent to pair one true.

-- Exercise 1c
{-
swap = <your definition here>
-}

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.

-- Exercise 1d
{-
swapIf = <your definition here>
-}

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.

-- Exercise 1e (optional)
{-
fib = <your definition here>
-}

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\).

-- Exercise 1f (optional)
{-
pred = <your definition here>
-}

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.

-- Exercise 1g (optional)
{-
eqNat = <your definition here>
-}

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:

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.

-- Exercise 1h (optional)
{-
collatz = <your definition here>
-}

Part 2 : Simply-typed lambda calculus and principal type inference

The aim of this part of this lab is to get a better understanding of how type inference works in Haskell, by considering a few examples of simple type inference for lambda terms.

But before any examples, let’s recall the formal typing rules of simply-typed lambda calculus (using inference rule notation where the judgments above the line represent premises and the judgment below the line is the conclusion):

\[ \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 \]

Here the underlying judgment \(\Gamma \vdash e:B\) takes a typing context of the form \(\Gamma = x_1:A_1,\dots,x_n:A_n\), a term (a.k.a. expression) \(e\), and a type \(B\). The judgment asserts that \(e\) has type \(B\) under the assumption that its free variables have the types in \(\Gamma\).

For example, here is a derivation that the expression \(\lambda f.\lambda x. f\ x\) has type \((o \to o) \to (o \to o)\):

\[ \frac{ \frac{\displaystyle f : o \to o \in f : o \to o,x : o}{\displaystyle f : o \to o,x : o \vdash f : o \to o}\qquad \frac{\displaystyle x:o \in f : o \to o,x : o}{\displaystyle f : o \to o,x : o \vdash x : o} } { \frac{ \frac{\displaystyle f : o \to o,x : o \vdash f\ x : o} {\displaystyle f : o \to o \vdash \lambda x. f\ x : o \to o}} {\displaystyle\lambda f.\lambda x. f\ x : (o \to o) \to (o \to o)}} \]

Now, an important property of simple typing is that if a term is typable then it always has a “best” type, called its principal type. Formally, this means that to check whether the term has some given type, it is necessary and sufficient to check whether that type is an instance of the principal type under a substitution for type variables.

For example, by substituting \(o\) for \(a\) and \(b\), it is easy to check that the type \((o \to o) \to (o \to o)\) is an instance of \((a \to b) \to (a \to b)\), which is the principal type of \(\lambda f.\lambda x. f\ x\).

In both cases, we can get the GHC interpreter to quickly give us this information using the :type command (which abbreviates to :t):

ghc> :t \x y z -> x (y z)
\x y z -> x (y z) :: (t1 -> t2) -> (t3 -> t1) -> t3 -> t2
ghc> :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, which is essentially a big constraint solving problem.

The expression \(\lambda xyz.x\ (y\ z)\) is a lambda abstraction, so 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\). 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) \] This is indeed equivalent up to renaming of variables with the type \((b \to c) \to (a \to b) \to (a \to c)\) that what we claimed was its principal type, and with the output of GHC.

On the other hand, for the expression \((\lambda x.x\ x)(\lambda x.x\ x)\) to be typed, using the \(app\) rule, we would 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 (at least with finite types), and so the subexpression \(\lambda x.x\ x\) is not simply-typable. 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.

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.)

-- Exercise 2a
{-
e1 :: ??
e2 :: ??
e3 :: ??
e4 :: ??
e5 :: ??
e6 :: ??
-}

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.

-- Exercise 2b
fn1 :: a -> b -> (a -> b -> c) -> c
fn1 = undefined
fn2 :: (a -> b) -> (b -> b -> a) -> (a -> a)
fn2 = undefined
fn3 :: ([a] -> b) -> a -> b
fn3 = undefined
fn4 :: ((a -> a) -> b) -> b
fn4 = undefined

Is there a simply-typed λ-expression whose principal type is \((a \to a) \to a\)? Why or why not?

-- Exercise 2c (optional)
{-
mysterylam = ??
-}

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.

-- Exercise 2d (optional)
mysteryfn = undefined

Part 3 (optional) : Implementing a bidirectional type checker

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:

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),

although it might still take the programmer some time to understand how to fix the bug.

The programmer had in mind a 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 str:

The reason for the misdirection is that the type checker is able to satisfy all of the 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:

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:

\[ \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.

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:

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:

-- Exercise 3 (optional)
check = undefined
synth = undefined

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))
True

To 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.

Lab 3 (lambda calculus and propositions-as-types)

General instructions

Introduction

Part 1 : Programming in untyped lambda calculus

Part 2 : Simply-typed lambda calculus and principal type inference

Part 3 (optional) : Implementing a bidirectional type checker