Re: Explicit inequality evidence

Out of curiosity: where's the current type safety proof, and is it mechanized? Oleg On 13.12.2016 17:01, Richard Eisenberg wrote:

I've thought about inequality on and off for years now, but it's a hard nut to crack. If we want this evidence to affect closed type family reduction, then we would need evidence of inequality in Core, and a brand-spanking-new type safety proof. I don't wish to discourage this inquiry, but I also don't think this battle will be won easily.

Richard

...

On Dec 13, 2016, at 1:02 AM, David Feuer wrote:

On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus 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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs