Questions about impredicative polymorphism

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.

Question #1

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?

Question #2

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


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s