scvalex.net

15. Phantom Types

There are two ways of looking at the type-system of a language: as a set of rules which must be followed for the program to compile, and as a tool to make code more expressive. In this post, we talk about phantoms types, which is one way of doing the latter.

To quote the Hakell Wiki:

A phantom type is a parametrised type whose parameters do not all appear on the right-hand side of its definition.

That’s a bit obtuse, but an example will make it clear:

data Zero = Zero
data Succ a = Succ a

data Vec n a = Vec [a]

type Vec2d a =
    Vec (Succ (Succ Zero)) a
type Vec3d a =
    Vec (Succ (Succ (Succ Zero))) a

transpose :: Vec2d a -> Vec2d a
add :: Vec n a -> Vec n a -> Vec n a

Zero and Succ are the usual encoding of Peano Numbers. Vec n a represents an n-dimensional vector with elements of type a – note that n does not appear on the right-hand side of the data declaration. Using these types, we define Vec2d and Vec3d such that they cannot be unified with each other. Now, we can define transpose such that it only works on 2-dimensional vectors, and add such that it only works on vectors with the same size. Using these the wrong way leads to compile-time errors; so, we’ve gotten more static checks out of the language.

There are many other things you can do with phantom types: You can use them to implement a type-safe variant of the Builder design pattern in Scala, or in Haskell. You can use them to embed a language in Haskell, and ensure that expressions are well-formed. You can use them to distinguish between two variants of the same data-structure – in this case, validated and unvalidated input have different types, but share the same definition. You can use them to ensure that needed operations are executed in the right order. You can even use them to enforce access control on data structures.

These aren’t just a Haskell idiom; you can use phantom types in Java, Scala, OCaml, and most languages that have type systems.