More Phantom Types in Java

Posted on December 9, 2010 by Tommy McGuire

Labels: notation, toy problems, quote, java, programming language

Text unabashedly stolen from Ralf Hinze, Fun with Phantom Types.

Introducing phantom types

Suppose you want to embed a simple expression language in Haskell. You are a firm believer of static typing, so you would like your embedded language to be statically typed, as well. This rules out a simple Term data type as this choice would allow us to freely mix terms of different types. Idea: parameterize the Term type so that Term \(\tau\) comprises only terms of type \(\tau\).

Zero :: Term Int
Succ, Pred :: Term Int \( \rightarrow \) Term Int
IsZero :: Term Int \(\rightarrow\) Term Bool
If :: \(\forall\alpha\). Term Bool \(\rightarrow\) Term \(\alpha \rightarrow\) Term \(\alpha \rightarrow\) Term \(\alpha\)

Alas, the signature above cannot be translated into a data declaration[...in un-extended Haskell 98. It can be done with Generalized Abstract Data Types.]

Idea: augment the data construct by type equations that allow us to constrain the type argument of Term.
\[
\begin{equation}\begin{split}
\textit{data}\ \textit{Term}\ \tau & = & \textit{Zero}\ & \textit{with}\ \tau = \textit{Int} \\
& | & \textit{Succ (Term Int)} & \textit{with}\ \tau = \textit{Int} \\
& | & \textit{Pred (Term Int)} & \textit{with}\ \tau = \textit{Int} \\
& | & \textit{IsZero (Term Int)} & \textit{with}\ \tau = \textit{Bool} \\
& | & \textit{If (Term Bool)} (\textit{Term}\ \alpha) (\textit{Term}\ \alpha) & \textit{with}\ \tau = \alpha
\end{split}\end{equation}
\]
Thus, Zero has [type Term \(\tau\)] with the additional constraint \(\tau\) = Int.

NB. The type variable does not appear on the left-hand side; it can be seen as being existentially quantified.

Here is a simple interpreter for the expression language. Its definition proceeds by straightforward structural recursion. Even though eval is assigned the type \(\forall\tau.\textit{Term}\ \tau\rightarrow\tau\), each equation has a more specific type as dictated by the type constraints. The interpreter is quite noticeable in that it is tag free. If it receives a Boolean expression, then it returns a Boolean.

I apologize for the Peano arithmetic, but, really, it's not my fault.

  public static abstract class Term<T>
  {
    public abstract T eval();
  }
  
  public static class Zero extends Term<Integer>
  {
    @Override public Integer eval() { return 0; }
  }
  
  public static class Succ extends Term<Integer>
  {
    public final Term<Integer> pred;
    public Succ(Term<Integer> pred) { this.pred = pred; }
    @Override public Integer eval() { return 1 + pred.eval(); }
  }
  
  public static class IsZero extends Term<Boolean>
  {
    public final Term<Integer> i;
    public IsZero(Term<Integer> i) { this.i = i; }
    @Override public Boolean eval() { return i.eval() == 0; }
  }
  
  public static class If<A> extends Term<A>
  {
    Term<Boolean> test;
    Term<A> t, f;
    public If(Term<Boolean> test, Term<A> t, Term<A> f) { this.test = test; this.t = t; this.f = f; }
    @Override public A eval() { return test.eval() ? t.eval() : f.eval(); }
  }
  
  public static     Term<Integer> zero()                  { return new Zero(); }
  public static     Term<Integer> succ(Term<Integer> i)   { return new Succ(i); }
  public static     Term<Boolean> isZero(Term<Integer> i) { return new IsZero(i); }
  public static <A> Term<A>       iff(Term<Boolean> test, Term<A> t, Term<A> f)
                                    { return new If<A>(test, t, f); }

  public static void main(String[] args)
  {
    Term<Integer> iff = iff(isZero(succ(zero())), zero(), succ(zero()));
    System.out.println(iff.eval());
    // Fails to compile with: The method isZero(Eval.Term<Integer>) in the type Eval is
    // not applicable for the arguments (Eval.Term<Boolean>)
    // isZero(isZero(zero()));
  }

The type Term \(\tau\) is quite unusual.
Term is not a container type: an element of Term Int is an expression that evaluates to an integer; it is not a data structure that contains integers.
We cannot define a mapping function \( (\alpha\rightarrow\beta) \rightarrow (\textit{Term}\ \alpha\rightarrow\textit{Term}\ \beta) \) as for many other data types.
The type Term \(\beta\) might not even be inhabited: there are, for instance, no terms of type Term String.
Since the type argument of Term is not related to any component, we call Term a phantom type.

Hinze's definition of phantom type is different from what I would call a phantom type. Instead of calling Term a phantom type, I would refer to Integer in Term<Integer> as a phantom type, in the definition of Zero. In that case, although the return value of eval is an Integer, the type Integer does not play any other role in the structure of the Zero type. In other words, the type Integer does not appear on the right-hand side of Zero values; nor does Boolean appear on the right-hand side of IsZero, except in the return value of eval.