§ A quick look at impredicativity

I found this video very helpful, since I was indeed confused about the two meanings of impredicativity that I had seen floating around. One used by haskellers, which was that you can't instantiate a type variable a with a ( forall t). Impredicative in Coq means having (Type : Type).

• polymorphic types:

forall p. [p] -> [p] -- LEGAL
Int -> (forall p. [p] -> [p])  -- ILLEGAL
(forall p. [p] -> [p])  -> Int -- ILLEGAL
[forall a. a -> a] -- ILLEGAL

• Higher rank types: forall at the outermost level of a let-bound function, and to the left and right of arrows!

Int -> (forall p. [p] -> [p])  -- LEGAL
(forall p. [p] -> [p])  -> Int -- LEGAL
runST :: (forall s. ST s a) -> a -- LEGAL
[forall a. a -> a] -- ILLEGAL

• Impredicative type:

[forall a. a -> a]

• We can't type runST because of impredicativity:

($) :: forall a, forall b, (a -> b) -> a -> b
runST :: forall a, (forall s, ST s a) -> a -- LEGAL
st :: forall s. ST s Int
runST st -- YES
runST $ st -- NO

• Expanding out the example:

($) runST st
($) @ (forall s. ST s Int) @Int  (runST @ Int) st

• Data structures of higher kinded things. For example. we might want to have [∀ a, a -> a]
• We have ids :: [∀ a, a -> a]. I also have the function id :: ∀ a, a -> a. I want to build ids' = (:) id ids. That is, I want to cons an id onto my list ids.
• How do we type infer this?

§ How does ordinary type inference work?

reverse :: ∀ a. [a] -> [a]
and :: [Bool] -> Bool
foo = \xs -> (reverse xs, and xs)

• Start with xs :: α where α is a type variable.
• Typecheck reverse xs. We need to instantiate reverse. With what type? that's what we need to figure out!
• (1) Instantiate: Use variable β. So we have that our occurence of reverse has type reverse :: [β] -> [β].
• (2) Constrain: We know that xs :: α and reverse expects an input argument of type [β], so we set α ~ [β] due to the call reverse xs.
• We now need to do and xs. (1) and doesn't have any type variables, so we don't need to perform instantiation. (2) We can constrain the type, because and :: [Bool] -> Bool, we can infer from and xs that α ~ [Bool]
• We solve using Robinson unification . We get [β] ~ α ~ [Bool] or β = Bool

§ Where does this fail for polytypes?

• The above works because α and Β only stand for monotypes .
• Our constraints are equality constraints , which can be solved by Robinson unification
• And we have only one solution (principal solution)
• When trying to instantiate reverse, how do we instantiate it?
• Constraints become subsumption constraints
• Solving is harder
• No principal solution
• Consider incs :: [Int -> Int], and (:) id incs versus (:) id ids.

§ But it looks so easy!

• We want to infer (:) id ids
• We know that the second argument ids had type [∀ a, a -> a]
• we need a type [p] for the second argument, because (:) :: p -> [p] -> [p]
• Thus we must have p ~ (∀ a, a -> a)
• We got this information from the second argument
• So let's try to treat an application (f e1 e2 ... en) as a whole.

§ New plan

• Assume we want to figure out filter g ids.
• start with filter :: ∀ p, (p -> Bool) -> [p] -> Bool
• Instatiate filter with instantiation variables κ to get (κ -> Bool) -> [κ] -> Bool
• Take a "quick look" at e1, e2 to see if we know that κ should be
• We get from filter g ids that κ := (∀ a, a -> a).
• Substitute for κ (1) the type that "quick look" learnt, if any, and (2) A monomorphic unification variable otherwise.
• Typecheck against the type. In this case, we learnt that κ := (∀ a, a -> a), so we replace κ with (∀ a, a -> a).
• Note that this happens at each call site !

§ The big picture

Replace the idea of:

• instantate function with unficiation variables, with the idea.
• instantiate function with a quick look at the calling context.
• We don't need fully saturated calls. We take a look at whatever we can see!
• Everything else is completely unchanged.

§ What can QuickLook learn?

• Video