Lately, it seems all I've been doing is writing. There's been that paper about the implementation of Mezzo, which I'm supposed to push out at some point. There's that ICFP submission (blog post pending) which we've been writing with some other cool kids from the lab. That's not counting the various presentations, research statements, and other misc. documents that I've been busy with...

Last week, I was (again!) writing, this time working on my part for a journal version of our ICFP paper, and I was trying to write a small tutorial with longer examples and a better introduction to Mezzo. After explaining tail-recursive concatenation for the n-th time, I decided to try out explaining a new example. Here's the result.

The example is about an interesting programming pattern in Mezzo, which I dub "control-flow inversion". The idea is not new: we've been using it for iterators, but is was somehow buried under the details of how iterators work. The present blog post tries to present it in a more self-contained way. It somehow showcases both the strengths and weaknesses of Mezzo as it stands right now. Hopefully we'll improve the shortcomings soon.

## An ownership problem

Imagine you want to find one element among a list that satisfies a given predicate. In OCaml, this can be easily done:

```let rec find0 (pred: 'a -> bool) (l: 'a list): 'a option =
match l with
| [] -> None
| hd::tl ->
if pred hd then
Some hd
else
find0 pred tl
```

However, there's an ownership problem here. Assuming an element is found, then doing the following breaks the ownership discipline.

```let l = ... in
match find0 ... l with
| Some elt -> (* Ownership problem here! *)
| None -> ...
```

Indeed, the element `elt` is reachable through two different, seemingly distinct paths: the variable `elt` itself, and the list `l` where the elements remains. In a language that tracks ownership, such as, but not limited to, Mezzo, this is a problem.

Indeed, if you want your `find` function to work for any list of `a`, then your function cannot make any assumptions on `a`, and has to assume that elements of type `a` have a unique owner. The `find0` function above will thus be rejected by Mezzo.

An alternative solution would be to add an extra constraint on a caller of the function, and require that the type `a` be duplicable. There is a mechanism for that in Mezzo. Here, however, we wish to attain a more general solution.

## The classic solution

The classic solution is to reverse the control-flow: instead of asking `find` to provide us with the element it found, we are going to provide `find` with whatever we want to do with the element. That is, we're going to pass a first-class function to `find`.

The signature of `find` thus becomes, in Mezzo:

```val find1: [a] (l: list a, pred: a -> bool, f: a -> ()) -> ()
```

(We could have `f` return an element of type `b` and then have `find1` return `b` as well. We keep it simple for now.)

Remember that in Mezzo, unless marked with `consumes`, arguments are preserved (i.e. their ownership is taken and returned). The function above thus preserves a list `l`; it takes a predicate and a function `f`. The function `f` is allowed to operate on an element but must leave it untouched.

The function `f` may want to perform side-effects: we can provide a better signature, as follows.

```val find2: [a, s: perm] (l: list a, pred: a -> bool, f: (a | s) -> ()) -> ()
```

One may use `find2` as follows.

```let l = ... in
(* l @ list (ref int) *)
let found = ref None in
find2 (l,
(fun (x: ref int): bool = !x > 2),
fun (x: ref int | found @ ref (int option)): () =
found := Some (!x)
);
match !found with
| Some x ->
(* Found an integer greater than 2, it's x *)
...
| None ->
...
end
```

This is awkward for a variety of reasons. First, the control-flow feels very unnatural. We're actually losing control. Second, writing first-class functions requires a lot of annotations. Finally, `find2` is actually no more useful than a regular `iter` function.

## The better solution

Turns out (ta-da!) we can actually do better. We can write this function in "direct style" (i.e. have the soon-to-be `find3` return the element to its caller) while still maintaining ownership guarantees. Without any runtime test!

The key insight is to have a `restore` function that consumes the ownership of the element in order to regain the ownership of the original list. This, of course, will rely a little bit on dependent types.

```alias restore_t (x: term) a (l: term) =
{ p: perm } (
(| consumes (p * x @ a)) -> (| l @ list a) | p
)
```

An element of type `restore_t x a l` is a package of a function along with an existentially-quantified permission `p`. The function, in order to be called, requires `x @ a * p`, which it consumes. In exchange, one gains `l @ list a`.

Phrased differently, this is a one-shot function (`p` is existentially-quantified, so the function can only be called once), which consumes `x @ a` to obtain `l @ list a`.

Since the permission `p` is existentially-quantified, we must treat it as affine. Because calling `f` requires `p`, after `f` has been called once, `p` is gone, meaning that `f` can no longer be called: this is effectively a one-shot function. The iterator blog post refers to this as a magic wand from `x @ a` to `l @ list a`.

As you may have guessed by now, the signature of `find3` is as follows.

```val find3: [a] (consumes l: list a, pred: a -> bool) ->
either (| l @ list a) (x: a, restore_t x a l)
```

The function takes, just like `find0`, a list `l` and a predicate function `pred`. The return type is a sum. In the `Left` case, no element has been found, so the unit value is returned, along with full ownership of the list. In the `Right` case, the caller does not regain ownership of the list `l`. What it gains instead is an element `x` (the element that was found) along with the `restore` function we just saw.

