Am Dienstag, 17. März 2009 11:49 schrieb Yandex:
> data (a :=: a') where
> Refl :: a :=: a
> Comm :: (a :=: a') -> (a' :=: a)
> Trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')
I don’t think, Comm and Trans should go into the data type. They are not
axioms but can be proven. Refl says that each type equals itself. Since GADTs
are closed, Martijn’s definition also says that two types can *only* be equal
if they are actually the same.
Here are the original definition and the proofs of comm and trans. Compiles
fine with GHC 6.10.1.
data (a :=: a') where
Refl :: a :=: a
comm :: (a :=: a') -> (a' :=: a)
comm Refl = Refl
trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')
trans Refl Refl = Refl