Stephanie Weirich - How to Implement the Lambda Calculus, Quickly

Stephanie Weirich compares different Haskell implementations of alpha-equivalence and capture-avoiding substitution in the lambda calculus.

Special thanks to the Haskell Foundation for supporting the production of this video! Haskell Love 2021 schedule: emamo.com/event/haskell-love Haskell Love twitter: twitter.com/_haskellove Alpha-equivalence and capture-avoiding substitution are two fundamental operations in the implementation of the lambda calculus. But, what is the best way to implement these operations in Haskell? I wish I knew. In this talk, which is part tutorial and part work-in-progress, I'll present what I have learned from gathering many, many implementations of these operations into the same repository and comparing their execution using a small benchmark suite. One observation to make is that that most of these implementations of capture-avoiding substitution require multiple traversals of the AST, which can lead to a significant slowdown on larger examples. However, by reifying, delaying, and fusing these traversals, we can dramatically improve performance. Not only that, but I will also show how this optimization can be invisibly incorporated into binding libraries that automatically provide capture-avoiding substitution "for free". Link to benchmark repository: github.com/sweirich/lambda-n-ways