In the world of object-orientation, they have design patterns and principles to guide the design of software. For example, mechanisms like instanceof or switch are discouraged, because they violate the open/closed principle; at least the open part. Such rules are Good Object-oriented Design; or GOD for short. Instead you should use dynamic dispatch, says GOD.

Among the heathens, there is a sneaky way out. They use isFoo methods instead of instanceof Foo, but of course a true follower of GOD will reject that. An if is just a poor switch anyway.

Let us be better than that. Let us design an interpreter for lambda calculus in the way of GOD.

The basic data structure is easy. An abstract Term class, with three subclasses Application, Abstraction, and Variable. Application contains two Terms, left and right. Abstraction contains a body term and a variable for substitution. Variable contains an id.

UML class diagram of Lambda data structures

Since we know that functional programmers love immutability, let us make those data structures immutable. All fields shall be final!

Now what methods do we need for a lambda calculus interpreter? Substitution is an important building block. Within a term we want to substitute a certain variable for another term. Since we want to call this on any term, it shall be declared as an abstract method in Term and implemented in all subclasses.

// Variable
Term substitute(Variable v, Term sub) {
  if (this.equals(v))
    return v;
  return this;
}

// Application
Term substitute(Variable v, Term sub) {
  Term l = left.substitute(v,sub);
  Term r = right.substitute(v,sub);
  if (l.equals(left) && r.equals(right))
    return this;
  return new Application(l,r);
}

// Abstraction
Term substitute(Variable v, Term sub) {
  if (var.equals(v))
    // same variable but bound differently in body
    return this;
  return new Abstraction(var,
                         body.substitute(v,sub));
}

Now we want beta reduction. The method should beta reduce a term once according to call-by-value semantics. How does beta reduction work? Given an application with an abstraction with a certain variable x on the left, substitute x for the application's right y in the abstraction's body.

Application(Abstraction(x,body),y) => body.substitute(x,y)

We might have to look deep into a term, until we match this pattern.

Now the signature is clear. The implementation for Variable and Abstraction is easy, since it follows the same pattern as substitution.

// Variable
Term evalOnce() {
  return this;
}

// Abstraction
Term evalOnce() {
  Term b = body.evalOnce();
  if (body.equals(b))
    return this;
  return new Abstraction(var, b);
}

Application is tricky. How do we check, if left is an abstraction? The word of GOD says, we are not allowed to. Instead we must defer the action to it via method call.

// Application
Term evalOnce() {
  Term l = left.apply(right);
  if (left.equals(l))
    return this;
  return l;
}

Now we must give Term another abstract method apply, which always returns this except for abstractions.

// Abstraction
Term apply(Term t) {
  return body.substitute(var, t);
}

At this point, we have a solution, which nice demonstrates how to avoid instanceof and similar mechanisms. A functional programmer would use pattern matching. That violates another word of GOD if it cannot be extended externally.

Visitors

Wait a moment, says GOD. You forgot to use a design pattern and design patterns are always good. We should decouple the operation from the data structure. Loose coupling is also good. Let us abstract the tree walking from substitute and evalOnce into a visitor. The basic visitor code is quite boring of course:

abstract class TermVisitor {
  Term visitVariable(Variable v);
  Term visitAbstraction(Abstraction a);
  Term visitApplication(Application a);
}

// Variable
Term accept(TermVisitor v) {
  return v.visitVariable(this);
}

// Abstraction
Term accept(TermVisitor v) {
  return v.visitAbstraction(this);
}

// Application
Term accept(TermVisitor v) {
  return v.visitApplication(this);
}

Now the substitution visitor. The code looks suspiciously like the recursive variant from above, but there are subtle differences.

class SubstitutionVisitor extends TermVisitor {
  final Variable var;
  final Term sub;

  Term visitVariable(Variable v) {
    if (v.equals(var))
      return v;
    return sub;
  }

  Term visitApplication(Application a) {
    Term l = a.left.accept(this);
    Term r = a.right.accept(this);
    return new Application(l,r);
  }

  Term visitAbstraction(Abstraction a) {
    if (var.equals(v))
      // same variable but bound differently in body
      return a;
    return new Abstraction(a.var, a.body.accept(this));
  }
}

Next step, we need to implement beta reduction.

class BetaReductionVisitor extends TermVisitor {
  // we only want to perform a single beta reduction
  boolean done;
  Term y;

  Term visitVariable(Variable v) {
    return v;
  }

  Term visitApplication(Application a) {
    this.y = a.right;
    Term l = a.left.accept(this);
    if (done)
        return new Application(l,r);
    // try to beta reduce on the right
    return a.right.accept(this);
  }

  Term visitAbstraction(Abstraction a) {
     if (y == null) {
         return new Abstraction(
               a.var, a.body.accept(this));
     } else {
         // pattern matched, now substitute
         a.body.accept(new
               SubstitutionVisitor(a.var, this.y));
         done = true;
     }
  }
}

In this specific case, the visitor pattern is probably over-engineered, although I had cases where it was suitable. Clearly, GOD needs apostles to apply holy principles to the real world.


Thanks to my colleagues for discussing this with me during lunch. They found a subtle bug, which is left to the reader to fix, as it does not affect to central point of this article. Hint: There is no alpha renaming in the code above.

©

Good Object-oriented Design (GOD) says to avoid instanceof. Here is how to implement pattern matching another way.