<div dir="auto">Possibly naive question: do we have decidable inequality in a meta theoretical sense? I feel like we have definite equality and fuzzy might not always be equal but could be for polymorphic types. And that definite inequality on non polymorphic terms is a lot smaller than what folks likely want?</div><div class="gmail_extra"><br><div class="gmail_quote">On Dec 13, 2016 10:01 AM, "Richard Eisenberg" <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
Richard<br>
<br>
> On Dec 13, 2016, at 1:02 AM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
><br>
> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi">oleg.grenrus@iki.fi</a>> wrote:<br>
>> First the bike shedding: I’d prefer /~ and :/~:.<br>
><br>
> Those are indeed better.<br>
><br>
>> new Typeable [1] would actually provide heterogenous equality:<br>
>><br>
>> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).<br>
>>    TypeRep a -> TypeRep b -> Maybe (a :~~: b)<br>
>><br>
>> And this one is tricky, should it be:<br>
>><br>
>> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).<br>
>>   TypeRep a -> TypeRep b -><br>
>>   Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b)<br>
>><br>
>> i.e. how kind inequality would work?<br>
><br>
> I don't know. It sounds like some details of how kinds are expressed<br>
> in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe<br>
> we should punt and use heterogeneous inequality? That's over my head.<br>
><br>
>> I'm not sure about propagation rules, with inequality you have to be *very* careful!<br>
>><br>
>> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear.<br>
>><br>
>> I assume that in your rules, variables are not type families, otherwise<br>
>><br>
>> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x where F x = ())<br>
>> other direction is true though.<br>
><br>
> I was definitely imagining them as first-class types; your point that<br>
> f x /~ f y => x /~ y even if f is a type family is an excellent one.<br>
><br>
>> Also:<br>
>><br>
>> f x ~ a -> b, is true with f ~ (->) a, x ~ b.<br>
><br>
> Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just<br>
> leave out that bogus piece.<br>
><br>
> Thanks,<br>
> David Feuer<br>
> ______________________________<wbr>_________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-devs</a><br>
<br>
______________________________<wbr>_________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>