Understanding Bound

WARNING: INCOMPLETE!

Introduction

bound is a Haskell library written by Edward Kmett that allows you to encode and manipulate languages that involve binding, such as lambda calculus. Edward has published an introduction to bound at the FP Complete School of Haskell. His introduction starts by summarizing other approaches to dealing with binding before explaining in detail how bound was derived from an earlier approach. I’m not sure who came up with the idea of bound but Edward is listed as the sole author on the Hackage page.

I’ll give a very brief refresher on untyped lambda calculus. It’s not supposed to be an introduction.

Lambda calculus lets us build “terms” by following three rules. We can

• write variables, such as x, y, z
• apply one term to another, so from x and y we get x y
• abstract a term with a lambda, so from x y we can get \x (x y) and \y (x y)

For notational convenience, instead of writing (x y) z we will often drop the parentheses and write simply x y z instead.

Besides these rules for forming terms there are important operations which manipulate terms.

Substitution

Given terms t1 and t2 we can “substitute t1 for all free occurrences of x in t2”. For example

• If t1 = z z and t2 = y x then the result is y (z z). One occurence of x has received the substitute.

• If t1 = \y y and t2 = z x x then the result is z (\y y) (\y y). Two occurrences of x have received the substitute.

• If t1 = z and t2 = \y (y z) then the result is t2 = \y (y z). There were no occurrences of x so the substitution left the term with the same form.

• If t1 = y z and t2 = (x y) (\x z x) then the result is t2 = (y z y) (\x z x). This is important! The first occurrence of x was not bound by any lambda so it is called “free” and receives the substitutute. The second occurrence was not free so it does not receive the substitute.

Instantiation

A term of the form \x ... can have its binding instantiated to a variable. For example, in \x (x y x) the lambda abstraction can be instantiated with x, giving x y x. But the x in the lambda was arbitrary, so we can also instantiate it with z, giving z y z.

When we embed something like the lambda calculus in Haskell we want a type that represents terms of this form