[Haskell-cafe] Type equality proof
lrpalmer at gmail.com
Tue Mar 17 16:51:06 EDT 2009
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
> are closed, Martijn’s definition also says that two types can *only* be
> 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,
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe