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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
