[Haskell-cafe] Type equality proof

[Wolfgang Jeltsch]

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