Gagallium

Last year (2017), I was following the MPRI, a research-oriented master programme in Paris. The project for the Functional programming and type systems course (taught by François Pottier, Didier Rémy, Yann Régis-Gianas and Pierre-Évariste Dagand) was to write a compiler for a tiny functional language. I extended that project with algebraic effects and a static type system checking that effects could not be unhandled. Explaining the type system of my implementation is what this post is about.

Introduction to algebraic effects

In programming, we say that an expression performs a side effect when its behaviour can depend on the context where it is executed, or modify that context. The most basic examples of this are accessing and modifying a mutable mutable variable, as well as input and output.

Algebraic effects take this idea one step further, and allow functions to perform user-defined effects, whose behaviour is given dynamically by an effect handler. Effect handlers control the behaviour to give to effects during the evaluation of an expression. The syntax and semantics are very similar to that of exceptions and the match with exception syntax. Let us recall how these work:

match f () with
| x -> g x
| exception Not_found -> 42

When evaluating the expression above, f () will be called. If it returns a value x, then g x will be called and its result will be the result of the whole match expression. However, if it raises the exception Not_found, then the result of the match expression will be 42, and if it raises another exception, the whole match construct will raise that same exception. Note that there is an important difference with

try
  let x = f () in
  g x
with Not_found -> 42

in that exceptions in g x are not handled by the match example: if it raises Not_found, the match example will re-raise the exception, while the try example will return 42.

Algebraic effects are quite similar, although the syntax is slightly different. The keyword perform is used instead of raise, and effect instead of exception, with a couple differences. The following expression

match ... with
| x -> x
| effect Get k -> k 6

is a handler around the scrutinee computation .... If evaluating the scrutinee returns a value x, it is passed by the handler unchanged. If it raises the Get effect, then the behaviour is determined by the way the effect Get clause handles its “continuation” k: the value passed to k in this clause (here 6) is used to continue the computation of the scrutinee, starting over where perform was interrupted (effect handlers generalize Lisp’s “resumable exceptions”).

With a full example, we have:

let f () = (perform Get) * 7 in
match f () with
| x -> x
| effect Get k -> k 6

Here the scrutinee is perform Get * 7, so the computation restarts as 6 * 7, and the whole match expression returns 42.

We will not dwell on the uses of algebraic effects here, as our goal, typing effects, only requires to know what the basics of effects are. If you are interested in them, you can learn more here or here.

One problem happening with effects is the same that happens with exceptions: not handling an effect or an exception is an error and interrupts the program. However, it is much more important in the case of effects than exceptions, as effect handlers, unlike exceptions, are not used only in exceptional situations, so there are a lot more places where there is a risk of an error. The whole point of typing being to avoid statically-identifiable errors, we want a type system that prevents them from happening in the first place.

Typing with effects

When we want to type effects, we have to make a difference between values, which have a type, and computations, which have a type and can produce effects when executed. We usually write a typing judgement e : t!Δ when e is an expression of type t which produces an effect Δ when executed. However, if we execute let x = e;; in the toplevel, then the answer will be of the form val x : t, since the value of x has the type t, and the effect Δ has already happened, and no longer exists in the type.

Moreover, since functions perform computations, there is an effect in the type of the function itself. Thus, an arrow type takes a type and produces a type with effect. We write s -> (t!Δ) as s -[Δ]-> t with the effect on the arrow to make it explicit that it is the function that performs the effect.

Note that a function of type s -[Δ]-> t may perform the effects in Δ, but it does not have to. However, it may not perform any effect not listed in Δ.

Another thing to note is that effects can already be expressed in existing languages using monads, where the type t!Δ woould be replaced by a value of type M Δ t, where M is a monad expressing computation. However, making effects first-class both expresses that effects only happen at computation time and do not impact the behaviour of an expression after that, and allows easier design and experimentation about the type system.

First try: row polymorphism and the usual unification algorithm

