[Haskell-cafe] Injective type classes?

[Kai-Oliver Prott]

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/96b6aa94/attachment-0001.html>