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.
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.
active directory applied formal logic ashurbanipal authentication books c c++ comics conference continuations coq data structure digital humanities Dijkstra eclipse virgo electronics emacs goodreads haskell http java job Knuth ldap link linux lisp math naming nimrod notation OpenAM osgi parsing pony programming language protocols python quote quotes R random REST ruby rust SAML scala scheme shell software development system administration theory tip toy problems unix vmware yeti
Member of The Internet Defense League
Site proudly generated by Hakyll.