Phantom types are a nifty trick: types are used to store additional information during the type-checking pass. These types have no implementations (there are no values actually having these types) but are still used as type parameter to tag values. This additional info is then used by the type system to statically ensure some conditions are met. As, I'm guessing this is all getting rather intriguing (or confusing) I propose to step through a very simple example.
Without phantom types
Let's start out with a very basic library to handle lists:
Combine needs both of its arguments to be of the same length. This is typically a job for dependent types (i.e. types depending on a value) where list length would be encoded in their types. Ocaml doesn't have dependant type but we'll see how to leverage the type inference mechanism to encode lengths.
Encoding the length
Since our types cannot contain values we need to find a way to code integers in our type system. We will using an encoding based on Peano's axiom's:
0 is represented by the type, 1 by , 2 by etc... There exist no values having these types: they are empty.
Using the phantom type
The previous type will be the "phantom type": it will be used to encode additional info but won't represent the type of any actual object.
The idea here is to make our lists depend on that type to store the length info. Instead of beingour list type is now:
whererepresents the length of the list. Giving types to our previous functions is now straightforward:
and since under the hood we are using standard OCaml's list, converting from our list to a normal list is a plain identity. We'll now wrap everything in a nice module in order to hide the internals:
Testing it all
And it's now time to play with our library...
That's right we've just statically caught an error becausewas called with two lists of different lengths!
Phantom types are a fun hack to play with, alas they are very restrictive and rarely useful. Their big brothers (GADT's and dependant types) require specific type systems and are tricky to groke.