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 <[email protected]> wrote: > -----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 > [email protected] > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
