[Haskell-cafe] Type equality proof

Wolfgang Jeltsch g9ks157k at acme.softbase.org
Tue Mar 17 08:14:15 EDT 2009


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

Best wishes,
Wolfgang


More information about the Haskell-Cafe mailing list