System Eff

So, last time I mentioned that the first example was one "that cannot be handled under Hindley-Milner style inference". So the question is, "Ummm... what?" Let's look at the same code, but in an ML-like syntax:

let twice f x = f (f x)
let pair x = (x, x)

The types inferred for these lovely functions are:

val twice : ('a -> 'a) -> 'a -> 'a
val pair : 'a -> ('a * 'a)

So, what does the type of twice mean? Well, each 'a stands for a universally quantified variable, and in particular one that is quantified at the top level. So it means that, "for all types x, twice takes a function from x to x, and an item of type x, and returns something of type x". But is this really what we "meant" when we wrote out the definition of twice?

Maybe not. When we try to use it with pair we are treating it as though it really had the following type: "for all types x, twice takes a function from any type to the same type, and an item of type x, and returns an x". That is, we want twice to take, as its first argument, a universally quantified type. So, if we throw in some new syntax, we want this type:

val twice : (forall 'y. 'y -> 'y) -> 'x -> 'x.

We want to be able to introduce a universal quantification within the type of twice, and not just at the top level. And this is the problem: in our system of choice, this is not possible.

Now, there are of course systems in which this sort of quantification is perfectly legal; System F, for example, allows all this and more, for just 27 payments of $34.95! But, then again, type inference in System F is undecidable, which might burst your balloon.