{-# LANGUAGE TypeOperators, RankNTypes #-}

-- Code from section 12.7

module PhantomTypes ((:=:) (Proof), apply, 
                     refl, symm, trans, 
                     list, 
                     from, to) 
where

newtype a :=: b = Proof { apply :: forall phi . phi a -> phi b }

refl :: forall a . a :=: a
refl = Proof id

newtype Id t = Id { unId :: t }
from :: forall a b . (a :=: b) -> a -> b
from p = unId . apply p . Id

to :: forall a b . (a :=: b) -> b -> a
to p = from (symm p)

newtype Flip phi a b = Flip { unFlip :: phi b a }
symm :: forall a b . (a :=: b) -> (b :=: a)
symm p = unFlip (apply p (Flip refl))

trans :: forall a b c . (a :=: b) -> (b :=: c) -> (a :=: c)
trans p q = Proof (apply q . apply p)

newtype List phi a = List { unList :: phi [a] }
list :: forall a b . (a :=: b) -> ([a] :=: [b])
list p = Proof (unList . apply p . List)