[Haskell-cafe] Type equality proof

[Luke Palmer]

On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch <
g9ks157k at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090317/87d97d56/attachment.htm