[Haskell-cafe] Type equality proof

[Conor McBride]

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