Weeknotes 39

I’m on holiday for the next week. As with last time this won’t involve going anywhere because that still doesn’t feel safe enough to be relaxing. The weather forecast looks a bit too grim for the occasional Hackney walks and bike rides I was imagining but I’m still looking forward to the downtime even if the scenery’s not going to be very novel.

My kitchen now contains a huge 16kg bag of very strong flour, thus completing my transformation into Internet Bread Man. I don’t have enough space to store a 16kg bag of anything so it’s a constant inconvenience. The crime is its own punishment.

More marketing: I enjoyed the new recreations of famous reaction GIFs that Naughty Dog released on Outbreak The Last of Us Day. Their version of Magikarp Guy in particular is impressively close to the original. I want to believe these are fun to make, although I suspect it’s all part of the larger soul-crushing grind of modern game development.

I’ve been having fun with some secret new hardware this week. This is sort of a useless and annoying thing to say but I’m mentioning it now so that I can link back here in a future weeknote once I’m able to talk about it.

At work I’m helping to run a Types and Programming Languages book club. I’ve been through this book once as a graduate student and again with London Computation Club so I’m now pretty comfortable with the material and am finding it interesting to take another run at it with a new group of people.

I learn theory best by putting it into practice, and last time I read the book I knocked up a little inference rule interpreter, an implementation of higher-order abstract syntax and a more conventional type checker to help cement my understanding. This time I’m trying to prepare exercises for my colleagues, specifically by writing tests for the various toy systems and challenging them to fill in the implementations.

At the moment we’re covering the untyped lambda calculus which is close to my heart but presents an interesting technical problem: how can I write tests for this language while remaining agnostic about whether its variables are represented conventionally (i.e. with names) or namelessly (i.e. with de Bruijn indices)? The book’s implementation uses the latter because that makes it easier to get the fiddly details right, but it’s also a bit harder to understand so I didn’t want to lock anyone into it if they prefer the familiarity of named variables. Avoiding lock-in would require an API for the tests to talk to the implementation — “make a variable with this name”, “make an abstraction with this body”, “evaluate this term” etc — which worked the same regardless of representation.

I ultimately abandoned this idea because I couldn’t come up with a tidy API which was agnostic without also being harder to implement correctly than the actual ideas we’re learning. (For the curious: if the API doesn’t supply a naming context then it has to be carried around by the representation of nameless terms themselves, which then complicates the construction of larger terms from smaller ones.) Instead I decided to write tests for named terms and then provide an evaluation adapter which could convert a named term into a nameless one, evaluate it, and convert it back into a named term again for checking.

At this point I realised I hadn’t implemented the conversion from named to nameless terms before, and wasn’t immediately sure how to do it. It feels slightly chicken-and-egg because we need to know the names of all the free variables to give each variable the right index, but we don’t know where all the free variables are until we’ve finished converting the term.

The naïve solution is to do it in two passes. First we walk over the term to find the free variables:

def free_in(term)
  case term
  when Variable
    [term.name]
  when Abstraction
    free_in(term.body) - [term.parameter]
  when Application
    (free_in(term.left) + free_in(term.right)).uniq
  end
end

Then, once we have the list of names, we can walk over the term again to convert it and give each variable its correct index by looking it up in the list:

def to_nameless(names, term)
  case term
  when Variable
    index = names.index(term.name)
    Nameless::Variable.new(index)
  when Abstraction
    body_names = [term.parameter] + names
    body = to_nameless(body_names, term.body)
    Nameless::Abstraction.new(body)
  when Application
    left = to_nameless(names, term.left)
    right = to_nameless(names, term.right)
    Nameless::Application.new(left, right)
  end
end

This works but it feels a bit shit because we’re visiting the nodes of the tree twice in the same order like a chump.

It took a shower for me to realise that we want to combine both phases and walk over the term only once, allowing the free variable names to flow up to the root and percolate back down again to the precise spot where they’re needed. We can do that by returning the list of names and a function which delays the computation of building the converted term:

def to_nameless(term)
  case term
  when Variable
    builder = -> names {
      index = names.index(term.name)
      Nameless::Variable.new(index)
    }
    [[term.name], builder]
  when Abstraction
    body_names, body_builder = to_nameless(term.body)
    builder = -> names {
      body = body_builder.call([term.parameter] + names)
      Nameless::Abstraction.new(body)
    }
    [body_names - [term.parameter], builder]
  when Application
    left_names, left_builder = to_nameless(term.left)
    right_names, right_builder = to_nameless(term.right)
    builder = -> names {
      left = left_builder.call(names)
      right = right_builder.call(names)
      Nameless::Application.new(left, right)
    }
    [(left_names + right_names).uniq, builder]
  end
end

Once we have the final list of names we can call the function with it and get a nameless term back. This staged solution is obvious in hindsight but it was fun to work it out.

I have enough self-awareness to realise that the above saga isn’t of general interest, but I retell it here because I want to remember the pleasure of being reminded this week how much I love programming. It gives me such satisfaction to build intricate little machines that solve these intricate little puzzles, even if nobody else sees them or cares, and if I write it down now I’ll be able to feel it later. What else are weeknotes for?

I know of at least two people who’ve bought one of those fancy bread knives after I wrote about them. I’m an influencer.