## Moderately practical uses of System F over ML

(Gabriel Scherer (gasche) @ 2010-11-11 13:51:41)

In a recent comment, SpiceGuid asked :

Or, more practically, can you exhibit a motivating code example that requires full System F […], or is it still active research?

This is a very good question indeed; I’m sorry I have been a bit long to answer, I was writing this post. I’m very glad I’m able to produce such a code example — otherwise it would be quite embarassing. I have no less than three examples, that I hope you’ll find motivating, with various degrees of practicality.

Let me clarify a bit: the key difference in expressivity between ML and System F is that System F types can have type quantification (the universal quantifier `∀`) arbitrarily deep inside types.

For example, `(∀(α)α→α)→int` is a System F type, that doesn’t exist in ML. Indeed, a ML type scheme is (implicitly) quantified outside the type: a ML approximation of the above type would be `('a → 'a) → int`, equivalent to System F `∀(α) (α→α)→int`: the quantification is on the outside.

Those two types are not equivalent. Consider the following λ-term:

``````λ(f) if f true then f 0 else f 1
``````

This term can be given the type `(∀(α)α→α)→int`: it accepts a polymorphic function of type `∀(α)α→α`, and uses it on `true` (returning a boolean), then on `0` and `1`, returning integers. But it cannot be given the type `('a → 'a) → int`: inside the function, `f` is used with type `bool`, but also with type `int`, so `'a` could neither be `bool` nor `int`.

``````# ((fun f -> if f true then f 0 else f 1) : ('a -> 'a) -> int);;
Error: This expression has type int but an expression was expected of
type bool
``````

So this is a crucial difference between System F and ML. When moving from ML to System F, we gain the ability to put ∀ inside types, inside arrow types `(→)`. The previous example demonstrates that System F is strictly more expressive than ML, but I do not claim it is an interesting or motivating example. Three examples will follow, but they will all use the same pattern: a `∀` inside a `(→)`.

Actually, we do not gain much from allowing `∀` at the right of arrows: `α → ∀(β)β→β` is not that different from `∀(β) α→(β→β)`. All the fun is when we have `∀` at the left of an arrow. This is deeply connected to the fact that `(→)` is positive on its right (covariant) and negative (contravariant) on its left…

### Object types: values carrying (polymorphic) functions

My first personal encounter with higher-rank polymorphism was when using OCaml object types. It is not directly related to object-oriented programming, but rather to the fact that this coding style promotes packing functions (or methods) together with values. When you want to pass a polymorphic function as a method of an object, you need higher-rank polymorphism.

For example, imagine you have a collection class `'a coll` that describes collections (lists, sequences, etc.) of values of type `'a`. You have added boring methods such as `length : int`, `iter : ('a → unit) → unit`.

