Why are there flexible and rigid bounds in MLF?

Question

I’m working on an implementation of MLF based on the paper Raising ML to the Power of System F. In the paper types are defined as:

t ::= a | g t1 ... tn
o ::= t | ⊥ | ∀(a ≥ o) o | ∀(a = o) o

I’m having trouble understanding what the difference between ≥ and = is in the construction of the types? Specifically for the unification algorithm.

I’ve implemented the unification and inference algorithms in the Appendix in a way which seems to maintain all invariants for those algorithms without ever reading from the bound kind in a meaningful way.

I’d like an example of when the result of unification changes based on the bound kind.

Answer 1

It is described in detail in the "Our track" section of the paper. I will try to provide a different and less formal explanation that will hopefully help you to build your own intuition.

Basically, the rigidly bound type variable is the MLF version of an ML weak variable. It could be illustrated using the examples from the paper. Given the function

choose x y = if true then x else y

we can assign two different types s1 and s2 to the expression choose id, that differ only in the way how we quantify the type variables,

 s1 = \forall a. ((a -> a) -> (a -> a))
 s2 = (\forall a. (a -> a)) -> (\forall a. (a -> a))

Apparently, neither type is more general than another in MLF, so we have to delay the choice of one or another by introducing a flexible type, and giving choose id the following type

 s3 = (\forall a. a >= (\forall a. a -> a)). (a -> a) 

We can easily see that both s1 and s2 are instances of s3.

The auto (x : \forall a. a -> a) = x x function is used as a litmus test that shows an example of a function that could not be given the flexible type, since it could be given the s2 type, which types well auto succ as (int -> int) -> (int -> int) which obviously leads to a breach of our type system (i.e., we would be able to apply succ succ). Thus we need to give a weaker type with a rigid bound,

 s4 = (\forall a. a = (\forall a. a -> a)). (a -> a) 

So if your implementation allows auto succ then it is not sound. If it doesn't allow choose id succ or choose id auto then it is incomplete wrt to the paper.

P.S. Other sources of intuition: this problem basically corresponds to the shift/reduce conflicts in parsing, or to the lazy/eager evaluation. Indeed, we need to decide whether we shall instantiate type application right now or delay it further, and neither choice is more general than another. As sometimes eager instantiation enables typing of an expression (e.g., ascribing s1 to auto) and sometimes delaying breaches the type system (by ascribing s2 to auto which enables auto succ)