On 17 Mar 2009, at 21:44, Martijn van Steenbergen wrote:
Conor McBride wrote:
instance Category (:=:) where id = Refl Refl . Refl = Refl That and the identity-on-objects functor to sets and functions.
Not sure what you mean by this, Conor. Can you please express this in Haskell code?
Apologies for being glib and elliptic: filthy habit. That would be coerce :: (a :=: b) -> (a -> b) coerce Refl a = a taking arrows in the :=: category (aka the discrete category on *) to arrows in the -> category, preserving the objects involved. It captures the main useful consequence of an equation between types. I guess the other thing you need is resp :: (a :=: b) -> (f a :=: f b) resp Refl = Refl (any type constructor gives you a functor from the :=: category to itself). If you compose the two, you get Leibniz's characterization of equality -- that it's substitutive: subst :: a :=: b -> (f a -> f b) subst = coerce . resp Or you can start from subst and build the other two by careful instantiation of f. By the way, I see the motivation for your Eq1 class, which seems useful for the singleton GADTs which get used to give value-level representations to type-level stuff (combine with fmap coerce to get SYB-style cast), but I'm not quite sure where Eq2, etc, come in. Have you motivating examples for these? It's well worth striving for some sort of standard kit here. I should add that mentioning "equality" is the best way to start a fight at a gathering of more than zero type theorists. But perhaps there are fewer things to cause trouble in Haskell. So thanks for this, Conor