|
I used de Bruijn indexes in Plumb[0], which is an alternative syntax for Lambda Calculus that embeds nicely in common scripting languages like PHP and Python. Whilst a classic lambda expression like `λx.y` has three parts: the argument name `x`, the body/result `y`, and the `λ_._` syntax to distinguish it from a variable or application; if we instead use de Bruijn indices, then we don't need a separate part for the argument: all we need is a body wrapped in some distinguishing syntax (like `λy` in the article). In Plumb, that distinguishing syntax is square brackets, so the "lambda term" `λy` would be written `[y]`. This wouldn't be possible if we had to write argument names, but ends up having some nice consequences: - We can write this as-is in many languages, and the result is a data structure (usually a list) which we can easily walk over with an interpreter function. - Variables are numbers, which can also be written as-is in many languages, and result in data that an interpreter function can handle. - The final piece of syntax is applications, which necessarily has two parts (the function and the input value). Classic Lambda Calculus uses juxtaposition, whilst Plumb uses an explicit binary operator: the comma `,`. Again, commas can be written as-is in many languages, and they interact nicely with square bracket notation, (host language) function application, and (in the case of Python and Haskell) tuple notation. The nice thing about using de Bruijn indexen, rather than de Bruijn "levels" or some other approaches to anonymous bindings (like those mentioned at the end of TFA), is that functions defined this way have an "intrinsic meaning"; e.g. `λ0` (or `[0]` in Plumb) is always the identity function; `λλλ(2 0 1)` (or `[[[2 , 0 , 1]]]` in Plumb) is always boolean NOT; etc. This lets us mix and match snippets of Plumb code with snippets of host-language code, embed each inside the other, and sprinkle around calls to an interpreter function willy-nilly, without worrying that the meaning depends on where our code ends up (e.g. at which "level" it reaches an interpreter). [0] http://www.chriswarbo.net/projects/plumb/using.html |