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 Best wishes, Wolfgang