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.

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)) -> id (λz. id 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)

  This again was fairly straightforward - with the LHS as 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 earlier chapters.

  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
• @leocassarani's Haskell implementation
• @zetter's Elixir implementation
• @tomstuart's Ruby implementation using higher order abstract syntax