Assignment 4 - Lambda calculus

The GitHub Classrooms link for this assignment is here

The deadline for the assignment is midnight on March 20th, 2024.

For this exercise, you will need to have the DataKinds and GADTs language extensions enabled.

Introduction to well scoped lambda terms

We have seen plenty of examples in the lectures using length-indexed lists, also known as vectors. These use the (type level version of) the natural numbers:

data Nat = Zero | Succ Nat

We can also use these numbers to define the well scoped lambda terms:

data Term n where
  App :: Term n -> Term n -> Term n
  Abs :: Term (Succ n) -> Term n
  Var :: Fin n -> Term n

Here each a Term n is:

We represent variables using (scoped) De Bruijn indices, where each variable uses a ‘number’ to refer its binding site. The ‘number’ 0 refers to the most recent lambda abstraction; the ‘number’ 1 refers to the one before that; etc.

To ensure we can only refer to existing variables, we introduce the following type to represent De Bruijn indices:

data Fin n where
  Top :: Fin (Succ n)
  Pop :: Fin n -> Fin (Succ n)

The type Fin n has exactly n inhabitants. We will use the Top constructor refers to the most recently bound variable; the Pop constructor to increments the variable index.

In particular, we can represent closed lambda terms (without any free variables) as follows:

type ClosedTerm = Term Zero

Exercise 1 - warm-up (1 point)

Show how to write values of type Closed corresponding to the I, K, S and Y combinators.

Exercise 2 - lookup (1 point)

Show how to write a vlookup function with the following type:

vlookup :: Fin n -> Vec a n -> a

This function return the i-th element of the input vector. It should always return a value and never fail dynamically (with an out-of-bounds exception).

Exercise 3 - show-up (1.5 point)

Write a show instance for Terms.

To do so, you will need to generate fresh names for variables bound by a lambda abstraction. Ensure that you produce a string that satisfies Barendregt’s variable convention – that is, each lambda should bind a unique variable name.

For example given a closed term idTerm representing the identity function, the call show App idTerm idTerm should produce a string such as:

(\x0 -> x0) (\x1 -> x1)

You may find it helpful to define an auxiliary function with the following type:

showTerm :: Vec String n -> Term n -> State VarNames String

To get full marks, ensure that your function takes account of precedences and does not introduce unnecessary parentheses.

Exercise 4 – check-up (1 point)

Not all terms are well scoped. Suppose that we have a parser that produces the following lambda terms:

type VarName = String

data RawTerm =
    RawApp RawTerm RawTerm
  | RawAbs VarName RawTerm
  | RawVar VarName

Write a scope checker to check whether a given raw term is closed or not:

newtype Error = OutOfScope VarName

check :: RawTerm -> Either Error ClosedTerm

Hint: Do not try to define the check function directly. Instead, find a more general function that works on (possibly open) Term n values.

Exercise 5 – Bracket abstraction (1 point)

We can use the same variable representation to represent terms in combinatory logic, built using the S, K, and I combinators that we saw in class:

data Combinator n where
  S :: Combinator n
  K :: Combinator n
  I :: Combinator n
  CApp :: Combinator n -> Combinator n -> Combinator n
  CVar :: Fin n -> Combinator n

Define a pair of functions:

fromC :: Combinator n -> Term n
toC :: Term n -> Combinator n

You will need an auxiliary function to handle lambda abstractions, sometimes called bracket abstraction.

Can you use this translation to express the Y combinator in terms of SKI?

Exercise 6 - reduce (1 point)

Define a function:

step :: Combinator n -> Maybe (Combinator n)

that performs the left-most reduction step in a given combinator using the following three rules:

Use the step and unfoldr functions to produce an evaluation trace,a that is, a (possibly infinite) list of combinator terms, ending in a term that cannot be reduced further.

Exercise 7 - substitution and renaming (1.5 points)

Define a function that renames all the ‘free’ variables:

rename :: (Fin n -> Fin m) -> Term n -> Term m

Hint: the only difficult case is the one for lambda abstractions. Update the function you are passing around so the freshly bound variable stays unchanged.

Finally, define a capture avoiding substitution function:

substitute :: Vec (Term k) n -> Term n -> Term k

You may find the vlookup and map functions on vectors useful.

Finally, show that there is an identity subustitution:

idEnv :: Vec (Term n) n

such that substitute idEnv t = t

Exercise 8 - open end (1 point)

Add a parser for the lambda calculus. Can you add Peano numbers? Let bindings? Booleans? Conditional expressions? Recursion? Data types and pattern matching? Lennart Augustsson’s MicroHs compiler maps a (fairly complete) subset of Haskell to a fixed collection of combinators. How far can you get?