Abstracting over constraints: Can this be implemented in GHC?
alexander at plaimi.net
Thu Nov 6 09:54:18 UTC 2014
-----BEGIN PGP SIGNED MESSAGE-----
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 at plaimi.net
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
-----END PGP SIGNATURE-----
More information about the ghc-devs