The first idea for typing effects is to use Hindley-Milner typing. To capture the fact that a function of type s -[Δ]-> t is also of type s -[Δ']-> t when Δ is included in Δ', we use row polymorphism. The type of the function would now be s -[Δ; !r]-> t with !r a row variable, that is a variable that quantifies over what can be added to Δ. That type can later be instantiated to any s -[Δ']-> t with Δ included in Δ' by taking !r as the difference of Δ' and Δ.

For instance, we could define function composition:

let compose f g x = f (g x);;
val compose : ('b -[!r]-> 'c) -[!s]-> ('a -[!r]-> 'b) -[!t]-> 'a -[!r]-> 'c = <fun>

The compose function takes two functions as arguments, and returns their composition. It assumes both input functions can only produce the effect !r, and the function it returns can then only produce that effect !r. The two extra effect variables, !s and !t, are used to make the function type more general, since we want to use the partial applications, which will produce no effect at all, in a context where any function is expected.

However, doing so suffers from over-unification. Indeed, consider the following program for which we wish to infer types using effects:

let rec iter n f x = if n = 0 then x else iter (n - 1) f (f x);;
let double = iter 2;;

We would like to get the following type annotations:

let rec iter n f x = if n = 0 then x else iter (n - 1) f (f x);;
val iter : int -[!r]-> ('a -[!s]-> 'a) -[!t]-> 'a -[!s]-> 'a = <fun>

let double = iter 2;;
val double : ('a -[!r]-> 'a) -[!s]-> 'a -[!r]-> 'a = <fun>

Note that we have row variables everywhere, as usual with row polymorphism. This is because we want to be able to use a function that does not perform any effect in any place where a function that performs an effect is expected. So, while giving double the type

('a -[!r]-> 'a) -[]-> ('a -[!r]-> 'a)

would be correct, it would not allow us to use the function double f (where f is any function), in a place where a function performing an effect is expected.

However, with the usual Hindley-Milner type inference algorithm, we get something less general:

let rec iter n f x = if n = 0 then x else iter (n - 1) f (f x);;
val iter : int -[!r]-> ('a -[!r]-> 'a) -[!r]-> 'a -[!r]-> 'a = <fun>

let double = iter 2;;
val double : ('a -[]-> 'a) -[]-> 'a -[]-> 'a = <fun>

Here, double can only take a function that performs no effect at all.

So, what happened? If we look in the definition of iter, the recursive call is done with a type:

int -[!s]-> ('a -[!s]-> 'a) -[!s]-> 'a -[!s]-> 'a

This type is not the same as int -[!r]-> ('a -[!s]-> 'a) -[!t]-> 'a -[!s]-> 'a, but only an instantiation of the former. Since this is a recursive function, the types must be exactly the same, resulting in !r and !t being unified with !s. Then, when creating double, the resulting effect of the evaluation is unified with the empty effect, since top-level statements are forbidden to produce an effect (remember, we want checked effects), which prevents double from using a function that performs an effect.

The problem in the definition of iter is exactly the same that happens when we write the following in vanilla OCaml:

let rec f x y = f x x;;
val f : 'a -> 'a -> 'b = <fun>

Here, a resulting type of 'a -> 'b -> 'c would be sound as well, but requires polymorphic recursion. It is possible to do that in the OCaml type system, but requires an explicit annotation. We do not want that for effects, as it would require to annotate every single recursive function with its type to get the types we would like. Although polymorphic recursion making Hindley-Milner type inference undecidable is a folklore result, it might not be the case if limited to effect variables as we are trying to do. The existence of the solution presented below, even if it is based on a different type system, could be seen as a hint that it might actually remain decidable, but I did not explore this idea further.

Exploiting subtyping

We need to exploit the structure that exists in the problem at hand to be able to get general enough types. One property we have is subtyping: a function that performs no effect at all can be used where a function that can perform an effect is expected.

In a system with effect subtyping, we expect the following types for the two functions above:

let rec iter n f x = if n = 0 then x else iter (n - 1) f (f x);;
val iter : int -[]-> ('a -[!r]-> 'a) -[]-> 'a -[!r]-> 'a = <fun>

let double = iter 2;;
val double : ('a -[!r]-> 'a) -[]-> 'a -[!r]-> 'a = <fun>

Here, the recursive call in iter is allowed, since int -[]-> ('a -[!r]-> 'a) -[]-> 'a -[!r]-> 'a is a subtype of int -[!r]-> ('a -[!r]-> 'a) -[!r]-> 'a -[!r]-> 'a, and thus can be used in its place. double has the expected type, since the effect type variable !r did not get unified.

The advantage of using subtyping here is that we did not require polymorphic recursion, that the usual ML type inference algorithm was not able to handle. Unfortunately, by doing so, it seems like we went out of the frying pan and into the fire: we no longer need polymorphic recursion, but we need to handle subtyping instead. Fortunately, a solution exists, which is the recent MLsub inference algorithm by Stephen Dolan, which infers compact (constraint-less) principal types for programs using subtyping.

MLsub is easy to extend to support additional features, in our case checking effects. We only need to define how effects are typed. Let us first see a quick summary of MLsub’s features. MLsub extends types with type union a | b and intersection a & b, as well as neutral elements, bottom and top, for these operations. Subtyping in MLsub is structural and not based on quantification: if a type a is a subtype of b, then every value of type a is a value of type b, but the other direction is wrong. This means that to prove that a type a is a subtype of type b, only logical operations such as commutativity and associativity of & and |, or their basic properties can be used. For instance, int & string would not be a subtype of bottom, even if it is a logically empty type, because proving it would require proving that either int or string are subtypes of bottom, both of which are false. Moreover, variables as really treated as indeterminates and not as quantification, for purposes of subtyping. MLsub also has recursive types, which are needed to assign a principal type to some expressions like let rec f x = f. Finally, in order to make type inference decidable, MLsub makes a difference between positive and negative positions and variable occurrences: during type inference, | and bottom may only appear in positive positions, while & and top may only appear in negative positions. As a consequence, user-definable types must not include |, &, bottom or top, since they can be used in both positive and negative positions.

We will not get into the details of how MLsub’s inference algorithm works here. Instead, we will see how effects, that we add to MLsub, are typed. We use a multi-kinded type system, with two kinds: types and effect types. An effect type corresponds to whether a specific effect can be present or not: it can either be absent or maybe present.

Then, as with the other types, we extend this type system to add |, &, and type variables. Both top and bottom are added as well, but are redundant: top is the same as maybe present, and bottom as absent, except that absent and maybe present can be used in both positive and negative positions. Then, when an expression is typed, we use a single effect type for each effect that appears in the expression, and a catchall effect type for all other effects, which will all behave in the same way for that expression, since they do not appear in it. In other words:

This is actually the same thing that we had for row polymorphism, except that with subtyping, row variables are not as omnipresent as previously: subtyping allows us to use _ -[]-> _ for a function that does not perform any effect, whereas with only row polymorphism, we would have needed to use _ -[!r]-> _ to be able to use this function in a context expecting a function that produces an effect.

Integrating that in the MLsub inference algorithm gives us precisely what we previously wanted, that is:

let rec iter n f x = if n = 0 then x else iter (n - 1) f (f x);;
val iter : int -[]-> ('a -[!r]-> 'a) -[]-> 'a -[!r]-> 'a = <fun>

let double = iter 2;;
val double : ('a -[!r]-> 'a) -[]-> 'a -[!r]-> 'a = <fun>

Implementation and conclusion

I implemented MLsub’s type inference algorithm for that project. Although MLsub’s paper explained quite well the ideas behind MLsub to give a good enough intuition about it, I needed to read Stephen Dolan’s thesis to be able to implement it. Besides, I managed to get a simple implementation only after reading his code and realizing that a structural type with destructive unification can be used to implicitely represent the automaton with references, making the implementation of the algorithm a lot closer to that of Hindley-Milner type inference with destructive unification, and thus a lot simpler. With that representation in mind, all algorithms become a lot more natural to write and easier to understand, at least for someone which has already some experience with Hindley-Milner type inference. All in all, the typer, which only supports a very simple type system if you exclude effects and subtyping, is about 1500 lines long and requires quite complicated types in some places (one of them is a type where some constructors contain sets of elements of the type itself, requiring the use of recursive modules).

There still are some rough edges, though. First and foremost, effects cannot hold type information. This means that polymorphic effects are completely impossible. Second, it is unclear how to treat local effects (similar to local exceptions in OCaml): how can it be guaranteed that a function that raises a given local effect can never escape the scope where that local effect is defined?

The first of these problems is mainly due to the semantics of effect matching. In the case of nested effect handlers for the same effect, performing the effect inside the innermost handler causes that handler to be used. However, in some cases, that use of the effect will have been typed with respect to the outermost handler. With pre-defined effects that have a fixed type, this causes no problem. However, with polymorphic effects, they might correspond to different instantiations, breaking type safety. For instance, consider the functions below:

let g f = match f () with x -> x | effect Exit _k y -> y;;
let () =
  match g (fun () -> perform (Exit false); 6) < 7 with
  | x -> x
  | effect Exit _k y -> y

Now, g is well-typed with type

(unit -[Exit : 'a, !r]-> 'a) -[!r]-> 'a

which is a subtype of

(unit -[!r]-> 'a) -[!r]-> 'a

Instanciating it with !r = Exit : bool and 'a = int makes the whole expression well-typed, when it tests if false < 7 at runtime, breaking type safety.

A way to prevent that which would not be overly restrictive in terms of expressivity would be to disallow such cases in the type system, and add protect and unprotect operators that would hide the effect of a subexpression from the surrounding effect handler. They could even be added in a type-directed way, but the semantics of the language will depend on the typing.

Concerning the second problem with local effects, a straightforward check is to ensure the added effect does not leak into the return type of the function. However, I have no proof that it is correct for now, so if you have one or find a counter-example, please leave a comment about it.

In case you want to learn more about MLsub, I encourage you to read Stephen Dolan’s MLsub paper, or even his whole thesis. If you are interested in joujou’s typing rules, you can have a look at them in the report for the project (in French).