Type-Level Programming In Haskell - Phantom Types

By Steven Leiva

N.B. This post is tagged with Note. This means that the post is not meant for external consumption. Instead, it is a "stream of conciousness" or "scratchpad" as I learn about new topics.

Terms, Types, and Kinds

One of the foundations of understanding type-level programming in Haskell is the realization that Haskell's type system divides itself into three separate layers - the term layer; the type layer; and the kind layer.

Just like the terms a, b, c are grouped into the type Char, types themselves are grouped together into something called a kind. The kind of Char, for example, is *.

Bridging Terms, Types, and Kinds

The separation between terms, types, and kinds is foundational for understanding type-level programming. Type-level programming simply means that instead of operating on terms, we are going to be operating on types. Types are useful only to the extent that they inform the behavior of our system at runtime. Therefore, we must be able to bridge the the term layer and the type layer. There must be facilities to take information at one layer and have that impact the other layer.

This idea of passing information between these two layers of the type system is so commonplace that we might not even be aware of it. For example, let's pass some information from the term layer to the type layer:

Nothing :: Maybe Int

Using a type annotation, we can tell type system that our Nothing data constructor has the type Maybe Int. We are now passing type information from the term layer to the type layer. As you can imagine, only type information can be passed into the type layer.

What about passing information from the type layer to the term layer? This is done via typeclasses! For example, we can think about the instance of Show Int as a function (loosely speaking) going from the type Int to the value Int -> String. In the discussion of phantom types below, we will see a more explicit example of using typeclasses to bridge the type and term layers.

Phantom Types

Let's imagine for a second that we are building the navigation software for a space craft. We want to make sure that we never mix up our units. A potential attempt at this might be as follows:

data Distance = Miles Double | Kilometers Double

distanceInMiles :: Distance
distanceInMiles = Miles 10

distanceInKilometers :: Distance
distanceInKilometers = Kilometers 10

How does this save us from mixing up our units? Well, in order to access the double, we have to pattern match on the data constructors, making it obvious what units we are dealing with. But there are two problems here:

The unit information exists only at the term layer - the type system is not aware of it.
It becomes increasingly difficult to perform simple operations values of type Distance a
No guarantees that something untoward won't happen outside of addDistances.

To the first point:

addDistances :: Distance -> Distance -> Distance
addDistances first second = ...

Notice how, at the type layer, we have no information about the units.

To the second point, let's actually implement addDistances:

addDistances :: Distance -> Distance -> Distance
addDistances (Miles x) (Miles y) = Miles (x + y)
addDistances (Kilometers x) (Kilometers y) = Kilometers (x + y)
addDistances (Miles x) (Kilometers y) = Kilometers (x * 1.60934 + y)
addDistances kilometers miles = addDistances miles kilometers

If we add more data constructors to the Distance type, we'd be in a mess of trouble!

Finally, to the third point, we have no guarantee that a client of Distance won't do the following:

distanceToDouble :: Distance -> Double
distanceToDouble (Miles x) = x
distanceToDouble (Kilometers y) = y

distanceToDouble (Miles x) + distanceToDouble (Kilometers y)

We could always use Haskell's combinator pattern and make Distance an absract data type, but that leads to its own issues.

Phantom Types

Let's go back to our original problem. We want to create navigation software in such a way that avoids the mixup of units. We saw a potential solution, where the unit information was carried along at the term level. This time, let's enlist the type system to help us ensure we don't mix up our types by encoding the unit information at the type level. We can do this using Phantom Types:

data Mile
data Kilometer

newtype Distance a = Distance { unDistance :: Double }

Let's pause here to understand what the above code snippet is doing.

First, we are declaring two new data types - Mile and Kilometer. Notice that these data types have no data constructors. As a result, we cannot create values of type Mile or Kilometer.

Secondly, we are creating a new type constructor - Distance. Distance is parameterized by a type variable. Crucially, because this type variable does not appear on the right-hand side of the data declaration, the type variable (a) is known as a phantom type. In more esoteric terms, you might here someone say that the type variable has not witness at the term level. What good is it then? Well, it might be phantom at the value level, but it is alive and well at the type level! The types Distance Mile and Distance Kilometer are two very distinct types. Using phantom types, our type system is now aware that distance values have units!

Operating on Distance

Now that we the unit have been promoted to the type level, the compiler can ensure we don't mix up our units. Let's how we would go about operating on our Distance a values.

Remember that our Distance type constructor is just a wrapper around an underlying value of type Double. For "number like" operations, we just want to unwrap the Double, perform the operation, and wrap things up again in our Distance data constructor. We can use GeneralizedNewtypeDeriving to have Haskell derive this exact instance for us:

newtype Distance a = Distance { unDistance :: Double } deriving (Num, Show)

a :: Distance Mile
a = Distance 20

b :: Distance Mile
b = Distance 20

a + b
=> Distance { unDistance = 40.0 }

However, if we attempt to add two distances with different units, we get a type error:

a :: Distance Mile
a = Distance 20

b :: Distance Kilometer
b = Distance 20

a + b
=> Couldn't match type ‘Kilometer’ with ‘Mile’

twentyMiles = (Distance 10 :: Distance Mile) + (Distance 10 :: Distance Kilometer)

Working with Information at the Type Level

So we've gained some type safety. The compiler is helping us ensure that we do not mix up types, and working with distances of the same type is fairly painless

