On 9/30/06, [EMAIL PROTECTED] <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
