The Ghost of Types Past

This is the second part of (Re)Visiting Expressions.

Is there a way to avoid having to wait until runtime to verify that our expressions are well-typed? Indeed, a simple application of Phantom types can make the compiler to work to our advantage. There is nothing in the application of phantom types that is specific to functional programming, except for the use of parametric polymorphism. We can use, like here, phantom types to make our Java programs type-safe, or to enforce statically (that is, in compile-time) various desirable properties of our program.

The idea is to constrain the construction of values by encoding the properties in type parameters. These constraints can go from typing ADT trees to enforcing access restrictions and static bounds-checking. As a technique, it is simplicity itself: a module exports a parametric type —which is kept abstract— but whose implementation does not depend on the type parameter. Smart constructor functions (the functional counterpart of static factories) are restricted in the module interface to various instantiations of the type parameter; the type-checker ensures that all applications are correctly typed by means of unification.

Our phantom type will wrap expressions, assigning to each a type tag T:

final class E<T> {
  private final Exp e;
  private E(Exp e) { this.e = e; }

However, values of this class will only be created by the smart constructors. For instance, an integer constant is tagged with Integer:

  public static E<Integer> con(int value) {
    return new E<Integer>(Exp.con(value));
  }

Similarly for addition and comparison, with respective tags Integer and Boolean:

  public static E<Integer> add(E<Integer> left, E<Integer> right) {
    return new E<Integer>(Exp.add(left.e, right.e));
  }
  public static E<Boolean> le(E<Integer> left, E<Integer> right) {
    return new E<Boolean>(Exp.leq(left.e, right.e));
  }

Note that the arguments are themselves tagged to codify the requirement that addition operates on two integer values and returns an integer. In this light, the constructor for a conditional:

  public static <T> E<T> cond(E<Boolean> test, E<T> ifTrue, E<T> ifFalse) {
    return new E<T>(Exp.cond(test.e, ifTrue.e, ifFalse.e));
  }

makes clear that the condition must be a boolean expression, and both the true and the false expressions must evaluate to the same type T (which has nothing to do with the class parameter, as this is a static method), which is then the type of the result.

For convenience, instances of this class know how to evaluate and print themselves out:

  private static final EvalExp evaluator = new EvalExp();
  private static final ShowExp printer   = new ShowExp();

  public Val eval() {
    return e.accept(evaluator);
  }
  public void print() {
    e.accept(printer);
  }
}

This avoids the need to expose the contents of the wrapper class; an alternative is to define a method that projects the phantom type to the type of the wrapped expression (i.e., a simple accessor).

We can now test our expressions. Our test harness becomes much simpler now that the phantom type dispatches the Visitors:

public final class PhantomTest {
  public static void main(String[] args) {
    E<Integer> e1;
    e1 = E.cond(E.le(E.con(3), E.con(5)), E.add(E.con(1), E.con(2)), E.con(0));
    e1.print();
    System.out.print(" = ");
    e1.eval().accept(new ShowVal());
    System.out.println();

    // E<?> e2 = E.cond(E.con(1), E.con(1), E.con(1));
  }
}

Running it produces the same output as before:

Cond(Leq(ConI(3),ConI(5)),Add(ConI(1),ConI(2)),ConI(0)) = 3 : int

(This is exactly the same ouput as before, which is unsurprising since the phantom type delegates blindly to the original, type-unsafe code). If you try to compile the test with the second, ill-typed expression uncommented, the compiler will complain, and will refuse to proceed:

PhantomTest.java:233: <T>cond(E<java.lang.Boolean>,E<T>,E<T>) in E cannot be
  applied to (E<java.lang.Integer>,E<java.lang.Integer>,E<java.lang.Integer>)
    E<?> e2 = E.cond(E.con(1), E.con(1), E.con(1));
               ^
1 error

As you can see, the type-checking rules of Java are being applied to detect the invalid construction of a conditional with a non-Boolean test. What is also important to remark is that it is not necessary to manually tag constructors; expressions are built out of method calls much as we've seen in the untyped case.