Abstracting over constraints: Can this be implemented in GHC?

[Alexander Berntsen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

I want to be able to write essentially this function:

f :: (a -> d) -> (b, c) -> (d, d)
f g (x, y) = (g x, g y)

What do we need here for this to work?

Well, given 'g :: a -> d', we need 'a' ~ 'b' ~ 'c' from the
constraints of 'g'. So let 'g = show', such that 'g :: Show a => a ->
String'. We need that forall 'a'. 'Show a'. And from that, forall 'b'
and 'c', 'Show b' and 'Show C'.

f show (1.2, False) = ("1.2", "False")

Another example, let 'g = (>2.0)'. Now 'g :: (Ord a, Fractional a) =>
a -> Bool'. So we need that forall 'a', 'Ord a, Fractional A'. From
this we need that forall 'b' and 'c', 'Ord b, Fractional b', and 'Ord
c, Fractional c'.

f (>5.0) (15, 6/2) = (True, False)

One last example, let 'g = id'. now 'g :: a -> a'. No constraints!

f id (x, y) = (x, y)


How close can we get to this today? Quite close. But the alternatives
all feel emphatically wrong to me.

λ :set -XRankNTypes
λ :set -XConstraintKinds
λ let f :: forall b c d k. (k b, k c) => (forall a. k a => a -> d) ->
(b, c) -> (d, d); f g (x, y) = (g x, g y)
λ (f :: (Show x, Show y) => (forall a. Show a => a -> d) -> (x, y) ->
(d, d)) show (1.2, False)

We need to specify k every time we use f. That's dreadful! While a
nicer syntax (which is suggested, but I don't think it's being
actively worked on right now) would allow us to write (f @Show) show
(1.2, False) or similar -- it's still not quite right. (Though an
obviously massive improvement over the status quo.)

Of course, were we merely concerned with getting the job done, we
would write either 'bimap g g', 'g *** g' or '\(x, y) -> (g x, g y)'.
The former two may look obscure at first ("hmm, why don't they just
use 'join'?"), so the latter might actually be best. But it's The
Wrong Thing! At least *I* think so.


So what do I want here? I guess kind-level forall for constraints, so
that 'f' can infer the constraints on 'b' and 'c' from the constraints
on 'a' imposed by 'g'. Is this implementable presently? Ever? :-]


CC'ing you, SPJ, because, well, types. Also CC'ing you, ekmett,
because you have an interesting library called Constraints, so maybe
you have some related insight to offer.
- -- 
Alexander
alexander at plaimi.net
https://secure.plaimi.net/~alexander
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iF4EAREIAAYFAlRbRUoACgkQRtClrXBQc7WYbQD+Icr54KvxNA90SKIzPpp726hI
wZF4OUtuTXqyXPlU3UYBAIvg8J5uRX+UfNJKOI3PZubCfkJLuraNiW0EIgGD+hgd
=fWFQ
-----END PGP SIGNATURE-----