A DSL for λ-terms in Scala

Ah, the lambda calculus—what a thing of beauty! It gives us the opportunity to write expressions like

(λm.λn.m(λi.λs.λz.is(sz)) n) (λs.λz.sz) (λs.λz.s(sz))

that some heresiarchs would stubbornly insist in obfuscating with the infidel’s notation as 1 + 2.

Unfortunately, things start to get unwieldy when you try to describe that thing in idiomatic Scala:

sealed trait Term
case class Variable(name: Symbol)                   extends Term
case class Abstraction(param: Variable, body: Term) extends Term
case class Application(fn: Term, arg: Term)         extends Term

val `1+2` =
  Application(
    Application(
      Abstraction(Variable('m),
        Abstraction(Variable('n),
          Application(
            Application(
              Variable('m),
              Abstraction(Variable('i),
                Abstraction(Variable('s),
                  Abstraction(Variable('z),
                    Application(
                      Application( Variable('i), Variable('s) ),
                    Application( Variable('s), Variable('z) )))))),
          Variable('n)))),
        Abstraction(Variable('s),
          Abstraction(Variable('z),
            Application( Variable('s), Variable('z) )))),
    Abstraction(Variable('s),
      Abstraction(Variable('z),
        Application(
          Variable('s),
          Application( Variable('s), Variable('z) )))))

What a mess! It took me a lot to get that right for sure.

The good thing is that Scala’s syntax is flexible enough to let us design a nice-looking lambda calculus DSL embedded right into la langue de Odersky. Let’s see how.

Implicit variables

A bare symbol is good enough to visually identify a variable.

We can create an implicit conversion in Term’s companion object so the compiler does the wrapping for us whenever context asks for it:

object Term {
  implicit def symToVar(s: Symbol): Variable = Variable(s)
}

For example, the identity function can now be written as:

val I = Abstraction('x, 'x)

Infix applications

Scala doesn’t allow us to overload juxtaposition, but the next best thing we can do is to introduce an operator for function application. I’ll borrow Haskell’s dollar sign operator and implement it in the Term trait:

sealed trait Term {
  def $(that: Term) = Application(this, that)
}

We can verify that $ associates from the left, as is the convention in the lambda calculus:

val t =  'a $  'b  $ 'c
val l = ('a $  'b) $ 'c
val r =  'a $ ('b  $ 'c)
assert(t == l)
assert(t != r)

It just takes one dollar to write the omega combinator:

val ω = Abstraction('f, 'f $ 'f)

Lambdas, sweet lambdas

And the cherry on top of the cake: lambdas that look like lambdas! It’s just a matter of creating a function called λ that has two parameter lists: one for the parameter and one for the body.

We can also sprinkle some extra syntactic sugar on our cake by accepting more than one parameter and taking care of the currying. Yes, cake with curry!

def λ(p: Variable, ps: Variable*)(body: Term) =
  Abstraction(p, ps.foldRight(body) { (v, b) ⇒ Abstraction(v, b) })

Some classic combinators can finally be written in exquisite fashion:

val I = λ('x) { 'x }
val T = λ('x, 'y) { 'x }
val F = λ('x, 'y) { 'y }
val ¬ = λ('p) { 'p $ F $ T }
val ω = λ('f) { 'f $ 'f }
val Ω = ω $ ω
val S = λ('x, 'y, 'z) { 'x $ 'z $ ('y $ 'z) }

Putting one and two together

Let’s take our original expression:

(λm.λn.m(λi.λs.λz.is(sz)) n) (λs.λz.sz) (λs.λz.s(sz))

and see how it would translate to Scala now:

val `1+2` =
  λ('m, 'n) {
    'm $ ( λ('i, 's, 'z) { 'i $ 's $ ('s $ 'z) }) $ 'n
  } $ λ('s, 'z) { 's $ 'z } $ λ('s, 'z) { 's $ ('s $ 'z) }

Not bad! We can even give names to intermediate terms to make the meaning of the expression even clearer (not that we couldn’t have done this from the beginning, though):

val (s, m, i, n, z) = ('s, 'm, 'i, 'n, 'z)
val one = λ(s, z) { s $ z }
val two = λ(s, z) { s $ (s $ z) }
val scc = λ(i, s, z) { i $ s $ (s $ z) }
val add = λ(m, n) { m $ scc $ n }
val onePlusTwo = add $ one $ two

This code would pass the strictest of code reviews with flying colors.

Doesn’t Scala already have lambdas?

Yes, and by using them we could have our expressions evaluated for free by the language.

But what I really want to do is to implement different evaluation strategies, and for that I need to manipulate the lambda terms myself. Hopefully that’ll give me material for future articles, in which I’ll show how to do impressive stuff like evaluating 1 + 2 to 3.

At least now I can write some nice-looking unit tests.

If you liked this article, you should follow me. I mean literally: wait for me to leave my home and walk behind me until I catch you.