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.fe...@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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
