Continuation monad with polymorphic return type

Learning
1

Starting from the usual continuation monad given a fixed type answer

module Cont0 = struct
  type 'a cont = 'a -> answer
  type 'a t = 'a cont -> answer
  let ret (x: 'a) = fun k -> k x
  let bind (x: 'a t) (f: 'a -> 'b t) : 'b t =
    fun k -> x (fun v -> f v k)
end

I would like to change it so that the return type is not fixed as answer, but can vary. As a starting point I defined the types as follows (I need to keep the same signature for the module), but I do not know how to write the bind:

module Cont2 = struct
  type ('a,'b) cont = 'a -> 'b
  type 'a t = Ret : (('a,'b) cont -> 'b) -> 'a t
  let ret (x: 'a) = Ret (fun k -> k x)
  let bind (x: 'a t) (f: 'a -> 'b t) : 'b t = ???
end

Is it possible to do so?

1 Like
2

I don’t have a solution with existential types, but a continuation monad with a universal quantification on answer would make more sense to me (the idea is that the caller of the continuation can choose the result type):

module Cont = struct
  type ('a, 'b) cont = 'a -> 'b
  type 'a t = { cont : 'b . ('a, 'b) cont -> 'b }
  let ret (x: 'a) = { cont = fun k -> k x }
  let bind (x: 'a t) (f: 'a -> 'b t) : 'b t =
    { cont = fun k -> x.cont (fun v -> (f v).cont k) }
end
2 Likes
3

Of course it is possible to implement a continuation monad that is polymorphic in its return type. The continuation monad is, well, a continuation underneath the hood, and a continuation has type ('a -> 'r) -> 'r, a common definition of the cont monad is.

type ('a,'r) cont = Cont of (('a -> 'r) -> 'r)

You can look at the monads (opam install monads) library that provides continuation monads and monad transformers, here is the implementation, if you’re interested in details.

P.S. of course the result type is fixed during the computation, so it can’t be changed in the bind operator, but each application of the run function can have a different result type. You can use dynamic types as a trade-off solution (the trade-off would be the lack of static typing of the result type).

1 Like
4

The problem is known as “answer type polymorphism” in the literature, just search for it. IIRC, @thierry-martinez’s solution is the correct one for pure computations, without control operators. It breaks when you add call/cc, unless you also use an effect system to delimit regions of the program that can have different answer types. A reference: Halo Thielecke, From Control Effects to Typed Continuation Passing, POPL 2003.

5 Likes
5

I don’t know what your goal is, but here’s an idea: I’ve thought about doing this:

  1. when you’re evaluating the CPS-term by supplying it with a final continuation, supply one that assigns the final value to a reference and throws an exception.
  2. catch the exception and recover the final value.
  3. this should allow the answer type to be empty, or abstract, or whatever, b/c nobody will ever construct a value of that type.

I haven’t worked this thru, but it seems like it should work.

6

Thanks for all the replies. The suggestion of @thierry-martinez works for bind, but it breaks when I extend it with a fail operator (which might be related to the call/cc remark by @xavierleroy):

module Cont = struct
  type 'b fcont = unit -> 'b
  type ('a,'b) cont = 'a -> 'b fcont -> 'b
  type 'a t = {cont: 'b. (('a,'b) cont -> 'b fcont -> 'b)}
  let ret (x: 'a) = {cont= fun k fcont -> k x fcont}
  let bind (x: 'a t) (f: 'a -> 'b t) : 'b t =
    {cont = fun k fcont -> x.cont (fun v fcont' -> (f v).cont k fcont') fcont}
  let fail () = fun k fcont -> fcont ()
  let rec branch l = {cont = fun k fcont ->
    match l with
    | [] -> fcont ()
    | b :: bs -> (b ()).cont k (fun () -> branch bs k fcont) }
end

I get an error that my type is not general enough for the fun

Error: This field value has type ('c, 'd) cont -> 'd fcont -> 'd
       which is less general than 'b. ('a, 'b) cont -> 'b fcont -> 'b

What I’m trying to write for this branch function is to take a bunch of frozen computations, run them in order until one fail (then try the next one) or until the program terminates.

I tried splitting the recursive function to make it generic enough:

  let rec gen_branch : 'b. (unit -> 'a t) list -> ('a,'b) cont -> 'b fcont -> 'b =
    fun l k fcont ->
    match l with
    | [] -> fcont ()
    | b :: bs -> (b ()).cont k (fun () -> gen_branch bs k fcont)
  let branch l = {cont = gen_branch l}

but I get the same error (at the gen_branch l call).

For the moment I’m using an approach similar to what @Chet_Murthy suggests, using a reference instead of an exception. I’m still curious to see if I can get enough polymorphism to succeed. I’m going to have a look at the papers Xavier suggests.

Finally, to reply to @ivg, the issue is that my monad need to conform to the type 'a t, i.e., I cannot mention the return type there. I agree the return type should be the same all the time for each instance of run.

1 Like
7

I haven’t looked at your code closely, but it seems that there’s a missing projection in the recursive call:

let rec branch l = {cont = fun k fcont ->
  match l with
  | [] -> fcont ()
  | b :: bs -> (b ()).cont k (fun () -> (branch bs).cont k fcont) }
8

This limitation sounds rather artificial, probably it would be eaiser to get rid of it, if you really need a polymorphic in the return type computation. Alternatively, you can constraint the type of your monadic computation to match the desired signature by choosing a concrete type of the return value, e.g.,

type 'a t = ('a, int) cont

As a last resort solution, you can use a universal type or just an extensible variant, e.g.,

type ret = ..
type 'a t = ('a -> ret) -> ret

With that said, I think it would be a good idea to if you will express your problem on the high level to avoid the xy-problem. It could be that there are cleaner solutions as it looks like that you’re digging in a wrong direction :slight_smile:

9

This was it, thanks a lot! (Another one was missing, but it now works.)