Type Systems #10: Universal Quantification and Rank-N Types

(This is part 10 in a series on type systems. You can find part 9 here .)

In post #5 I claimed that System F generics shouldn’t be a huge conceptual leap. Looking at a type like toString :: ∀A. A → String, you’ll probably immediately know what it does — the function takes anything and turns it into a string.

In post #8 we even looked at a very degenerate case, error :: ∀R. String → R, that can never return at all, which is probably less obvious to most.

But there is one thing all the generic functions we’ve looked at so far have in common… we always put the ∀ symbol — the universal quantifier — at the very front of the type.

Nobody says that we have to do that, it’s just that this kind of generic function is the only one we deal with in day-to-day programming, because the major programming languages only allow for this specific kind of generic function. But System F is actually a lot more powerful than that.

Since this is where we leave the comfort zone of “working man’s knowledge”, we will slow the pace to explore this new concept. From now on I will also drop explicit type annotations in function definitions, if they can be inferred from context, to reduce visual noise. (This is problematic in System F but we’ll talk about that later.)

Have a look at this function definition:

apply10 :: (∀A. A → A) → Int
apply10 = λf. f 10

Here, the quantifier ∀A is not at the outermost layer of the type, but rather inside the function argument. We call this sort of type a Rank-N Type, where the N indicates how deeply nested the universal quantifier is, in this case 2.

This is markedly different from the rank-1 type weird :: ∀A. (A → A) → Int, because whoever calls weird gets to choose what A is — this is not the case for apply10: if you wish to call apply10, you have to provide a generic function.

(Hard) bonus question: apply10 isn’t a particularly useful function. Why?

Can you explain in words what apply10 does?

Let me show you an actually useful example of a rank-2 type as well, assuming Haskell semantics for a moment:

withFile :: FilePath → (∀R. FileHandle → R) → Void

This function takes a path to a file, and a continuation. withFile will do some file opening logic and then hand a file to another function.

As discussed in post #8, the continuation’s type ∀R. FileHandle → R might make you scratch your head, because such a function can never return, or in a Haskell context, only return an error.

I must clarify then that returning an error in Haskell is perfectly fine and will not blow up your program, as long as you don’t try to access it. That is to say, the Haskell snippet let x = error "oops!" in 42 will happily evaluate to 42 without crashing. let x = error "oops!" in x on the other hand will blow up.

So — why is genericising the return type like that useful?

Well — since your continuation must return an error, it can in particular not return anything else, like the file handle, and it cannot leak the file handle to the outside world in sneaky ways.

Haskell does have a way to reference “global-ish” state using IORefs, but if you want to for example call modifyIORef to sneakily put the file handle in a global state so you can use it later, Haskell would force you to return a value of type IO (), meaning the continuation would have a type of FileHandle → IO (), which is not ∀R. FileHandle → R, so it won’t typecheck.

Again, we’ve enforced a very desirable property at the type level. We can safely assume that the continuation has done whatever it needed to do with the file and the file is no longer needed, so withFile can close it after the continuation ran. In so many other programming languages, this would require careful runtime checks by the programmer… here we just get it for free by the type system, and the compiler can enforce it for us! ^[1]

It’s theorems for free all over again!

(This is part 10 in a series on type systems. You can find part 11 here .)