Haskell Type Functions - Example Programs

{- a class for collections `c' with elements `Elem c' -}
class Col c where
  type Elem c
  isEmpty   :: c -> Bool
  add       :: c -> Elem c -> c
  head      :: c -> Elem c
  tail      :: c -> c

{- lists are collections -}
instance Col [e] where
  type Elem [e] = e
  isEmpty  =  Prelude.null
  add      =  Prelude.flip (:)
  head     =  Prelude.head
  tail     =  Prelude.tail

{- add all elements from one collection to another -}
addAll :: (Col c1, Col c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
addAll c1 c2
        | isEmpty c1  =  c2
        | otherwise   =  addAll (tail c1) (add c2 (head c1))

 {- type level natural numbers -}
data Zero
data Succ x

{- type level sum function -}
type family Sum n
type instance Sum Zero x     = x
type instance Sum (Succ x) y = Succ (Sum x y)

{- length-indexed vectors -}
data Vector elem len where
  VNil  :: Vector elem Zero
  VCons :: elem  -> Vector elem n -> Vector elem (Succ n)

{- vector concatenation -}
vconcat :: Vector e n -> e Vector e m -> Vector e (Sum n m)
vconcat VNil         l   = l
vconcat (VCons x xs) ys  = VCons x (vconcat xs ys)

 {- type level natural numbers -}
data Zero
data Succ x

{- abbreviations -}
type One = Succ Zero
type Two = Succ (Succ Zero)

{- type level sum function -}
type family Sum n
type instance Sum Zero x     = x
type instance Sum (Succ x) y = Succ (Sum x y)

{- wrapper for phantom types `a' and `b'
   which are not inhabited by values
-} 
data a := b  =  T

{- hypothesis -}
hypothesis :: Sum One One := Two
hypothesis = T

{- for equality of types -}
test :: (a := a) -> ()
test _ = ()

{- actual proof: type checks iff hypothesis holds -} 
proof :: ()
proof = test hypothesis