we rely on the way that Doubles work.

But what about working with distances with two different units? What if we wanted to, in fact, add miles and kilometers together? Well, we know we can write the functions:

addMilesToKilometers :: Distance Mile -> Distance Kilometer -> Distance Kilometer
addMilesToKilometers distanceInMiles distanceInKilometers = Distance (unDistance distanceInKilometers + unDistance distanceInMiles 1.60934)

addKilometersToMiles :: Distance Kilometer -> Distance Mile -> Distance Mile
addKilometersToMiles distanceInKilometers distanceInMiles = Distance (unDistance distanceInMiles + unDistance distanceInKilometers * 0.621371)

Now, if we have two distances - one in miles and another in kilometers - we know whether we need to choose addKilometersToMiles or addKilometersToMiles based on the information at the type level. As we've said earlier, going for information from the type level to the term-level requires a typeclass:

class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b

instance Add Mile Kilometer where
  addDistance = addMilesToKilometers

instance Add Kilometer Mile where
  addDistance = addKilometersToMiles

instance Add Mile Mile where
  addDistance = +

instance Add Kilometer Kilometer where
  addDistance = +

Lessons for the Novice Type-Level Programmer

The code snippet above contains a multitude of tidbits for the novice type-level programmer. Let's start with the typeclass declaration:

class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b

Notice how we apply the type variable a and b to the Distance type constructor in our declaration of the typeclass. Thus, even though Distance does not appear anywhere in our typeclass declaration's head, we can only call addDistance to values of type Distance. Remember, we need to decide between using addMilesToKilometers or addKilometersToMiles. The only information we need to make this choice is the units of the two distance values we are adding. And that is precisely the information that our Add class is "asking" for.

Now, let's at one of our instance declarations:

instance Add Mile Kilometer where
  addDistance = addMilesToKilometers

Notice how the typeclass instance is used to go from type level information - the units of the distances that we are adding - to term level information, namely, a function from two distances (mile and kilometer) to a single distance in kilometers.

What Have We Gained

Our first declaration of Distance was conceptually simple, fairly type-safe, but hard to work with and hard to extend.

Our "phantom type" version of distance was conceptually more complex, just as type-safe, and we didn't sacrifice much in the way of ergonomics:

let tenMiles = Distance 10 :: Distance Mile
let tenKilometers = Distance 10 :: Distance Kilometer

addDistance tenMiles tenMiles
=> Distance {unDistance = 20.0} :: Distance Mile

addDistance tenKilometers tenKilometers
=> Distance {unDistance = 20.0} :: Distance Kilometer

addDistance tenMiles tenKilometers
=> Distance {unDistance = 26.0934} :: Distance Kilometer

addDistance tenKilometers tenMiles
=> Distance {unDistance = 16.21371} :: Distance Mile

Complete Module

The code snippet below is a complete module of the lessons learned here. Notice that we declare a Convert typeclass that lets us convert from miles to kilometers or kilometers to miles. If you load this module in GHCI, you can run the main action and see the tests pass (hopefully!).

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module IntroToTypeLevelProgramming.PhantomTypes where

import           Test.Hspec

newtype Distance a = Distance { unDistance :: Double } deriving (Eq, Show, Num)

data Mile

data Kilometer

milesToKilometers :: Distance Mile -> Distance Kilometer
milesToKilometers distanceInMiles = Distance (unDistance distanceInMiles * 1.60934)

kilometersToMiles :: Distance Kilometer -> Distance Mile
kilometersToMiles distanceInKilometers = Distance (unDistance distanceInKilometers * 0.621371)

class Convert a b where
  convert :: Distance a -> Distance b

-- instance Convert (Distance Mile) (Distance Kilometer); we'd be passing
instance Convert Mile Kilometer where
  convert = milesToKilometers

instance Convert Kilometer Mile where
  convert = kilometersToMiles

class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b

instance Add Mile Kilometer where
  addDistance distanceInMiles distanceInKilometers = convert distanceInMiles + distanceInKilometers

instance Add Kilometer Mile where
  addDistance distanceInKilometers distanceInMiles = convert distanceInKilometers + distanceInMiles

instance Add Mile Mile where
  addDistance = (+)

instance Add Kilometer Kilometer where
  addDistance = (+)

main :: IO ()
main = hspec $ do
  it "converts from miles to kilometers" $ do
    let distanceInMiles = Distance 10 :: Distance Mile
    (convert distanceInMiles :: Distance Kilometer) `shouldBe` Distance 16.0934
  it "converts from kilometers to miles" $ do
    let distainceInKilometers = Distance 10 :: Distance Kilometer
    (convert distainceInKilometers :: Distance Mile) `shouldBe` Distance 6.21371
  it "can add miles to kilometers" $ do
    let distanceInKilometers = Distance 10 :: Distance Kilometer
        distanceInMiles = Distance 10 :: Distance Mile
    (addDistance distanceInMiles distanceInKilometers) `shouldBe` (Distance 26.0934 :: Distance Kilometer)
  it "can add kilometers to miles" $ do
    let distanceInKilometers = Distance 10 :: Distance Kilometer
        distanceInMiles = Distance 10 :: Distance Mile
    (addDistance distanceInKilometers distanceInMiles) `shouldBe` (Distance 16.21371 :: Distance Mile)