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:

`(*The empty list*)`

let nil=[]

(*Appends an element in front of a list*)

let cons e l = e::l

(*Converts two list of same sizes to a list of couples *)

let combine = List.combine

let nil=[]

(*Appends an element in front of a list*)

let cons e l = e::l

(*Converts two list of same sizes to a list of couples *)

let combine = List.combine

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:

`type zero`

type 'length succ

type 'length succ

0 is represented by the type `zero`, 1 by
`succ zero`,
2 by `succ succ zero`
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 being `'a list` our list type is now:

`type ('a,'length) t`

where `'length`
represents the length of the list. Giving types to our previous functions is
now straightforward:

`val nil:('a,zero) t`

val cons:'a -> ('a,'length) t -> ('a,('length succ)) t

val combine:('a,'length) t -> ('b,'length) t -> (('a*'b),'length) t

val cons:'a -> ('a,'length) t -> ('a,('length succ)) t

val combine:('a,'length) t -> ('b,'length) t -> (('a*'b),'length) t

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:

`module DepList:`

sig

type zero

type 'length succ

type ('a,'length) t

val nil:('a,zero) t

val cons:'a -> ('a,'length) t -> ('a,('length succ)) t

val toList:('a,'length) t -> 'a list

val combine:('a,'length) t -> ('b,'length) t -> (('a*'b),'length) t

end

=

struct

type zero

type 'b succ

type ('a,'length) t='a list

let nil=[]

let cons e l = e::l

let combine = List.combine

let toList l = l

end

sig

type zero

type 'length succ

type ('a,'length) t

val nil:('a,zero) t

val cons:'a -> ('a,'length) t -> ('a,('length succ)) t

val toList:('a,'length) t -> 'a list

val combine:('a,'length) t -> ('b,'length) t -> (('a*'b),'length) t

end

=

struct

type zero

type 'b succ

type ('a,'length) t='a list

let nil=[]

let cons e l = e::l

let combine = List.combine

let toList l = l

end

## Testing it all

And it's now time to play with our library...

`# open DepList;;`

# let a=cons 5 (cons 6 nil);;

val a : (int, DepList.zero DepList.succ DepList.succ) DepList.t = <abstr>

# toList a;;

- : int list = [5; 6]

# let b=cons "a" nil;;

val b : (string, DepList.zero DepList.succ) DepList.t = <abstr>

# combine a b;;

Characters 10-11:

combine a b;;

^

This expression has type (string, DepList.zero DepList.succ) DepList.t

but is here used with type

(string, DepList.zero DepList.succ DepList.succ) DepList.t

# let a=cons 5 (cons 6 nil);;

val a : (int, DepList.zero DepList.succ DepList.succ) DepList.t = <abstr>

# toList a;;

- : int list = [5; 6]

# let b=cons "a" nil;;

val b : (string, DepList.zero DepList.succ) DepList.t = <abstr>

# combine a b;;

Characters 10-11:

combine a b;;

^

This expression has type (string, DepList.zero DepList.succ) DepList.t

but is here used with type

(string, DepList.zero DepList.succ DepList.succ) DepList.t

That's right we've just statically caught an error because `combine` was
called with two lists of different lengths!

## Conclusion

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.

## 5 comments:

Merci pour ça!

It helped me understand phantom types a bit better. It's still quite a new thing for me and it will take a while for me to get my head around it.

Thanks for taking the time to write about the topic!

Well I'm glad glad it turned out useful for someone. In practice they are rarely useful and require a rather big dose of aspirin before getting good results.

Thanks for this article: very interesting and clear.

Can you suggest me some other sources of information about phantom types?

the est article I know of is, funnily enough, "fun with phantom types" by ralph hinze. I've just added a new post on the subject.

Prenuptial agreements are also intercheangeably referred to stength

during the sequestration litigate, so we powerfully urge that you keep recitation this

article. The lawsuit to try and salvage your spousal relationship and family.

The financial aspect is especially these days can cost from $20,

000-40,000. If a polyamorous aliveness of multiple lovers or a train of through and through sequestration or tiddler related matters, At that place are several coordination compound areas of federal and

country law that hold specifically to your cause.

my page; Justin Bieber

Post a Comment