Thursday, March 31, 2011

Scala Internal DSL for Lambda Calculus

I've been playing with the untyped lambda calculus recently, and come up with this notation for it in Scala:

'x ^: 'y ^: 'x ! 'y
'x ^: 'y ^: 'x ! ('x ! 'y)
'x ^: 'y ^: 'x ! ('x ! ('x ! 'y))

which translates to:

λx.λy.xy
λx.λy.x(xy)
λx.λy.x(x(xy))

(You might recognize these as the Church numerals one through three.)

To digest this, you first have to imagine abstraction as an infix operator rather than a prefix operator. If you squint a little, you can see a caret as a lambda (the colon is necessary to get Scala to make the operator right-associative, as is conventional).

The exclamation point is the application operator by analogy with the notation used in Scala Actors. It takes only a wee bit of mental squinting to see passing an argument to a function as sending a message to an actor.

The single quote prefix in Scala turns an identifier into a Symbol, which is like a String but with only half the quoting. Scala Symbols are intended for purposes that are, uh, symbolic—I think a lambda calculus variable qualifies.

As cute as dancing kittens? You be the judge.

2 comments:

  1. I like it. But how did you teach Scala this notation?

    ReplyDelete
  2. Try this:


    package lambdas

    sealed trait Expr {
    def ^: (v: Var) = Lam(v,this)
    def ! (arg: Expr) = Ap(this,arg)
    }

    object Expr {
    implicit def toExpr (sym: Symbol): Expr = Var.toVar(sym)
    }

    case class Var (sym: Symbol) extends Expr

    object Var {
    implicit def toVar (sym: Symbol): Var = Var(sym)
    }

    case class Lam (v: Var, expr: Expr) extends Expr

    case class Ap (f: Expr, arg: Expr) extends Expr


    then:


    scala> import lambdas._
    scala> import Expr._

    scala> 'x ^: 'y ^: 'x ! 'y
    res0: lambdas.Lam = Lam(Var('x),Lam(Var('y),Ap(Var('x),Var('y))))

    ReplyDelete