I don't see a way to do this without a proxy parameter (or an explicit type application, once those are available). But, I also don't see a reason why inference can't be extended to include this case. Figuring out how it would work would be a proper, full-on research project, though.
Interesting.
Richard
On Nov 6, 2014, at 4:54 AM, 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@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----- _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs