F#antom Treats for Halloween?

Last time we created our Phantom type and successfully converted it to a list.  Let’s quickly review the goals of our Phantom type before pushing forward. 

 

The primary goal is to trick the compiler into catching discrepancies in lengths between lists. The length parameter of our Phantom type is never used by the consumer of our list library.  It is purely a static compile time phenomena used to prevent run time problems.  Hence, the name phantom.

 

The Phantom Library

 

Because our type parameters cannot have values, we need a way to represent integers in our type system.  Let’s add the following types.

 

type Zero

type Succ<’length>

 

type Zero = Zero of int

type Succ<’length> = Succ of int

 

Zero represents the integer 0, Succ<Zero> represents 1,  Succ<Succ<Zero>> represents 2 and so on.  We can now use these types as values to the length parameter of our Phantom<’a,’length> type.  Let’s start with a definition for nil. 

 

val nil : Phantom<’a,Zero>

 

let nil =

    let nil_1 = Phantom []

    nil_1<’a, Zero>

 

We create a new empty list, construct it as our Phantom type, then return it with Zero as the length parameter.  Let’s up the mind bending quotient and move on to a definition of cons.

 

val cons : ‘a -> Phantom<’a,’length> -> Phantom<’a,Succ<’length>>

 

let cons (e : ‘a) (l : Phantom<’a,’length>) =

    let cons_1 = e :: (toList l)

    let cons_2 = Phantom cons_1

    cons_2<Succ<’length>>

 

We deconstruct our Phantom type into a list, do the cons operation, wrap it back up in a Phantom type, then return it with Succ<’length> as the length parameter.  Now our combine function.

 

val combine : Phantom<’a,’length> -> Phantom<’b,’length> -> Phantom<’a*’b,’length>

 

let combine (al : Phantom<’a,’length>) (bl : Phantom<’b,’length>)=

    let combine_1 = List.zip (toList al) (toList bl)

    let combine_2 = Phantom combine_1

    combine_2<’length>

 

We deconstruct our two lists, run the zip function, construct our combined list into a phantom type, and return the list with length as the length parameter.  So our library is complete.

 

These definitions appear self evident once they are complete, but I must admit to struggling to come up with the definitions.  Keeping the types straight in your head is not easy, and explicit annotation have to be used or else the type inference algorithm infers new generic types.

 

Trick or Treat?

 

Now that the hard work is done let’s see if we have a Halloween brought us a trick or a treat.

 

//val a : Phantom<int,Succ<Succ<Zero>>>

let a = cons 1 (cons 2 nil)

 

//[1; 2]

let r = toList a

 

//val b : Phantom<string,Succ<Succ<Zero>>>

let b = cons “a” (cons “b” nil)

 

//[(1,"a"); (2,"b")]

let r1 = toList (combine a b)

 

Our combine function works as expected, lists a and b can be combined since they are both of the same length.

 

// Type mismatch. Expecting a Phantom<string,Succ<Succ<Zero>>>

// but given Phantom<string,Succ<Zero>>.

// The type Succ<Zero> does not match the type ‘Zero’.

let c = cons “a” nil

let r2 = toList (combine a c)

 

But when we try to combine a list of length 1 with a list of length 2 the compiler statically catches the problem.  Basically our length parameter expands into the following definitions.

 

0 = Zero

1 = Succ<Zero>

2 = Succ<Succ<Zero>>>

 

Succ<Zero> is obviously not equal to Succ<Succ<Zero>>> and the compiler recognizes this.  So Halloween brought us a treat this year, are you brave enough to use them in your code?

 

Full Source

 

#light

 

module DepList

     type Zero

     type Succ<’length>

     type Phantom<’a,’length>

     val toList : Phantom<’a,’length> -> ‘a list

     val nil : Phantom<’a,Zero>

     val cons : ‘a -> Phantom<’a,’length> -> Phantom<’a,Succ<’length>>

     val combine : Phantom<’a,’length> -> Phantom<’b,’length> -> Phantom<’a*’b,’length>

 

#light

 

module DepList

 

type Zero = Zero of int

type Succ<’length> = Succ of int

type Phantom<’a,’length> = Phantom of ‘a list

let toList (l : Phantom<’a,’length>) =

    match l with

    | Phantom l -> l

let nil =

    let nil_1 = Phantom []

    nil_1<’a, Zero>

let cons (e : ‘a) (l : Phantom<’a,’length>) =

    let cons_1 = e :: (toList l)

    let cons_2 = Phantom cons_1

    cons_2<Succ<’length>>

let combine (al : Phantom<’a,’length>) (bl : Phantom<’b,’length>)=

    let combine_1 = List.zip (toList al) (toList bl)

    let combine_2 = Phantom combine_1

    combine_2<’length>

 

#light

 

open DepList

 

//val a : Phantom<int,Succ<Succ<Zero>>>

let a = cons 1 (cons 2 nil)

 

//[1; 2]

let r = toList a

 

//val b : Phantom<string,Succ<Succ<Zero>>>

let b = cons “a” (cons “b” nil)

 

//[(1,"a"); (2,"b")]

let r1 = toList (combine a b)

 

// Type mismatch. Expecting a Phantom<string,Succ<Succ<Zero>>>

// but given Phantom<string,Succ<Zero>>.

// The type Succ<Zero> does not match the type ‘Zero’.

let c = cons “a” nil

let r2 = toList (combine a c)

 

printfn “%A” r1

System.Console.ReadLine()