Ours & Hippy [ abridged edition]

Moderately practical uses of System F over ML

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 (→).

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 folds 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.

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

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.

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.