Use of phantom types for static validation of list length
// Phantom types - http://web.archive.org/web/20100615031841/http://blog.matthewdoig.com/?p=138 | |
// Rather than DUs, just use simple marker interfaces | |
type Zero = interface end | |
type Succ<'length> = interface end | |
type Phantom<'a,'length> = Phantom of 'a list | |
let toList (Phantom l) = l | |
let nil = Phantom [] : Phantom<_,Zero> | |
// 'a -> Phantom<'a,'length> -> Phantom<'a,Succ<'length>> | |
let cons (e : 'a) (l : Phantom<'a,'length>) = | |
let cons1 = e :: (toList l) | |
Phantom cons1 : Phantom<_,Succ<'length>> | |
// Phantom<'a,'length> -> Phantom<'b,'length> -> Phantom<'a*'b,'length> | |
let combine (al : Phantom<'a,'length>) (bl : Phantom<'b,'length>)= | |
let combine1 = List.zip (toList al) (toList bl) | |
Phantom combine1 : Phantom<_,'length> | |
//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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment