[Haskell-cafe] Type equality proof
Wolfgang Jeltsch
g9ks157k at acme.softbase.org
Wed Mar 18 06:20:40 EDT 2009
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
More information about the Haskell-Cafe
mailing list