Phantom type

A phantom type parameter appears in a type's declaration and in none of its constructors^[1]^[3]. It carries no data, is erased before run time, and exists only so the type checker can refuse to let two representationally identical values be confused. Leijen and Meijer used phantom types in 1999 to give types to SQL queries built as strings^[1]; they are now a standard technique for units, validation states, capabilities and protocol states, often called typestate^[6]. The technique depends on abstraction: the type is exported without its constructors, so the only way to obtain a value at a particular phantom type is through the functions the library provides. Fluet and Pucella showed that phantom parameters can also encode subtyping^[2]. In Haskell, a phantom parameter must be given the nominal role or coerce can change it freely^[5]. Rust marks such parameters with PhantomData^[8]. The difference from a GADT is what a pattern match learns.

§ 01

Example

Lengths in OCaml. Inside the module a length is a float; outside, its unit is part of its type.

(* The parameter 'u appears in no constructor: every length is a float at
   run time, and the unit exists only for the type checker. *)
module Length : sig
  type 'u t
  type metres
  type feet
  val metres : float -> metres t
  val feet : float -> feet t
  val add : 'u t -> 'u t -> 'u t
  val to_metres : feet t -> metres t
  val value : 'u t -> float
end = struct
  type 'u t = float
  type metres
  type feet
  let metres x = x
  let feet x = x
  let add = ( +. )
  let to_metres x = x *. 0.3048
  let value x = x
end

Using it.

open Units

Running it.

3304.8 metres

Adding metres to feet.

open Units
let total = Length.add (Length.metres 3000.) (Length.feet 1000.)

The compiler's error.

File "units_bad.ml", line 2, characters 45-64:
2 | let total = Length.add (Length.metres 3000.) (Length.feet 1000.)
                                                 ^^^^^^^^^^^^^^^^^^^
Error: This expression has type Units.Length.feet Units.Length.t
       but an expression was expected of type
         Units.Length.metres Units.Length.t
       Type Units.Length.feet is not compatible with type Units.Length.metres

Nothing in the representation distinguishes the two units, and the conversion to_metres is an ordinary multiplication. The guarantee comes from the signature: 'u t is abstract, so outside the module the only lengths are those built by metres and feet.

§ 02

How it works

Email Unchecked and Email Checked are different types with one representation. The library provides validate as the only way from one to the other; in Haskell, coerce is a second way unless the parameter is given the nominal role.

A phantom parameter adds distinctions between types that the representation does not make. Three things make it work. The parameter must appear in the type, so that $τ α$ and $τ β$ are different types when $α \neq = β$ . The type must be abstract, so that clients cannot build a value at an arbitrary instantiation. And the library's functions must fix the parameter in their signatures, which is how the invariants are stated: validate : Email Unchecked -> Maybe (Email Checked) is the only producer of checked addresses.

Since the parameter is erased, there is no run-time cost and no run-time check; everything is decided by type checking. The corresponding limitation is that the type checker knows only what the signatures say: a function that could produce a value at the wrong phantom type, because it is inside the abstraction boundary, is trusted.

§ 03

Typed embedded languages

Leijen and Meijer introduced phantom types to type an embedded query language^[1]. Queries are built as SQL strings, but each expression carries the SQL type of its result as a phantom parameter, so the combinators can accept only well-typed operands.

A fragment of a typed SQL builder.

-- Leijen and Meijer's embedded query language: an expression is a string
-- of SQL, and the phantom parameter records the SQL type it denotes.
newtype Expr a = Expr String
 
column :: String -> Expr a
column = Expr
 
int :: Int -> Expr Int
int = Expr . show
 
str :: String -> Expr String
str s = Expr ("'" ++ s ++ "'")
 
(.+.) :: Expr Int -> Expr Int -> Expr Int
Expr a .+. Expr b = Expr ("(" ++ a ++ " + " ++ b ++ ")")
 
(.==.) :: Expr a -> Expr a -> Expr Bool
Expr a .==. Expr b = Expr ("(" ++ a ++ " = " ++ b ++ ")")
 
(.&&.) :: Expr Bool -> Expr Bool -> Expr Bool
Expr a .&&. Expr b = Expr (a ++ " AND " ++ b)
 
where_ :: String -> Expr Bool -> String
where_ table (Expr cond) = "SELECT * FROM " ++ table ++ " WHERE " ++ cond
 
age :: Expr Int
age = column "age"
 
name :: Expr String
name = column "name"
 
main :: IO ()
main = putStrLn (where_ "people" ((age .+. int 1 .==. int 30) .&&. (name .==. str "Ada")))

Running it.

SELECT * FROM people WHERE ((age + 1) = 30) AND (name = 'Ada')

Comparing an integer column with a string.

import Sql
query = where_ "people" (age .==. str "thirty")

GHC's error.


sql_bad.hs:2:35: error:
    * Couldn't match type `[Char]' with `Int'
      Expected: Expr Int
        Actual: Expr String
    * In the second argument of `(.==.)', namely `str "thirty"'
      In the second argument of `where_', namely
        `(age .==. str "thirty")'
      In the expression: where_ "people" (age .==. str "thirty")
  |
2 | query = where_ "people" (age .==. str "thirty")
  |                                   ^^^^^^^^^^^^

§ 04

Subtyping with phantom types

