Rank-2 polymorphism and overloading
Hello all, I'm having difficulties understanding rank-2 polymorphism in combination with overloading. Consider the following contrived definition: f :: (forall a . Eq a => a -> a -> Bool) -> Bool f eq = eq True True Then, we pass f both an overloaded function and a regular polymorphic function: x :: forall a . Eq => a -> a -> Bool x = \x y -> x == y y :: forall a . a -> a -> Bool y = \x y -> True g :: (Bool, Bool) g = (f x, f y) Could someone explain to me, or point me to some reading material, why g is correctly typed? I understand that x's type is what f expects, but why does y's polymorphic type fulfill the overloaded type of f's argument? I can imagine that it is justified since f's argument type is more restrictive than y's type. However, it requires y to throw away the provided dictionary under the hood, which seems counter intuitive to me. Regards, Thomas
Am Montag 26 April 2010 19:52:23 schrieb Thomas van Noort:
Hello all,
I'm having difficulties understanding rank-2 polymorphism in combination with overloading. Consider the following contrived definition:
f :: (forall a . Eq a => a -> a -> Bool) -> Bool f eq = eq True True
Then, we pass f both an overloaded function and a regular polymorphic function:
x :: forall a . Eq => a -> a -> Bool x = \x y -> x == y
y :: forall a . a -> a -> Bool y = \x y -> True
g :: (Bool, Bool) g = (f x, f y)
Could someone explain to me, or point me to some reading material, why g is correctly typed?
I understand that x's type is what f expects, but why does y's polymorphic type fulfill the overloaded type of f's argument? I can imagine that it is justified since f's argument type is more restrictive than y's type.
Yes, y's type is more general than the type required by f, hence y is an acceptable argument for f - even z :: forall a b. a -> b -> Bool is.
However, it requires y to throw away the provided dictionary under the hood, which seems counter intuitive to me.
Why? y doesn't need the dictionary, so it just ignores it.
Regards, Thomas
On 26-4-2010 20:12, Daniel Fischer wrote:
Am Montag 26 April 2010 19:52:23 schrieb Thomas van Noort:
...
Yes, y's type is more general than the type required by f, hence y is an acceptable argument for f - even z :: forall a b. a -> b -> Bool is.
That's what I thought. I've just never seen such a notion of a more general type involving overloading before.
However, it requires y to throw away the provided dictionary under the hood, which seems counter intuitive to me.
Why? y doesn't need the dictionary, so it just ignores it.
Sure, but y's type explicitly mentions that it doesn't want a dictionary, so why would you provide one to it?
Regards, Thomas
Regards, Thomas
On Mon, Apr 26, 2010 at 2:55 PM, Thomas van Noort
On 26-4-2010 20:12, Daniel Fischer wrote:
Am Montag 26 April 2010 19:52:23 schrieb Thomas van Noort:
...
Yes, y's type is more general than the type required by f, hence y is an acceptable argument for f - even z :: forall a b. a -> b -> Bool is.
That's what I thought. I've just never seen such a notion of a more general type involving overloading before.
However, it requires y to throw away the provided dictionary under the hood, which seems counter intuitive to me.
Why? y doesn't need the dictionary, so it just ignores it.
Sure, but y's type explicitly mentions that it doesn't want a dictionary, so why would you provide one to it?
Actually, y's type doesn't say anything at all about dictionaries.
That's a detail about GHC's implementation.
y's type says it will accept two values of any type. f's type says it
will provide two values of a type which is an instance of Eq.
--
Dave Menendez
Thomas van Noort wrote:
Hello all,
I'm having difficulties understanding rank-2 polymorphism in combination with overloading. Consider the following contrived definition:
f :: (forall a . Eq a => a -> a -> Bool) -> Bool f eq = eq True True
Then, we pass f both an overloaded function and a regular polymorphic function:
x :: forall a . Eq => a -> a -> Bool x = \x y -> x == y
y :: forall a . a -> a -> Bool y = \x y -> True
g :: (Bool, Bool) g = (f x, f y)
Could someone explain to me, or point me to some reading material, why g is correctly typed?
I understand that x's type is what f expects, but why does y's polymorphic type fulfill the overloaded type of f's argument? I can imagine that it is justified since f's argument type is more restrictive than y's type. However, it requires y to throw away the provided dictionary under the hood, which seems counter intuitive to me.
f requires a function that is able to compute, for two values of type a (which instantiates Eq), a Boolean. y certainly fulfills that requirement: it does not even require that the values are of a type instantiating Eq. This is also well-typed and might or might not be enlightening:
z :: forall a. Eq a => a -> a -> Bool z = y
g :: (Bool, Bool) g = (f x, f z) -- note the use of z here instead of y
Jochem -- Jochem Berndsen | jochem@functor.nl
On 26-4-2010 20:13, Jochem Berndsen wrote:
Thomas van Noort wrote:
...
f requires a function that is able to compute, for two values of type a (which instantiates Eq), a Boolean.
y certainly fulfills that requirement: it does not even require that the values are of a type instantiating Eq.
This is also well-typed and might or might not be enlightening:
z :: forall a. Eq a => a -> a -> Bool z = y
g :: (Bool, Bool) g = (f x, f z) -- note the use of z here instead of y
I find your example of z more intuitive as it is z that does not provide its dictionary to y, but throws it away explicitly. This in contrast to y that is provided a dictionary but throws it away implicitly. Regards, Thomas
Jochem
participants (4)
-
Daniel Fischer -
David Menendez -
Jochem Berndsen -
Thomas van Noort