The H2 Wiki


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

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

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