Phantom Types in Java

Typed programming languages (and I am channeling Frank Atanassow for the definition of "typed" versus "untyped") generally have (at least) two levels. Ignoring macros, partial evaluation, and other "meta-" schemes, typed languages have value expressions and type expressions; value expressions are the normal statements, values, and operators of the language, while type expressions express the types needed by the program. For most traditional typed languages, type expressions are not very interesting; in C, non-templated C++, pre-1.5 Java, and so on, type expressions are limited to literal types, the equivalent of 1, 2.0, and "Hello, world", and relatively simple subclass relationships (and subclassing is not subtyping).

Once you add generics, however, things get more interesting. Parametric polymorphism in languages such as ML, OCaml, post-1.5 Java, and templated C++ (-ish; the case for C++ templates is much more complicated) introduces type variables which make life much more interesting. Beyond the utility of type-safe collections, type variables enable techniques that provide some of the benefits of the Curry-Howard correspondence. Specifically, it allows you to easily specify more meaningful types, which correspond to more meaningful theorems when the program is viewed as a proof. In my opinion, the next step down this road actually compresses the type and value levels in dependently typed programming languages.

But back to parametric polymorphism, one relatively simple technique that has been floating around the typed functional language community for a while is phantom types (strangely, no wikipedia link). Phantom types, however, have not made it out of that ghetto into more mainstream languages which are perfectly capable of supporting them. Recently, however, I found the clearest, sweetest example of phantom types I have ever seen and I felt compelled to translate part of that example into Java, just to bask in the limelight. (Oddly enough, Jeff Foster's post does not focus on phantom types; he uses them to simplify the code in a Haskellization of a Clojure program. By translating part of it to Java and bringing it back to the JVM, I am probably closing some sort of karmic circle.)

A phantom type is a type that does not have any values or that is not primarily used for its values. Typically, if they have any values then those values have no structure; they are just used as a value-level tag somewhat like a value of an enumeration. Instead, the phantom type is used to create more complex type-level predicates that eliminate some sources of errors.

The key to the phantom type that makes it more than a type-level tag is the usage in another type with a more interesting structure. In the code below, the more interesting type is the class Vec, a 2 element vector used in Foster's orbital simulation. The key to this use is that the more-interesting type has a type variable that it never uses. In this case, the type variable V is never actually used in the class Vec; Vec is not a collection of V's, it never examines any value of V (which would be pointless anyway), its only instance variables are a couple of doubles, and in fact the only use of V is as a parameter to Vec in methods.

By the way, the code below has been highlighted and colored by the Pygments syntax highlighter. This is an experiment.



I am actually translating the version of Vec that I described in a comment to Foster's post. My extension is to add a constraint on V to limit it to a particular set of allowed arguments. By adding the interface Vector and constraining V to be a subtype of Vector, this code disallows Vec[Integer] or Vec[String] while allowing Vec[Position]. (In my commentary, I will use "[]" instead of "<>" since I'm a lazy sod.)


Position, Velocity and Force are the three types that are allowed for V, and are the three kinds of 2 element vectors needed by Uncle Bob's and Foster's simulations. Implementing the Vector interface tag is the second part of the constraint on V, and making these classes final and Vector protected are steps towards encapsulating the constraint and preventing V from being instantiated with an unexpected type. If that encapsulation is actually important, those steps should be taken further, but I actually have worse problems below that should be addressed first. That is, if that kind of strictness is necessary, which it is not.

Position, Velocity, and Force actually do have instances and specifically designated instances at that. (Actually, the specific instances are not special; any instance of Velocity should be equivalent to any other instance; the identity of the instances is unimportant.) These value-level tags are needed by the convert() methods described below. In the functional programming community, it is conventional to name the constructors of the types (which value-level objects are used in the same way as my instances) the same as the type, for example Force and Force in Foster's code. I find that confusing and have used the consistent name "tag" for my tag values. Strictly, the constructors for Position, Velocity, and Force should be private and so-forth, but as I mentioned above, that is not necessary.


The two instance variables x and y are the meat of the 2 element vector Vec class. I am implementing Vec as a pure-value class, with constant, final values. I personally think that is better style, although it does result in many more object creations. The improvement in the safety of the code is worth the extra allocation cost, which should be mitigated by a reasonably intelligent memory manager anyway.

For Vec's operations, there are two style options. I could implement each as static methods, which would be equivalent to Foster's code, or I could implement each as an instance method, which is more typical object-oriented style. I am somewhat undecided about the choice. On the one hand, the static approach is slightly more complicated to implement and slightly more verbose to use. It also does not match typical Java style. On the other hand, I seriously dislike the "x.add(y)" style. In such an expression, x and y should be of equivalent weight although that code makes x appear somehow special.

The code below implements vector addition in both styles for comparison. For the operations below, I decided to use the object-oriented, instance method style, because it more closely matches typical Java. As I write this, I am rethinking that decision, which does not seem very compelling.


