Explicit inequality evidence

[Oleg Grenrus]

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 <david.feuer at gmail.com> wrote:
>>
>> 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
>> _______________________________________________
>> 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: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161215/63880779/attachment.sig>