Lambda interpreter in the way of GOD

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. I even encountered an isFooVisitor once, which takes the evil one step beyond a simple method.

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.

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.

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);
}

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));
  }
}

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;
     }
  }
}