'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.
I like it. But how did you teach Scala this notation?
ReplyDeleteTry this:
ReplyDeletepackage 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))))