As I mentioned above, this code has some known issues that are more high-priority safety problems. The big one is that the types of the vector should be used to limit the operations. For example, adding two positions is not meaningful. Two positions added do not produce another position, nor a velocity or a force. However, two positions can be subtracted, with a position viewed as a direction-and-distance. On the other hand, a position vector and a velocity vector can be added to produce a new position.


The addPV method shows this kind of type-level constraint and demonstrates the use of phantom types for Curry-Howard-style type predicates: addPV takes a position and a velocity and produces a new position vector. (Please ignore the actual implementation; I will discuses convert() below.)

Note that addPV has a funny name. I have to do that because of Java's type erasure. With erasure, the Java runtime cannot choose between a call to a method Vec[V] add(Vec[V],Vec[V]) and a method Vec[Position] add(Vec[Position],Vec[Velocity]).

convert() is the odd operation in Vec. It is fundamentally a C or Java cast; it does nothing to the value at compile- or run-time, it just changes the compile-time type associated with a value. However, a cast would be bad in user code, since a cast could cause a runtime error of the exact kind that typing is supposed to prevent. Since I do not intend to implement a host of methods like addPV(), I need to provide a convert limit casts to things that are reasonably safe. Specifically, a Vec of something to a Vec of something else.

My first attempt at convert(), commented out below, fundamentally does not work. convert(w) given Vec-something w, has no information about what the resulting something-else should be, especially since Java cannot do anything useful about return types. As a result, that convert is valid code, but does nothing useful.


In order to provide the type information about the result, I, like Foster, am using the value-level tags of the Vector subtypes. I am also providing both styles of covert. If you will now look at the implementation of addPV above, you will see how convert is used.


zero is another problem, similar to convert. It provides a single vector, (0,0), but needs to do so in the appropriate type. Neither of these implementations is completely satisfactory, although the method version does seem to do the right thing if the value is assigned to a variable with the right type. Ultimately, I probably need a zero method which takes a type tag argument, similar to convert.


The remaining operations needed by the simulation are below. They are not fundamentally interesting, but do illustrate that the type argument V is not used in Vec; hence the "phantom type".


If you really want to hurt yourself, look up some of the examples of using phantom types with the open/close/read/write file operations, where the phantom type is used to prevent read or write from being called on a closed file descriptor. Other, clearer, examples include capability-like access control for data structures and elevated-privileged operations.

At some point soon, I intend to return to my web application authentication saga, with a post (or more likely a series) on SAML. This may be your only warning. Duck and cover!

Postscript: It occurs to me that I did not give any examples of the use of the snazzy phantom-typed vector class. The following methods are from the translation of Foster's physics logic code:

private static double gravity(double m1, double m2, double r)
  {
    if (r == 0) { return 0; } else { return (m1 * m2) / (r*r); }
  }

  private Vec<Force> forceBetween(Obj other)
  {
    Vec<Position> p = other.position;
    // Compute the force between this and other
    double g = gravity(mass, other.mass, position.distance(p));
    // Compute the direction from this to other
    Vec<Position> direction = p.sub(position).unit();
    // Convert the direction to a force and scale by the force g
    return direction.convert(Force.tag).scale( g );
  }

Having to deliberately use the convert method to change a position vector to a force vector is both a (simple) safety check and a documentation step. Without the convert step, the method would not compile because the value of

direction.scale(g)

would have a type of Vec[Position].

Calculating the forces on all of the objects is handled by the following code:

private Obj accumulateForces(Collection<Obj> objs)
  {
    Vec<Force> totalForces = Vec.zero();
    for (Obj obj : objs)
    {
      if (!obj.equals(this))
      {
        totalForces = totalForces.add( forceBetween(obj) );
      }
    }
    return new Obj(position, velocity, totalForces, mass);
  }
  
  private static Collection<Obj> calculateForcesOnAll(final Collection<Obj> objs)
  {
    return Collections2.transform(objs, new Function<Obj,Obj>()
    {
      @Override public Obj apply(Obj obj) { return obj.accumulateForces(objs); }
    });
  }

(The transform method provided by the Google Guava library.)

Comments

thanks much for this post. can i talk you into hiring on once the angel funding comes through? (that's a joke at my own expense, i don't have any angel funding on the way, unfortunately.)

Raoul Duke
2010-07-01

also, i'm trying to figure out how to do http://ocaml.janestreet.com/?q=node/11 sorts of readonly vs. readwrite in java. but i also need frozen vs. unfrozen (different that the readonly vs. readwrite) so i'm quickly getting myself confused and lost. oh well.

Raoul Duke
2010-07-01

I don't actually have any angel funding, either. (Why does any phrase that starts with the word "angel" make me think there are devils involved?)

Tommy McGuire
2010-07-05

Instead of creating tag values, I think you could use the class values themselves, as is commonly done in the Java standard library. Everywhere you take a value type "U", you could instead take its class type "Class<U>", passing e.g. Position.class instead of Position.tag.

Anonymous
2012-10-28

Copyright © 2007-2017 Tommy M. McGuire