Explicit inequality evidence

[David Feuer]

On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <oleg.grenrus at iki.fi> wrote:
> First the bike shedding: I’d prefer /~ and :/~:.

Those are indeed better.

> new Typeable [1] would actually provide heterogenous equality:
>
> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
>     TypeRep a -> TypeRep b -> Maybe (a :~~: b)
>
> And this one is tricky, should it be:
>
> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
>    TypeRep a -> TypeRep b ->
>    Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b)
>
> i.e. how kind inequality would work?

I don't know. It sounds like some details of how kinds are expressed
in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe
we should punt and use heterogeneous inequality? That's over my head.

> I'm not sure about propagation rules, with inequality you have to be *very* careful!
>
> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear.
>
> I assume that in your rules, variables are not type families, otherwise
>
> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x where F x = ())
> other direction is true though.

I was definitely imagining them as first-class types; your point that
f x /~ f y => x /~ y even if f is a type family is an excellent one.

> Also:
>
> f x ~ a -> b, is true with f ~ (->) a, x ~ b.

Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just
leave out that bogus piece.

Thanks,
David Feuer