On Wed, Oct 25, 2017 at 4:35 AM, Richard W.M. Jones <rich@annexia.org>
wrote:

>
> Having said all that I was writing a little ML language last
> year and I tried to implement a return statement, but it was very
> awkward to work out how to map that to my lambda calculus, so
> I understand how return statements are rather difficult to implement
> in practice.
>
> Rich.
>
>

The return statement is in fact a tamed exception, as it provides an
exceptional, i.e., a non-local control flow. However, exceptions are not
first class citizens in functional programming languages as they are not
explicitly represented in typed lambda calculus, and are not really
represented in the type system (in a sence that an expression with and
without exception has the same type). Thus dealing with expressions that
may raise an exception is hard, as well as dealing with any expression that
has a side effect. OCaml multicore project is actually bringing more than
the multicore support, they also reify the effect system into the language.
Thus exceptions, as well as the return statements, can be soon easily
implemented on top of the effect system and can be reasoned in a much more
natural way.

With all that said, safe and first class exceptions can be implemented in
plain OCaml, or any other functional programming language that provides
higher order polymorphism (type classes, functors, etc). The limited form
of an exception can be implemented even without it. As it was already
noticed, the Maybe monad, as well as the Error monad, or any other monad
that reifies non-total computations can be used to implement a poor man
return statement. The problem is that when one computation yields the null
value, the rest of the computation chain is still evaluated. This is not a
big issue if a chain is written manually (i.e., is a block of code, like in
your example), but it could be serious if the chain is very long (i.e.,
processing a big list), or even worse infininte. If the problem with a list
of computations can be solved on the monad implementation (as we do in the
[Monads][2] library), the problem with the infinite computation can be
easily addressed in a non-total monad.

The answer is to use the continuation passing style (CPS). We can use
delimited continuations (as in the upcoming multicore), or we can use plain
non-delimited continuations. The rough idea, is that if you have function
that needs to escape the computation prematurely, you can pass a
continuation to that function, e.g.,

     let do_stuff return =
       if world_is_bad then return None
       else if moon_phase_is_bad then return None
       else return (compute_some_stuff ())

You may notice, that we still need the else statement as our return
function has type `'a -> 'a`, but for the non-local return we need
something of type `'a -> 'b`, to implement this we need to switch to the
continuation passing style, where each computation is a continuation, i.e.,
a function of type `('a -> 'b) -> 'b`. For example, this is how the
List.fold function will look in the CPS:

        let fold xs ~init ~f =
          let rec loop xs k = match xs with
            | [] -> k
            | x :: xs -> fun k' ->  k (fun a -> loop xs (f a x) k') in
          loop xs (fun k -> k init)

Programming in this style directly is a little bit cubersome, but the good
news, is that the continuation passing style can be encoded as a monad. The
[Continuation monad][2] has only one extra operator, called call/cc, that
calls a function and passes the current continuation (i.e., a first class
return statement) to it, e.g.,

       let do_stuff ~cc:return =
         if world_is_bad then return () >>= fun () ->
         if moon_phase_is_bad then return () >>= fun () ->
         compute_some_stuff ()

     let main () = Cont.call do_stuff

The interesting thing with the non-delimited continuation is that  `cc`
here is a first class value that can be stored in a container, resumed
multiple times, etc. This gives us enough freedom to implement lots of
weird variants of a control flow, e.g., return statement, exceptions,
couroutines, concurrency, and, probably, even the [COMEFROM][4]
instruction. Basically, a continuation is a first class program label.

Is it good or bad, you can decide yourself. Maybe this is too much freedom,
however, this is totally a part of the lambda calculus, and is not using
any type system escape hatches, like exceptions, even given that the
`return` function has type `a -> 'b t`.

P.S. Although I took your examples for demonstration purposes of the Cont
monad, I still believe that for your particular case a non-total monad
would be much nicer and more natural. Using the Monads library Error monad,
it can be expressed as:

   let do_stuff () =
     if world_is_bad then failf "the world is wrong" () >>= fun () ->
     if moon_phase_is_bad then failf "look at the Moon!" () >>= fun () ->
     compute_some_stuff ()

The Error monad implements the Fail interface, that provides mechanisms for
diverging the computation with an exception (not real exception of course),
as well as provides the catch operator. The Error monad has a much stricter
type discipline, and limited control flow variants, that can be considered
as boon in most cases.


[1]: http://kcsrk.info/ocaml/multicore/2015/05/20/effects-multicore/
[2]: http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.html
[3]:
http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.Monad.Cont.html
[4]: https://en.wikipedia.org/wiki/COMEFROM
[5]:
http://binaryanalysisplatform.github.io/bap/api/v1.3.0/Monads.Std.Monad.Fail.S.html