§ 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 wantto 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 oftype [β], 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 needto 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?