This Impredicative Sentence Talks about Itself

In which we learn a new word and check in on recent research in type inference.

Word of the day

William Safire's "Fumblerules" is a book on writing, a collection of short essays on various points of grammar and style, each based on a memorable self-explanatory example: "A writer must not shift your point of view" and "No sentence fragments." Fumblerules make the mistake they name.

While it's not a mistake, the title of this post is my self-explanatory example of our programming language word of the day:

impredicative

which is said of a definition that is self-referencing. Russell's Paradox uses a well-known example: "the set of sets that don't include themselves."

Self-reference and types

This word of the day comes to us via the paper "Boxy Types: Inference for Higher-Rank Types and Impredicativity" by Simon Peyton-Jones (with Microsoft Research in Cambridge, England) along with Stephanie Weirich, and Dimitrios Vytiniotis (University of Pennsylvania) from ICFP 2006, to my knowledge the only paper containing the phrase "plain as a pikestaff." (My money is on Peyton-Jones for contributing that one. ) But what were higher-rank types and impredicativity, I wanted to know.

A higher-rank type only makes sense with some background in parametric polymorphism, but I'll take a stab at explaining it. A polymorphic type is expressed with a universal quantifier "for all types a...", as in "for all types a, list of a -> int", the type of a polymorphic list length function. In general a polymorphic type can have any number of universal quantifiers. In Hindley-Milner, these universal quantifiers all come at the beginning of the type phrase. For any particular invocation of a polymorphic function, this means the polymorphic variables are each bound to one particular type. The higher-rank type means that the universal quantifiers can appear inside function types, allowing those polymorphic variables to be bound to different types within the body of the function. The utility of this is apparently in a kind of generic programming, as explained in Peyton-Jones work "Scrap Your Boilerplate", work done with Ralf Lämmel, another Microsoft Research employee.

The impredicative part of type inference is interesting. At first, I thought it meant recursive types, such as are used for linked lists. But I was puzzled how that could relate to this statement from the paper:

In the Hindley-Milner system, type variables range only over monotypes, but to allow function g we must allow a type variable—a, in the definition of Maybe—to be instantiated with a polytype. In the jargon, we need an impredicative type system, whereas Hindley-Milner is predicative.

After some digging, I think perhaps an impredicative type system is as the Wikipedia "Type polymorphism" indicates, one allowing impredicative polymorphism, allowing an instantiation of a variable in a type with the type itself.

The difference comes down to what is meant by "for all types" in the universal quantifier. In the predicative type system "for all types" is ranging over the monotypes, anything without a universal quantifier. More to the point, for all types does not include other polymorphic types... and therefore cannot include itself. In the impredicative type system, "for all types" can range over the polymorphic types too, and can include itself, hence the term "impredicative."