Continuation monad with polymorphic return type

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?

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
``````
1 Like

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

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.

4 Likes

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.

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

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) }
``````

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

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