# 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.

## 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:

• 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'', ...]`.
• 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`).