Explicit inequality evidence

[Oleg Grenrus]

Hi,

I was thinking about (and almost needing) inequality evidence myself, so I’m :+1: to exploration.

First the bike shedding: I’d prefer /~ and :/~:.

--

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'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.

Also:

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

--

Oleg

- [1]: https://github.com/ghc-proposals/ghc-proposals/pull/16

> On 13 Dec 2016, at 06:34, David Feuer <david.feuer at gmail.com> wrote:
> 
> According to Ben Gamari's wiki page[1], the new Typeable is expected to offer
> 
> eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
> 
> Ideally, we'd prefer to get either evidence of equality or evidence of inequality. The traditional approach is to use Dec (a :~: b), where data Dec a = Yes a | No (a -> Void). But  a :~: b -> Void isn't strong enough for all purposes. In particular, if we want to use inequality to drive type family reduction, we could be in trouble.
> 
> I'm wondering if we could expose inequality much as we expose equality. Under an a # b constraint, GHC would recognize a and b as unequal. Some rules:
> 
> Base rules
> 1. f x # a -> b
> 2. If C is a constructor, then C # f x and C # a -> b
> 3. If C and D are distinct constructors, then C # D
> 
> Propagation rules
> 1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y)
> 2. x # y <=> (x z) # (y z) <=> (z x) # (z y)
> 3. If x # y then y # x
> 
> Irreflexivity
> 1. x # x is unsatisfiable (this rule would be used for checking patterns).
> 
> With this hypothetical machinery in place, we could get something like
> 
> data a :#: b where
>   Unequal :: a # b => Unequal (a :#: b)
> 
> eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either (a :#: b) (a :~: b)
> 
> Pattern matching on an Unequal constructor would reveal the inequality, allowing closed type families relying on it to reduce.
> 
> Evidence structure:
> 
> Whereas (:~:) has just one value, Refl, it would be possible to imagine richer evidence of inequality. If two types are unequal, then they must be unequal in some particular fashion. I conjecture that we don't actually gain much value by using rich evidence here. If the types are Typeable, then we can explore them ourselves, using eqTypeRep' recursively to locate one or more differences. If they're not, I don't think we can track the source(s) of inequality in a coherent fashion. The information we got would only be suitable for use in an error message. So one option would be to bundle up some strings describing the known mismatch, and warn the user very sternly that they shouldn't try to do anything too terribly fancy with them.
> 
> [1] https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161213/86db0714/attachment.sig>