Abstracting over constraints: Can this be implemented in GHC?

[Richard Eisenberg]

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 <alexander at plaimi.net> 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
> 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-----
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>