Here's some sample client code for `find3` which, as you can see, is written in the same, natural style as the OCaml code for `find0`, except for the call to `restore` (but well, our language tracks ownership, so the user will have to talk about ownership too...).

```val _ =
(* Create a sample list. *)
let l = cons (newref 1, cons (newref 2, nil)) in
(* Try to find an element greater than 1 *)
match find (l, fun (x: ref int): _ = !x > 1) with
| Left ->
(* No such element has been found *)
()
| Right { contents = (elt, restore) } ->
(* The element [elt] has been found. *)
print elt;
(* Calling the (ghost) [restore] function allows one to give up ownership
* of [elt] and recover ownership of [l] instead. *)
restore ()
end;
(* In any case, we can use [l] afterwards. *)
assert l @ list (ref int)
```

In can hear the impatient readers eager to see the implementation of `find3`. Behold! Here it is.

```val rec find3 [a] (consumes l: list a, pred: a -> bool):
either (| l @ list a) (x: a, restore_t x a l)
=
match l with
| Nil ->
(* We found no suitable element. *)
left ()
| Cons { head; tail } ->
(* We found the element we're looking for! *)
right (
fun (| consumes (head @ a * tail @ list a)): (| l @ list a) =
(* Here's permission p:   ^^^^^^^^^^^^^ *)
())
else
(* The element we're looking for may be further away. *)
match find3 (tail, pred) with
| Left ->
left ()
| Right { contents = (elt, restore) } ->
let flex s: perm in
right (
elt,
fun (| consumes (elt @ a * head @ a * s)): (| l @ list a) =
(* Here's permission p:    ^^^^^^^^^^^^ *)
restore ())
end
end
```

It's a 20-liner, so don't be afraid, and let's break it down.

### Boring case

In the case that we've reached the end of the list, we return the `left` injection with the unit type. The ownership of the list is properly returned to the caller: it's the empty list.

### Interesting case

Let us now turn to the first interesting case: the element we've hit is precisely the one we were looking for.

We return `head`: this corresponds to the `x` we wrote in the function signature.

Let us now examine the definition of `restore`. It requires the permission for `head`: this is line with the definition of `restore_t`. The definition of `restore_t` also mentions a certain permission `p`: in our case, this is `tail @ list a`. The `restore` function also captures the duplicable permission `l @ Cons { head = head; tail = tail }`: duplicable permissions can be captured in Mezzo. Combining these three permissions, without performing any run-time operation, `restore` returns full ownership for the list `l`.

In Mezzo lingo: `head @ a * tail @ list a * l @ Cons { head = head; tail = tail } ≤ l @ list a`.

There an existential-packing involved: the type-checker performs this automatically and packs `tail @ list a` as `p` (this is real, unedited Mezzo code that I'm showing).

One can glance briefly further down, to see that in the last case, the actual permission `p` is a different one. Without the existential quantification, the types would fail to match. The actual value of `p` ("existential witness") depends on the case.

### Actually not-boring case

In the case that the element failed to be found further down the list, the recursive call to `find3` returns `Left`. Even though the code is terse, let us break down what happens.

In the `Left` branch, we learn that we regain full ownership of whatever we called `find3` with: in our case, we gain `tail @ list a`. The type-checker knows that we still possess `head @ a * l @ Cons { head = head; tail = tail }`: it thus recombines the three permissions to show that `left ()` actually produces `Left { contents = () } | l @ list a`, per the return type of `find3`.

There's a lot of under-the-hood machinery that is completely transparent: I'm going to be bold and declare that I find this pretty cool.

### Very interesting case

The last case is, naturally, the most interesting one. The element we're looking for has actually been found further down the list. The recursive call provided us with: the element `elt`, along with `elt @ a`; a function `restore` that consumes `elt @ a` and returns us `tail @ a`; a certain permission that `restore` needs in order to be called. It's the existentially-quantified one. Let's name it `s`.

We return the element we've found, `elt`, along with a function that consumes `elt @ a` and returns full ownership of the list. How do we write that function?

That function will consume `elt @ a`, which is sort of expected. It also needs other permissions: it needs the "certain permission" `s`, in order to call the inner `restore` function. We also need `head @ a` if we are to piece back everything together to recreate ownership of `l`.

Entering the new `restore` function, we have `elt @ a * s * head @ a`. Calling `restore` consumes `elt @ a * s`, and gives `tail @ a`. The rest of the story is familiar: all is well and ownership of `l` is returned.

## Wrapping it up

In order for the story to have a happy ending, we must somehow get rid of the run-time operations for `restore` which is, in essence, a no-op. Turns out the story's not that good: we don't have ghost functions in Mezzo. That's a pretty big deal actually: it's a major feature to add into the language. One needs to think carefully about termination criteria. In our example, since our data types are inductive, and never co-inductive, one can use the length of the list to show that `restore` only ever calls itself with a smaller parameter. But imagine we have integers: should we use an external solver to prove that `f(x) < g(x)`? Should we write our own? What about other termination criteria?

So it's a little bit frustrating that the run-time operations are still there. Hopefully that's something that we'll fix at some point. It seems there's still some valuable research to be done about Mezzo...