A Quickie: A Use Case for Impredicative Polymorphism

Amulet now (as of the 18th of October) has support for impredicative polymorphism based on Quick Look impredicativity, an algorithm first proposed for GHC that treats inference of applications as a two-step process to enable inferring impredicative types.

As a refresher, impredicative types (in Amulet) are types in which a forall appears under a type constructor (that is not (->) or (*), since those have special variance in the compiler).

Quick Look impredicativity works by doing type checking of applications in two phases: the quick look, which is called so because it’s faster than regular type inference, and the regular type-checking of arguments.

Given a n-ary application f x1 … xn:

1. The quick look proceeds by inferring the type of the function to expose the first n quantifiers, based on the form of the arguments. For a regular term argument e, we expect a 't -> quantifier; For visible type arguments, we expect either forall 'a. or forall 'a ->.

   After we have each of the quantifiers, we quickly infer a type for each of the simple arguments in x1 … xn. Here, simple means either a variable, literal, application or an expression annotated with a type x : t. With this type in hands, we unify it with the type expected by the quantifier, to collect a partial substituion (in which unification failures are ignored), used to discover impredicative instantiation.

   For example, say f : 'a -> list 'a -> list 'a (the cons function)¹, and we want to infer the application f (fun x -> x) (Nil @(forall 'xx. 'xx -> 'xx)). Here, the quick look will inspect each argument in turn, coming up with a list 'a ~ list (forall 'xx. 'xx -> 'xx) equality by looking at the second argument. Since the first argument is not simple, it tells us nothing. Thus, the second phase starts with the substitution 'a := forall 'xx. 'xx -> 'xx.

2. The second phase is traditional type-checking of each argument in turn, against its respective quantifier. Here we use Amulet’s type-checking function check instead of applying type-inference then constraining with subsumption since that results in more precise resuls.

   However, instead of taking the quantifiers directly from the function’s inferred type, we first apply the substitution generated by the quick-look. Thus, keeping with the example, we check the function (fun x -> x) against the type forall 'xx. 'xx -> 'xx, instead of checking it against the type variable 'a.

   This is important because checking against a type variable degrades to inference + subsumption, which we wanted to avoid in the first place! Thus, if we had no quick look, the function (fun x -> x) would be given monomorphic type 't1 -> 't2 (where 't1', 't2 are fresh unification variables), and we’d try to unify list ('t1 -> 't2) ~ list (forall 'xx. 'xx -> 'xx) - No dice!

Why does this matter?

Most papers discussing impredicative polymorphism focus on the boring, useless example of stuffing a list with identity functions. Indeed, this is what I demonstrated above.

However, a much more useful example is putting lenses in lists (or optional, either, or what have you). Recall the van Laarhoven encoding of lenses:

type lens 's 't 'a 'b <- forall 'f. functor 'f => ('a -> 'f 'b) -> 's -> 'f 't

If you’re not a fan of that, consider also the profunctor encoding of lenses:

type lens 's 't 'a 'b <- forall 'p. strong 'p => 'p 'a 'b -> 'p 's 't

These types are both polymorphic, which means we can’t normally have a list (lens _ _ _ _). This is an issue! The Haskell lens library works around this by providing a LensLike type, which is not polymorphic and takes the functor f by means of an additional parameter. However, consider the difference in denotation between

foo :: [Lens a a Int Int] -> a -> (Int, a)
bar :: Functor f => [LensLike f a a Int Int] -> a -> (Int, a)

The first function takes a list of lenses; It can then use these lenses in any way it pleases. The second, however, takes a list of lens-like values that all use the same functor. Thus, you can’t view using the head of the list and over using the second element! (Recall that view uses the Const functor and over the Identity functor). Indeed, the second function can’t use the lenses at all, since it must work for an arbitrary functor and not Const/Identity.

Of course, Amulet lets you put lenses in lists: See lens_list and xs at the bottom of the file.