``````class type ['a] collection = object
method length : int
method iter : ('a -> unit) -> unit
end

let collection_of_list : 'a list -> 'a collection =
fun li -> object
method length = List.length li
method iter f = List.iter f li
end
``````

Now, suppose you want to add a `fold` method, in the spirit of folding over a list. A quick reminder on list folding:

``````fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
``````

In this type (for lists, not for collection), `'a` denotes the type of the elements of the list, and `'b` the type of an accumulator that is computed by iterating the list. Classic examples:

``````let length list = fold (fun acc elem -> 1 + acc) list 0
let iter f list = fold (fun () elem -> f elem) list ()
``````

The type of a `fold` method for a `'a collection` is `('a→'b→'b)→'b→'b`. In this type, `'b` is locally quantified: it corresponds to `∀(β) (α→β→β)→β→β`.

``````class type ['a] collection = object
method length : int
method iter : ('a -> unit) -> unit
method fold : ('a -> 'b -> 'b) -> 'b -> 'b
end
``````

But the corresponding implementation doesn’t work as is:

``````let collection_of_list : 'a list -> 'a collection =
fun li -> object
method length = List.length li
method iter f = List.iter f li
method fold f init = List.fold_right f li init
end

Error: This expression has type
< fold : ('a -> 'b -> 'b) -> 'b -> 'b; iter : ('a -> unit) -> unit;
length : int >
but an expression was expected of type 'a collection
The universal variable 'c would escape its scope
``````

OCaml can’t infer higher-rank polymorphism: we have to be explicit about it.

``````    method fold : 'b . ('a -> 'b -> 'b) -> 'b -> 'b =
fun f init -> List.fold_right f li init
``````

Note that OCaml departs from ML here: this is not a ML type, but a System F type. The syntax `'b . ...` is the OCaml syntax for ```∀(b) ...```.

If you wanted a ML type, you would have a collection type parametrized by the `fold` accumulator type:

``````type ('a, 'b) folder = < fold : ('a -> 'b -> 'b) -> 'b -> 'b; .. >
``````

But this is very restrictive, as you couldn’t run two `fold`s on the same collection returning different result types. In short, it wouldn’t work.

Note that I didn’t directly show a `∀` inside a `(→)` type yet. It seems that I only used `∀` inside the set of methods of the collection class; in other words, a `∀` inside a product (record, objet) type. But the arrows come when we write a function using a collection:

``````let list_of_collection : 'a collection -> 'a list = ...
``````

You don’t see it here, but there is a `∀` inside "collection". You can make it explicit:

``````let list_of_foldable
: < fold : 'b . ('a -> 'b -> 'b) -> 'b -> 'b; .. > -> 'a list =
fun c -> c#fold (fun hd tl -> hd::tl) []
``````

The important part is not that `∀` is inside the object; the OCaml type system forces us to use `∀` only in method and record field types, but in full System F we could do something like:

``````list_of_foldable : ∀(α) (∀(β) < fold : (α→β→β)→β→β; .. >) → α list
``````

It is slightly less precise, but equivalent if you’re careful. The important part is that the `∀` is at the left of the arrow.

Those OCaml code examples obviously do not use the ML type system. The OCaml language has been extended with partial support for higher-rank polymorphism, as described in the paper Semi-Explicit First-Class Polymorphism for ML (1999), by Jacques Guarrigue and Didier Rémy.

This work is semi-explicit in that we have to be explicit when we introduce higher-rank polymorphism, by giving the quantified type explicitely, but we do not have to give the type at elimination time; we only need to say that we eliminate something, without needing to give the type. The restriction of such types to record and methods is used to hide the elimination construct from the programmer, making the system simpler: it is implicitly embedded in the field access and method access operations.

This is previous work that has indeed been an inspiration for the MLF type system by Didier Rémy.

### ST monad: polymorphism means no escape

This is one use of higher-rank polymorphism that I like very much: polymorphism can mean purity, or rather unobservable side-effects. The original paper about the ST Monad is Lazy Functional State Thread (1994), by John Launchbury and Simon Peyton Jones.

If you don’t know what a monad is, you should try to learn it now. I won’t explain it here, and `ST` is not a beginner-friendly monad. You will certainly learn more trying to understand monads than reading this section. My favourite introduction to monads (for now) is the beginning of the Monads for functional programming (PDF) (1992) by Philip Wadler.

`ST` is a monad that is used to express local side effects. Monads are designed to affect computations, such that return types stay in the monad, and side effects cannot escape from the monad. `ST` is a monad you can escape from, if you’re nice enough.

Lets be more precise. `ST` is actually a family of monads indexed by a type parameter `'s`: `('s,'a) st` is a computation in the `('s,_) st` monad with values of type `'a`. The `'s` parameter is used by the side-effectful operations you allow in your `ST` monad. For example, if you design a `ST` monad for references:

``````type ('s, 'a) st_ref
val st_ref : 'a -> ('s, ('s, 'a) st_ref) st
val get : ('s, 'a) st_ref -> ('s, 'a) st
val set : ('s, 'a) st_ref -> 'a -> ('s, unit) st
``````

The idea is that you link the type of the reference and the type of the `st` monad which uses it. You have a type `('s,'a) st_ref` for references, and each use of a reference is a `('s,_) st` computation, with the same `'s`. I think of `'s` as a phantom type, but you may find the names region or thread more evocative.

What’s the use of such `'s`-ification of memory accesses? Here is the reward — beware, this is not directly OCaml syntax, I’m using a System F type here:

``````val run_st : ∀(α) (∀(s) (s, α) st) → α
``````

If a value is polymorphic in the `ST` parameter `s`, it is allowed to escape the monad and return into the pure world. As if all side effects, mutations of references, were forgotten.

The reason why it works is that « polymorphism means no escape »: if your code is polymorphic in `s`, the effects inside cannot escape, they will never be side-effects. Let’s consider a few attempts at wrongdoing:

• You could try to give a reference to the `run_st` function: if the reference were to escape the monad, it could be used in pure code, breaking the advantage of monadicity, which is precisely to control side effects. But it can’t! If you want to return the reference, `a` would have to be of the form `(s,b) st_ref`, or possibly a more complicated type in which this subtype would appear. But this is illegal, as `a` is quantified outside the arrow, while `s` is quantified inside: an instantiation of `a` certainly cannot refer to `s`.

• You could try to make the `ST` reference escape, without having it appearing in the result type. A classical felony in OCaml is to silently capture variables inside global references — here I’m talking about native OCaml references, `'a ref`. This techique sometimes called covert channel, is known to break for example the `with_open_file` wrapper — the file handler can escape in a reference, which would therefore keep a dangling pointer. But we can’t play the same trick here: the type of the reference would mention the `s` variable, and attempts to make the computatation polymorphic in `s` would fail to type, as it is captured in a global variable.

You could also try to capture the ST reference in a value where the `s` type does not appear. For example you could build the closure `(fun () → ignore the_st_ref)`. But this is fine, as you can’t read from the captured reference, as that would create a computation in the `('s,_) st` monad, again breaking `'s` polymorphism. You could still read from the reference to build a value that wouldn’t appear in the return type… but you can see this reasoning is going nowhere.

Here is some OCaml code implementing a `ST` monad:

``````module ST : sig
type ('s, 'a) st
val return : 'a -> ('s, 'a) st
val bind : ('a -> ('s, 'b) st) -> ('s, 'a) st -> ('s, 'b) st

type ('s, 'a) st_ref
val st_ref : 'a -> ('s, ('s, 'a) st_ref) st
val get : ('s, 'a) st_ref -> ('s, 'a) st
val set : ('s, 'a) st_ref -> 'a -> ('s, unit) st

type 'a secretive = { run : 's . unit -> ('s, 'a) st }
val run_st : 'a secretive -> 'a
end = struct
type ('s, 'a) st = 'a
let return x = x
let bind f m = f m

