On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch < g9ks1...@acme.softbase.org> 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. > > > Best wishes, > Wolfgang > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
