[Haskell-cafe] Re: irrefutable patterns for existential types /
GADTs
Jim Apple
jbapple+haskell-cafe at gmail.com
Sat Sep 30 10:36:55 EDT 2006
On 9/30/06, apfelmus at quantentunnel.de <apfelmus at quantentunnel.de> wrote:
> data Eq a b where Refl :: Eq a a
>
> coerce :: Eq a b -> a -> b
> coerce ~Refl x = x
But this works well with Leibniz-style equality (
http://homepage.mac.com/pasalic/p2/papers/thesis.pdf ), because the
Equality proof/term is actually used:
data Equal a b = Equal (forall f . f a -> f b)
newtype Id x = Id { unId :: x}
coerce :: Equal a b -> a -> b
coerce ~(Equal f) x = unId (f (Id x))
Jim
More information about the Haskell-Cafe
mailing list