I recently attended the SPLASH-E presentation on Lambdulus: Teaching Lambda Calculus Practically by Jan Sliacky and Petr Maj. It was a very interesting presentation describing the Programming Paradigms (PPA) course at the Czech Technical University. I really think they are onto something!
Much of the presentation focused on the web-based programmer-friendly λ-calculus evaluator, affectionately called Lambdulus. To make the evaluator more programmer-friendly, they extend the untyped λ-calculus with macros and break-points and they use special evaluation rules for reducing macros. The paper was also a very good read and went into a little more detail about the course and their approach to teaching the λ-calculus.
One of the more important parts of Lambdulus is that it chooses which type of evaluation is appropriate. This is particularly important for reducing church numerals, but also leads to much cleaner looking λ-expressions because they are careful with how they expand macros. Lambdulus is also careful about how many of the evaluation steps to show to the programmer.
Macros are named expressions defined using the syntax NAME := [λ-expression].
Lambdulus is very careful about when they expand macros. In general, macros are
only expanded if they are applied to some other expression. If a λ-abstraction
is applied to a macro it is passed by reference, i.e. the abstracted variable is
substituted for the macro not its definition. This makes the reduced expression
look much cleaner.
Lambdulus also supports something they call dynamic macros. Currently these are numbers and arithmetic operators. Instead of defining a infinitely many macros manually, one for each church numeral, Lambdulus defines numeric macros dynamically. Reduction, when arithmetic operators are applied to numeric macros are also simplified.
Overall I really liked the project and their approach to teaching students how to program in the λ-calculus! I really liked how they have a clearly defined goal of teaching students how to program in the λ-calculus by treating it as a “real” programming language and they build everything around that goal. One of the strengths of their approach is realizing that when programming in the λ-calculus, we really want different kinds of reduction for different kinds of λ-expressions. For example, even if we are working in a call-by-value or call-by-name setting, for arithmetic on church numerals we probably want to be a little more agressive and do a full normal order reduction and then contract the result into a numeric macro. This makes the result look a lot cleaner and helps programmers debug their λ-calculus programs since what is going on during execution is a lot more clearer.
Their evaluator is available at https://lambdulus.github.io/! They paid a lot of attention to making Lambdulus more developer friendly. I didn’t talk about break-points above, but I found that interesting as well! I remember having a lot of trouble with church encodings when I was learning to program in the λ-calculus and I really think I could have benefitted from playing around in Lambdulus!