Am Dienstag, 17. März 2009 21:51 schrieben Sie: > On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch wrote: > > 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 > > These two theorems should be in the package.
But they should not be data constructors. Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe