Gagallium

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 } ->
      if pred head then
        (* We found the element we're looking for! *)
        right (
          head,
          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...