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 twostep 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 typechecking of arguments.
Given a n
ary application f x_{1} … x_{n}
:

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 argumente
, we expect a't >
quantifier; For visible type arguments, we expect eitherforall 'a.
orforall 'a >
.After we have each of the quantifiers, we quickly infer a type for each of the simple arguments in
For example, sayx_{1} … x_{n}
. Here, simple means either a variable, literal, application or an expression annotated with a typex : 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.f : 'a > list 'a > list 'a
(the cons function)^{1}, and we want to infer the applicationf (fun x > x) (Nil @(forall 'xx. 'xx > 'xx))
. Here, the quick look will inspect each argument in turn, coming up with alist '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
. 
The second phase is traditional typechecking of each argument in turn, against its respective quantifier. Here we use Amulet’s typechecking function
check
instead of applying typeinference 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 quicklook. Thus, keeping with the example, we check the function
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)
against the typeforall 'xx. 'xx > 'xx
, instead of checking it against the type variable'a
.(fun x > x)
would be given monomorphic type't1 > 't2
(where't1'
,'t2
are fresh unification variables), and we’d try to unifylist ('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:
If you’re not a fan of that, consider also the profunctor encoding of lenses:
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 lenslike 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.
Assume that the
'a
variable is bound by aforall 'a.
quantifier. Since we don’t use visible type application in the following example, I just skipped mentioning it.↩︎