Search code examples
haskelltype-theory

What is predicativity?


I have pretty decent intuition about types Haskell prohibits as "impredicative": namely ones where a forall appears in an argument to a type constructor other than ->. But just what is predicativity? What makes it important? How does it relate to the word "predicate"?


Solution

  • Let me just add a point regarding the "etymology" issue, since the other answer by @DanielWagner covers much of the technical ground.

    A predicate on something like a is a -> Bool. Now a predicate logic is one that can in some sense reason about predicates -- so if we have some predicate P and we can talk about, for a given a, P(a), now in a "predicate logic" (such as first-order logic) we can also say ∀a. P(a). So we can quantify over variables and discuss the behavior of predicates over such things.

    Now, in turn, we say a statement is predicative if all of the things a predicate is applied to are introduced prior to it. So statements are "predicated on" things that already exist. In turn, a statement is impredicative if it can in some sense refer to itself by its "bootstraps".

    So in the case of e.g. the id example above, we find that we can give a type to id such that it takes something of the type of id to something else of the type of id. So now we can give a function a type where an quantified variable (introduced by forall a.) can "expand" to be the same type as that of the entire function itself!

    Hence impredicativity introduces a possibility of a certain "self reference". But wait, you might say, wouldn't such a thing lead to contradiction? The answer is: "well, sometimes." In particular, "System F" which is the polymorphic lambda calculus and the essential "core" of GHC's "core" language allows a form of impredicativity that nonetheless has two levels -- the value level, and the type level, which is allowed to quantify over itself. In this two-level stratification, we can have impredicativity and not contradiction/paradox.

    Although note that this neat trick is very delicate and easy to screw up by the addition of more features, as this collection of articles by Oleg indicates: http://okmij.org/ftp/Haskell/impredicativity-bites.html