Why is impredicative polymorphism allowed only for functions in Haskell?
Asked Answered
T

1

17

In Haskell I can't write

f :: [forall a. a -> a]
f = [id]

because

• Illegal polymorphic type: forall a. a -> a
  GHC doesn't yet support impredicative polymorphism

But I can happily do

f :: (forall a. a -> a) -> (a, b) -> (a, b)
f i (x, y) = (i x, i y)

So as I see GHC does support impredicative polymorphism which is contradict to the error message above. Why is the (->) type constructor treated specially in this case? What prevents GHC from having this feature generalized over all datatypes?

Triboluminescence answered 4/6, 2019 at 17:35 Comment(2)
It may have to do with the recursive nature of []. The function only requires RankNTypes to be enabled. (Strictly speaking, Rank2Types would suffice, were it not superseded by RankNTypes.) It's [] which is special, not (->).Noblewoman
@Noblewoman it is (->) that's special: Maybe (forall a . a) is a subtype of forall a . Maybe a in that every value of the first type is admissible when the second is expected but not vice-versa; ie impredicative polymorphism is disallowed for Maybe and [] for exactly the same reason.Bonbon
T
19

Higher-rank polymorphism is a special case of impredicative polymorphism, where the type constructor is (->) instead of any arbitrary constructor like [].

The basic problems with impredicativity are that it makes type checking hard and type inference impossible in the general case—and indeed we can’t infer types of a higher rank than 2: you have to provide a type annotation. This is the ostensible reason for the existence of the Rank2Types extension separate from RankNTypes, although in GHC they’re synonymous.

However, for the restricted case of (->), there are simplified algorithms for checking these types and doing the necessary amount of inference along the way for the programmer’s convenience, such as Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism—compare that to the complexity of Boxy Types: Inference for Higher-rank Types and Impredicativity.

The actual reasons in GHC are partly historical: there had been an ImpredicativeTypes extension, which was deprecated because it never worked properly or ergonomically. Part of the problem was that we didn’t yet have the TypeApplications extension, so there was no convenient way to explicitly supply a polymorphic type as a type argument, and the compiler attempted to do more inference than it ought to. In GHC 9.2, ImpredicativeTypes has come out of retirement, thanks to GHC proposal 274 and an algorithm, Quick Look, that infers a predictable subset of impredicative types.

In the absence of ImpredicativeTypes, there have been alternatives for a while: with RankNTypes, you can “hide” other forms of impredicativity by wrapping the polymorphic type in a newtype and explicitly packing & unpacking it to tell the compiler exactly where you want to generalise and instantiate type variables.

newtype Id = Id { unId :: forall a. a -> a }

f :: [Id]
f = [Id id]  -- generalise

(unId (head f) (), unId (head f) 'x')  -- instantiate to () and Char
Thick answered 4/6, 2019 at 18:11 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.