[Haskell-cafe] Injective type classes?

[Tom Smeding]

Hi Kai,

Thanks for the links! Your [2] is a workaround that works perfectly for my purposes. I had already considered using an associated type, but that puts the GHC type checker into an infinite loop... Using a separate type family fixes my issue.

Cheers,
Tom

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Tuesday, March 30, 2021 10:01 AM, Kai-Oliver Prott <kai.prott at hotmail.de> wrote:

> Hey Tom,
>
> there is a paper "Bidirectional type class instances" [1] about a similar concept.
>
> However, the approach is not implemented in GHC. At the moment, the dictionary for 'C (a, b)' does not explicitly include a dictionary for C a and C b. It is only implicitly referenced in the implementation of C's class methods.
> For it to be explicitly available for further usage, the dictionary data type for classes of C would have to be extended by an argument. This is not trivial and is discussed in the mentioned paper.
>
> The discussion at the GHC proposal show some alternative approaches how something like this can be achieved with the current GHC (e.g. [2]).
>
> Best,
> Kai
>
> [1] https://dl.acm.org/doi/abs/10.1145/3331545.3342596
> [2] https://github.com/ghc-proposals/ghc-proposals/pull/284#issuecomment-542322728
>
> On 30.03.21 09:27, Tom Smeding wrote:
>
>> Hi Cafe,
>>
>> With this class definition with this instance:
>>
>> class C a where
>> instance C b => C (a, b)
>>
>> GHC can of course infer, given 'C b', that 'C (a, b)'. This is nothing more
>> than the meaning of the instance declaration above.
>>
>> However, GHC cannot infer the inverse:
>>
>> {-# LANGUAGE FlexibleContexts #-}
>>
>> foo :: C a => a -> Int
>> foo = undefined
>>
>> bar1 :: C (a, b) => a -> b -> Int
>> bar1 _ = foo
>>
>> This gives an error on the right-hand side of 'bar1': "Could not deduce (C b)
>> arising from a use of ‘foo’; from the context: C (a, b)". The same happens in
>> similar cases:
>>
>> {-# LANGUAGE GADTs #-}
>>
>> bar2 :: (C p, p ~ (a, b)) => a -> b -> Int
>> bar2 _ = foo
>>
>> data Thing a where
>> Tup :: a -> b -> Thing (a, b)
>>
>> bar3 :: C a => Thing a -> Int
>> bar3 (Tup x y) = foo y
>>
>> Both these usages of 'foo' yield the same error.
>>
>> My use-case is 'bar3', where I would like GHC to determine that the call to
>> 'foo' is valid. (I don't actually care directly about bar1 and bar2.)
>>
>> Is there a way to make 'bar3' compile?
>>
>> Note that:
>> - In my actual use case, 'C' is of course not empty.
>> - In my actual use case, my type class instances _are_ in fact injective, even
>> though I do enable FlexibleInstances to be able to write e.g.
>> 'instance C (T a Int)'.
>> - Above, the dictionary for 'C (a, b)' includes a dictionary for 'C b', doesn't
>> it? So if inference can resolve 'C b', then the compilation to Core can find
>> the right dictionary, I think? (Not sure about this part.)
>>
>> Thanks a lot for your help.
>>
>> Cheers,
>> Tom
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210330/c95eab3e/attachment.html>