What is predicativity?

by

The central question of these type systems is: “Can you substitute a polymorphic type in for a type variable?”. Predicative type systems are the no-nonsense schoolmarm answering, “ABSOLUTELY NOT”, while impredicative type systems are your carefree buddy who thinks that sounds like a fun idea and what could possibly go wrong?

Now, Haskell muddies the discussion a bit because it believes polymorphism should be useful but invisible. So for the remainder of this post, I will be writing in a dialect of Haskell where uses of forall are not just allowed but required. This way we can distinguish between the type a, which is a monomorphic type which draws its value from a typing environment that we can define later, and the type forall a. a, which is one of the harder polymorphic types to inhabit. We’ll also allow forall to go pretty much anywhere in a type — as we’ll see, GHC restricts its type syntax as a “fail-fast” mechanism rather than as a technical requirement.

Suppose we have told the compiler id :: forall a. a -> a. Can we later ask to use id as if it had type (forall b. b) -> (forall b. b)? Impredicative type systems are okay with this, because we can instantiate the quantifier in id‘s type to forall b. b, and substitute forall b. b for a everywhere in the result. Predicative type systems are a bit more wary of that: only monomorphic types are allowed in. (So if we had a particular b, we could write id :: b -> b.)

There’s a similar story about [] :: forall a. [a] and (:) :: forall a. a -> [a] -> [a]. While your carefree buddy may be okay with [] :: [forall b. b] and (:) :: (forall b. b) -> [forall b. b] -> [forall b. b], the predicative schoolmarm isn’t, so much. In fact, as you can see from the only two constructors of lists, there is no way to produce lists containing polymorphic values without instantiating the type variable in their constructors to a polymorphic value. So although the type [forall b. b] is allowed in our dialect of Haskell, it isn’t really sensible — there’s no (terminating) terms of that type. This motivates GHC’s decision to complain if you even think about such a type — it’s the compiler’s way of telling you “don’t bother”.*

Well, what makes the schoolmarm so strict? As usual, the answer is about keeping type-checking and type-inference doable. Type inference for impredicative types is right out. Type checking seems like it might be possible, but it’s bloody complicated and nobody wants to maintain that.

On the other hand, some might object that GHC is perfectly happy with some types that appear to require impredicativity:

> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}

It turns out that some slightly-restricted versions of impredicativity are not too bad: specifically, type-checking higher-rank types (which allow type variables to be substituted by polymorphic types when they are only arguments to (->)) is relatively simple. You do lose type inference above rank-2, and principal types above rank-1, but sometimes higher rank types are just what the doctor ordered.

I don’t know about the etymology of the word, though.

* You might wonder whether you can do something like this:

data FooTy a where
     FooTm :: FooTy (forall a. a)

Then you would get a term (FooTm) whose type had something polymorphic as an argument to something other than (->) (namely, FooTy), you don’t have to cross the schoolmarm to do it, and so the belief “applying non-(->) stuff to polymorphic types isn’t useful because you can’t make them” would be invalidated. GHC doesn’t let you write FooTy, and I will admit I’m not sure whether there’s a principled reason for the restriction or not.

(Quick update some years later: there is a good, principled reason that FooTm is still not okay. Namely, the way that GADTs are implemented in GHC is via type equalities, so the expanded type of FooTm is actually FooTm :: forall a. (a ~ forall b. b) => FooTy a. Hence to actually use FooTm, one would indeed need to instantiate a type variable with a polymorphic type. Thanks to Stephanie Weirich for pointing this out to me.)

More Related Contents:

  1. Haskell: Given a list of numbers and a number k, return whether any two numbers from the list add up to k
  2. What is the monomorphism restriction?
  3. What is the difference between . (dot) and $ (dollar sign)?
  4. Good examples of Not a Functor/Functor/Applicative/Monad?
  5. Monads with Join() instead of Bind()
  6. When is memoization automatic in GHC Haskell?
  7. How to get normal value from IO action in Haskell
  8. What does the “@” symbol mean in reference to lists in Haskell?
  9. New state of the art in unlimited generation of Hamming sequence
  10. How do you represent a graph in Haskell?
  11. Haskell types frustrating a simple ‘average’ function
  12. What’s the “|” for in a Haskell class definition?
  13. Lifting a higher order function in Haskell
  14. Distinction between typeclasses MonadPlus, Alternative, and Monoid?
  15. How do I write, “if typeclass a, then a is also an instance of b by this definition.”
  16. Function definition by special cases in GHCi
  17. Applicative functor evaluation is not clear to me
  18. Expressing do block using only monadic bind syntax
  19. Lambda for type expressions in Haskell?
  20. Pattern matching identical values
  21. Composing Monads v. Applicative Functors
  22. Abusing the algebra of algebraic data types – why does this work?
  23. How to interpret bind/>>= of the function instance?
  24. What does the : infix operator do in Haskell?
  25. Monoidal Functor is Applicative but where is the Monoid typeclass in the definition of Applicative?
  26. How to return a pure value from a impure method
  27. How to convert Unicode Escape Sequence to Unicode String in Haskell
  28. Haskell: why the convention to name a helper function “go”?
  29. Functional lenses
  30. Does Haskell have return type overloading?

Leave a Comment