Questions about impredicative polymorphism
I was playing around with polymorphic functions and ended up with a few questions. Let me know if I'm getting anything wrong.
Here's a function with a rank 2 type:
f :: (forall a. a -> a) -> b -> b f id' b = id' b
And a usage of f:
f id 5 == 5
Lets wrap that first function in a Maybe.
g :: Maybe (forall a. a -> a) -> b -> b g (Just id') b = id' b g Nothing b = b
This requires ImpredicativeTypes, because the 'a' in 'Maybe a' is being instantiated with a polymorphic type (right?). However usage of g is not as I would expect:
g (Just id) 5 == error
The error is "Couldn't match type
t0 -> t0' withforall a. a -> a'"
This was surprising, since matching
t0 -> t0' withforall a. a -> a' seems like exactly what we did when we passed id to f.
Is this running into the limitations of ImpredicativePolymorphism, or am I missing something in my understanding?
id has type a -> a. GHC has no problem with this:
let id' = id id
Doesn't this instantiate a type variable with a polymorphic type, which would be impredicative? Passing higher ranked polymorphic types to id does seem to require ImpredicativeTypes. Is it not considered impredicative to instantiate type variables with rank 1 types?
Submitted July 15, 2017 at 01:53AM by cairnival
via reddit http://ift.tt/2uvfi7J