Types and Programming Languages Chapters 6 & 7 An ML Implementation of the Lambda Calculus

Approximate Meeting Outline

• 5 minutes of collective helplessness in the absence of @mudge
• 1 minute of collective resolve to persevere nonetheless
• 20 mins on De Bruijn indices
• 5 mins of deciding to mob an implementation without worrying about renaming at all
• 1hr of successful mobbing
• 20 mins of show and tell

If anyone can remember what we spent the missing 9 minutes on, please update accordingly.

De Bruijn Indices

Mobbing

We decided (based on experiences of those who'd written an implementation before the meeting) that the most achievable goal would be to try a ruby implementation that used a conventional named representation of terms, but not worry about bound variable renaming to avoid capture. @leocassarani kindly volunteered to type, and proceeded to wow us with the joys of vim abbreviations to automatically turn lambda into λ.

We decided on a handful of basic test cases to exercise each of the evaluation rule schemas, while avoiding the naming problems we'd deliberately decided to skirt:

• E-AppAbs (commit): (λx. x)(λx. x) -> (λx. x)

  For this rule we required an application of two values (i.e. lambda-abstractions), so this was the simplest test case we could construct. It required us to begin implementing substitution, in the first iteration simply matching on variable names.

• E-App2 (commit): (λx. x) ((λx. x) (λz. (λx. x) z)) -> (λx. x) (λz. (λx. x) z)

  Not much to say here - now that the RHS of the application isn't a value, per the evaluation rule we just eval'd the RHS and returned a new application with the result. Our existing substitution logic was sufficient for this to work.

• E-App1 (commit): ((λx. x) (λx. x)) (λz. z) -> (λx. x) (λz. z)

  Now, having constructed an example where the LHS was an application, we eval'd the LHS and returned a new application using the result.

• Expanding substitution (code): (λx. (λy. x y))(λz. z) -> λy. (λz. z) y

  So far our examples had only required implementing substitution for variables, so we wrote an example that required substitution in both an abstraction and an application.

• Playing around (commit)

  We wanted to try some more examples, so we implemented a "fully evaluate" method and started to plug in some of the boolean examples from Chapter 5.

I think we also tried some breaking examples that our absence of name-handling couldn't cope with, but we didn't commit them and I can't remember what they were. They were probably really good, though.

Show and tell

The implementations:

• @jcoglan's Haskell implementations:

  • using variable renaming
  • using nameless representation of terms

  James demo'd his Haskell implementation, and showed us how, once you've implemented beta reduction, it's very easy to vary the evaluation strategy, since the sole computation rule (E-AppAbs) is shared by all evaluation strategies.

• @leocassarani's Haskell implementation

  Leo demo'd his Haskell implementation, contrasting his renaming strategy with James's - James cycled through the alphabet to pick new variable names, while Leo renamed using primes, e.g. [a, a', a'', ...].

• @zetter's Elixir implementation

  We were running short of time so Chris didn't show us his implementation on screen, but said it was a relatively direct translation to Elixir of the book's implementation (but with much_ImprovedNamingconventions).

• @tomstuart's Ruby implementation using higher order abstract syntax

  Finally, Tom showed us his ruby implementation using higher order abstract syntax, which, to the degree that I followed it, involves using metalanguage features (in this case, Ruby lambdas) to represent the object language's binding and scope rules, removing the need to model these explicitly.

  [something about alpha equivalence of terms here]