### understanding-bound

# 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