A phantom parameter that is itself a set of capabilities can encode subtyping. Fluet and Pucella showed how to encode subtyping hierarchies in the parameters of phantom types in ML^[2]; in OCaml, polymorphic variants make it direct. A handle's parameter lists the operations it permits, and a function that needs only reading accepts any handle whose list includes `Read.

Read and write capabilities as phantom polymorphic variants.

(* Capabilities as phantom polymorphic variants (Fluet and Pucella):
   a handle's parameter lists what it may be used for, and subtyping on
   variants lets a read-write handle go wherever a read handle is needed. *)
module File : sig
  type 'cap t
  val open_rw : string -> [ `Read | `Write ] t
  val read_only : [> `Read ] t -> [ `Read ] t
  val read : [> `Read ] t -> string
  val write : [> `Write ] t -> string -> unit
end = struct
  type 'cap t = { name : string; contents : Buffer.t }
  let open_rw name = { name; contents = Buffer.create 16 }
  (* the same file, retyped: 'cap is phantom, so this is just a copy of
     the record *)
  let read_only f = { name = f.name; contents = f.contents }
  let read f = Buffer.contents f.contents
  let write f s = Buffer.add_string f.contents s
end

Using a read-write handle and a read-only view of it.

open Perms

Running it.

started; ok

Writing through the read-only view.

open Perms
let () = File.write (File.read_only (File.open_rw "log")) "oops"

The compiler's error.

File "perms_bad.ml", line 2, characters 20-57:
2 | let () = File.write (File.read_only (File.open_rw "log")) "oops"
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type [ `Read ] Perms.File.t
       but an expression was expected of type [> `Write ] Perms.File.t
       The first variant type does not allow tag(s) `Write

§ 05

Roles and coercions

Haskell's coerce converts between types with the same representation at no cost, and its safety is tracked by roles^[5]. A type parameter that is not used in the representation gets the phantom role, which means coerce may change it to anything, even when the constructor is not exported. For a phantom type used to enforce an invariant, that is a hole.

A validation library that hides its constructor.

module Email (Email, Unchecked, Checked, unchecked, validate, send) where
 
data Unchecked
data Checked
 
-- The constructor is not exported: the only way to get an Email Checked
-- is through validate.
newtype Email s = Email String
 
unchecked :: String -> Email Unchecked
unchecked = Email
 
validate :: Email Unchecked -> Maybe (Email Checked)
validate (Email s) = if '@' `elem` s then Just (Email s) else Nothing
 
send :: Email Checked -> String
send (Email s) = "sent to " ++ s

A client that bypasses validate.

import Data.Coerce (coerce)
import Email
 
main :: IO ()
main = do
  print (fmap send (validate (unchecked "[email protected]")))
  print (fmap send (validate (unchecked "nobody")))
  -- The parameter s has the phantom role, so coerce may change it even
  -- though the constructor is hidden:
  putStrLn (send (coerce (unchecked "nobody")))

Running it: an address that failed validation is sent anyway.

Just "sent to [email protected]"
Nothing
sent to nobody

The fix is a role annotation, type role Email nominal, which makes Email Unchecked and Email Checked non-coercible outside the module.

The same client against the annotated library.

type role Email nominal
newtype Email s = Email String

GHC's error.


roles_safe.hs:10:19: error:
    * Couldn't match type `Unchecked' with `Checked'
        arising from a use of `coerce'
    * In the first argument of `send', namely
        `(coerce (unchecked "nobody"))'
      In the first argument of `putStrLn', namely
        `(send (coerce (unchecked "nobody")))'
      In a stmt of a 'do' block:
        putStrLn (send (coerce (unchecked "nobody")))
   |
10 |   putStrLn (send (coerce (unchecked "nobody")))
   |                   ^^^^^^

§ 06

Phantom types and GADTs

The difference from a GADT is what happens on the way out. A phantom parameter constrains callers but tells a pattern match nothing: matching on a length's constructor learns no more about its unit than was already known, because every constructor has the same fully polymorphic result type. A GADT constructor fixes its type index, so matching on it recovers the index, which is why a GADT branch can return a value at a type that depends on the constructor and a phantom-typed match cannot^[3]^[4]. GADTs are sometimes called first-class phantom types for this reason^[4].

§ 07

Other uses

Typestate, in which the type of a resource records its protocol state, such as a file being open or closed or a builder having set its required fields, was proposed by Strom and Yemini in 1986^[6] and is commonly encoded with phantom parameters, especially in Rust, whose PhantomData marker declares a parameter that the fields do not use^[8]. Other uses include tagging identifiers with the kind of entity they refer to, tracking whether a string has been escaped, and tagging indices with the array they are valid for. Units of measure are a common example, although F# builds them into the type system, following Kennedy's dimension types^[7], so that units can be multiplied and divided, which phantom parameters alone cannot express.

§ 08

History

Leijen and Meijer introduced the term in 1999, for the typed query combinators of their embedded compiler for SQL^[1]. Hinze's “Fun with phantom types” of 2003 and Cheney and Hinze's “First-class phantom types” described the extension to type indices that pattern matching can recover, which became GADTs^[3]^[4]. Fluet and Pucella gave the encoding of subtyping in 2006^[2]. GHC's roles, introduced with coerce in 2014, made the phantom role explicit and added role annotations^[5].