One recent arrival in `Core`

is `with_return`

, a function that lets you return early from a computation. Here's a trivial example:

let sum_until_first_negative list = with_return (fun r -> if x >= 0 then acc + x else r.return acc))

One thing that might not be obvious in the above example is what the type of `r`

is. It turns out it's this:

type 'a return = { return : 'b . 'a -> 'b }

The reason for this is to have the return function be truly polymorphic in its return value. That way, like `raise`

, it can be used in any context because its return value will unify with any type.

Note that the `sum_until_first_negative`

example will work even without the record trick, because `r.return`

is used in only one place (and more importantly, with only one type.) But if you want this to work in the general case, you need the record.

So, how does one go about implementing this? Here's the implementation that's currently in Core. Note that we use a locally defined exception, to make sure that only this exception handler can catch the exceptions in question. Also, we use a ref to store the value being returned.

let with_return f = let module M = struct exception Return end in let r = ref None in let return = { return = (fun x -> r := Some x; raise M.Return); } in try f return with M.Return -> match !r with | None -> assert false | Some x -> x

In OCaml 3.12, we can make this code, simpler, safer and more efficient:

let with_return (type t) (f : _ -> t) = let module M = struct exception Return of t end in let return = { return = (fun x -> raise (M.Return x)); } in try f return with M.Return x -> x

I'd like to be able to improve this further by getting rid of the overhead of the record, but I suspect it's not possible.

It's worth noting that `with_return`

has its pitfalls. For example, there's no guarantee that the return always terminates the full computation. For example, the following code:

let foo = with_return (fun r -> try r.return 0 with _ -> 1)

will return 1, not 0. Another interesting behavior is to see what happens when `r.return`

is called outside the scope of the closure passed into `with_return`

. Consider the following convoluted function, which returns an optional function which, when called, calls r.return.

let foo = with_return (fun r -> Some (fun () -> r.return None))

If you call the function contained in foo, you'll get the following response:

# let f = Option.value_exn foo;; val f : unit -> 'a = <fun> # f ();; Exception: Return 0.

This isn't particularly surprising, once you understand the implementation, and it's semantically fairly reasonable. The only thing you could really ask for beyond this is a warning that the return has escaped its scope, but I think this is beyond the powers of the type-checker.

That’s a lovely hack. I’m still getting used to all the 3.12 features…

Slightly lighter use of the record-based solution, for OCaml 3.12:

with_return (

fun {return} ->

ignore (return () : int);

ignore (return () : string)

)

You can kind of avoid the first problem with `with_return` with something like this:

exception Return

let with_return (type t) (f : _ -> t) =

let ret : t option ref = ref None in

(* can only be set once *)

let set_ret x = match !ret with

Some _ -> () | None -> ret := Some x in

let get_ret () = match !ret with

Some x -> x | None -> assert false in

let return = { return = (fun x -> set_ret x; raise Return) } in

(try set_ret (f return) with Return -> ());

get_ret ()

To get:

# let fixed_foo = with_return (fun r -> try r.return 0 with _ -> 1);;

val fixed_foo : int = 0

It is not an entirely satisfactory fix because the handler for the inner `try` is still run, and its value discarded.

To remove the overhead of the record, I propose the following:

module Ret: sig

type ‘a return

val with_return: (‘a return -> ‘a) -> ‘a

val return: ‘a return -> ‘a -> ‘b

end =

struct

type ‘a return = ‘a -> exn

let with_return (type t) f =

let module M = struct exception Return of t end in

try f (fun x -> M.Return x) with M.Return x -> x

let return r x = raise (r x)

end

Assuming this module is opened, you can write:

let sum_until_first_negative list =

with_return (fun r ->

List.fold list ~init:0 ~f:(fun acc x ->

if x >= 0 then acc + x else return r acc))

which is not very different from your original example.

Indeed, I think that one of our earlier implementations had exactly this flavor. We moved to the record solution to avoid namespace polution — return is used for every monad, and so is a pretty valuable word.

But I hadn’t thought about the performance implications at the time. Maybe we’ll change back…

By the way, another neat solution to this is to use the type `never_returns`. This is an uninhabited type that we use to indicate that function doesn’t return. There’s also a function `never_returns` with this signature:

val never_returns : never_returns -> ‘a

which basically just calls assert false in its implementation. One could then replace `’a return` with

‘a -> never_returns , and write the code as follows:

let sum_until_first_negative list =

with_return (fun r ->

List.fold list ~init:0 ~f:(fun acc x ->

if x >= 0 then acc + x else never_returns (r acc)))

But I think in the end that’s more confusing.

Craig and I talked about why the record is necessary. If you write the function without the record, you basically get a function

`val with_return1 : (forall 'a) (forall 'b). (('a -> 'b) -> 'a) -> 'a`

(I added the “forall”s, they aren’t actually valid ocaml.) What you get with the record is basically:

`val with_return2 : (forall 'a). [((forall 'b) ('a -> 'b)) -> 'a] -> 'a`

Although the naive recordless

`with_return1`

function could be given the more general second type, ocaml has no way to express that type without the use of a record.We were originally confused by the fact that the two types are logically equivalent (i.e., they’re equivalent when viewed as logical statements). I think we thought that because of that, the compiler should use the more general second type when you actually use with_return. But that just underlines the fact that logical isomorphism only implies coercions both ways, not that those coercions are automatic. Indeed, I believe you can write

`with_return2`

using just`with_return1`

and pure ml (no exceptions, for example).The type of with_return is also basically Pierce’s law, which is the logical statement ((P=>Q)=>P)=>P. The Curry-Howard isomorphism says that the type of anything you write in pure ml corresponds to an intuitionistically valid logical statement. Classical logic is equivalent to intuitionistic logic plus Pierce’s law. I think this is why classical logic is sometimes thought of as intuitionistic logic “plus continuations”, or something along those lines.

Anybody with actual knowledge should feel free to correct anything I’ve said above.