type ('s, 'a) st_ref = 'a ref
let st_ref, get, set = ref, (!), (:=)

type 'a secretive = { run : 's . unit -> ('s, 'a) st }
let run_st st = st.run ()
end

let (>>=) m f = ST.bind f m
``````

An example of unobservable side effect. I create a reference, get its value, change it, get the value again, then only return the sum of values, forgetting the reference.

``````# let test =
ST.run_st { ST.run = fun () ->
ST.st_ref 1 >>= fun r ->
ST.get r >>= fun before ->
ST.set r 2 >>= fun () ->
ST.get r >>= fun after ->
ST.return (before + after)
};;

val test : int = 3
``````

You may have noticed that I use `∀(s) (unit → (s,'a) st)` instead of directly `∀(s) (s,'a) st`; this avoids OCaml value restriction issues and does not change the semantics (the unit function is run only once, immediately in `run_st`).

Two examples of attempt to break unobservability by return the reference or escaping it through a global reference.

``````# let test_escape_1 =
ST.run_st { ST.run = fun () ->
ST.st_ref 1 >>= fun r ->
ST.return r
}
Error: This field value has type unit -> ('a, ('a, int) ST.st_ref) ST.st
which is less general than 'b. unit -> ('b, 'c) ST.st

# let test_escape_2 =
let hole = ref None in
ST.run_st { ST.run = fun () ->
ST.st_ref 1 >>= fun r ->
hole := Some r;
ST.return ()
}
!hole
Error: This field value has type unit -> ('a, unit) ST.st
which is less general than 'b. unit -> ('b, 'c) ST.st
``````

There is another situation where polymorphism is used as a tool to ensure purity: polymorphism over monads. A piece of code may use a monad `m`, but actually be parametric in `m`, instead of using a particular value of `m`. If a code is polymorphic over a monad, it means there is actually no effect: it is only pure code in monadic style.

It is related to the ST polymorphism I described, but still quite different. For one, it cannot be expressed directly in System F: monads use higher-order polymorphism, they’re not types but type operators. And it is quite easy to see why such code is pure: you just have to instantiate `m := Id`, the identity monad, to extract the pure computation underlying.

I think the ST monad is more subtle: it is not pure, it is a secretly impure term. The polymorphism seals its secret, so that it can never be observed.

We may however think of an informal explanation similar to polymorphism over monads, where instantiating the quantified variable with the right term leads to purity.

Imagine that, instead of being just a phantom type, the type variable `s` decribed the memory region where the reference is allocated. A `('s,_) st` computation is a computation that is allowed to make effects on all references allocated in `'s`, and no others. Now suppose our piece of code is polymorphic in `'s`; to run it, we only have to choose an arbitrary region `'s0`, or allocate it on the fly. The only way we could have side-effects is to have another piece of code in our program interacting with the same region `'s0`. But if we know that another piece of code uses a given region `s0`, we can always instantiate the `'s` variable of the `run_st` function with a different region `'s1`. This is similar to how we handle bound names in syntaxic term manipulations: we may always choose a fresh term that doesn’t conflict with any other name in the program. Here we can choose a fresh memory region, making mutations that are unobservable to the outside, as they don’t know the region we have chosen.

Please note, finally, that the `ST` monad is not the end of it all, the graal of side-effects tamers. It nicely captures a specific usage pattern for local side effects, that can be proved observably pure by the type system itself. Note that the type system used here is System F, not ML, as we crucially use the `∀(s)` quantification on the left of the arrow in the `run_st` type.

Some uses of references don’t fit that pattern, and they need more complicated proofs of observational purity; we may be able to present them as well-typedness in more complicated type systems. In this direction, I know of the work of Francois Pottier, which has done quite a lot of things on regions for separating non-interacting effects, capabilities to represent fine-grained ownership and sharing of regions, and various rules attempting to model "hidden state", or unobservable local side effects. See for example the slides on Hidden state and the anti-frame rule (PDF) (2009), or the corresponding papers and other publications.

### Existential types: locally hidden values

The two examples above were much more verbose than I had originally planed, so I will try to keep this one short. Besides, I haven’t found any simple and practical example for this one, though I’m convinced the notion itself is indeed of practical importance.

Existential types are used to hide parts of a type. For example, the type `∃(α) α*(α→string)` represents the type of any value along with a printing function for it. The real type of the value is hidden by the new quantifier `∃`, and the only thing we can do is print it. The interest of hiding parts of a type is that we can mix together types having different hidden parts. For example, we could never put two values of type `bool*(bool→string)` and `int*(int→string)` together in a list, but we could pack them as elements of `∃(α) α*(α→string)` and put them into the same list.

You could define the type `thunk α := ∃(β) β*(β→α)` of suspended computations that ultimately return a value of type α. The advantage over the classic `unit→α` is that you don’t have to allocate an extra closure to hide the `β` value. Existential types are useful for other low-level stuff, like typed compilation of closures, or even compilation to a typed assembly language. They also represent hiding and modularity, and allow to dynamically encode abstract data types and some object-oriented techniques.

For an in depth explanation of existential types and its use in typed closure conversion — which is roughly a technique to compile away all inner functions in a functional language — see the following courses notes (2010) by Didier Rémy.

Existential types can be added to a type system. For example, the seminal paper Abstract Types Have Existential Types (PDF) (1988), by John Mitchell and Gordon Plotkin, uses a type system similar to System F, extended with existential types. You can easily see that in this case, the same distinction between ML-style and F-style quantifications apply: you really need to pass `∃` inside arrows, as function parameters.

But the importance of System F goes further here: existential types can actually be encoded directly in System F, while this is not possible in ML. The idea is that the existential type `∃(α)T` (here `T` is a metavariable representing a type expression that may contain occurences of the type variable `α`) can be encoded as:

``````∀(β) (∀(α)T→β)→β
``````

We choose `β` fresh, in particular it does not appear in `T`. This encoding has a natural explanation: the existential type `∃(α)T` means, in some way, that « I have a precise type for `α`, but I won’t show it to you ». How can I prove that I have such a value for `α`, without showing it to you? Well, I propose that you give me a challenge: you choose any type `β`, and give me a computation that needs `T` to build a `β`. If I really have some `α`, I will be able to build your `β` and pass it back to you.

This encoding crucially uses the `∀(α)` quantification on the left of the outer arrow: it cannot be done in ML.

You may have noticed that the encoding above, including its interactive explanation, seems related to double-negation translations. But one should be careful when making such comparisons, as the `∀` and `∃` quantifiers here are not the quantifier from first-order logic:

• They are second-order quantifications, not first-order.

• You don’t have the nice duality between `∃` and `∀` that you have in classical logic. The typing rules for `∃` — that I’ve been careful not to give — are much more complicated than those for `∀`. The idea is that you can "open" an existential type locally, if the exact type for the existential variable doesn’t escape the local scope; this is quite subtle. If you want all the details, look at the aforementioned course notes.

Post Scriptum: I would like to thank rz0 for the proof-reading he consistently offers me for each blog article. I ashamedly use him as a spell checker, english grammar reference, and Master of Typography. His insightful questions and remarks also force me to improve and clarify my articles significantly.