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
(*), 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.
f x1 … xn:
The quick look proceeds by inferring the type of the function to expose the first
nquantifiers, 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 ->.
After we have each of the quantifiers, we quickly infer a type for each of the simple arguments inFor example, say
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.
f : 'a -> list 'a -> list 'a(the cons function)1, 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.
The second phase is traditional type-checking of each argument in turn, against its respective quantifier. Here we use Amulet’s type-checking function
checkinstead 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 functionThis 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 type
forall 'xx. 'xx -> 'xx, instead of checking it against the type variable
(fun x -> x)would be given monomorphic type
't1 -> 't2(where
't2are 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
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
Identity functor). Indeed, the second function can’t use the lenses at all, since it must work for an arbitrary functor and not
Of course, Amulet lets you put lenses in lists: See
xs at the bottom of the file.
Assume that the
'avariable is bound by a
forall 'a.quantifier. Since we don’t use visible type application in the following example, I just skipped mentioning it.↩︎