[Haskell-cafe] Get proof of injectivity for an injective type family

[Adam Gundry]

[Apologies for the duplicate!]


On 06/04/2021 03:30, Richard Eisenberg wrote:
> No. Injective type families are solely a type-inference mechanism. There are no proofs or other evidence. Figuring out how to get this right would be a significant research project, I'm afraid.

This is quite true, but...


>> On Apr 3, 2021, at 2:59 AM, Andreas Källberg <anka.213 at gmail.com> wrote:
>>
>> Is there any way to get hold of a proof of injectivity for an injective type family?
>> In other words, given this type family
>>
>>    type family F a = b | b -> a
>>
>> can I get the term
>>
>>    fInj :: F a ~ F b => (a ~ b => r) -> r
>>
>> in any way (without using unsafeCoerce)?

...while injective type families don't themselves carry evidence, it is
sometimes helpful to encode it by writing the inverse family explicitly
and adding constraints that require it to be an inverse:

    type family FInv b = a | a -> b

    type Good a = FInv (F a) ~ a

    fInj :: (F a ~ F b, Good a, Good b) => (a ~ b => r) -> r
    fInj x = x

Of course this may not be enough, because the extra constraints may get
in the way.

Hope this helps,

Adam


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
118 Wymering Mansions, Wymering Road, London W9 2NF, England