What OCaml type to extract IO to?

[Lysxia]

Currently we have

type 'a io = ('a -> unit) -> unit

This has the benefit of being usable everywhere, without having to depend on a common type definition. However this type is a bit too big: some inhabitants may not call the continuation, e.g., fun _ -> ().

This implies that we cannot define a total function 'a io -> 'a. You can still define a function with that signature by having your continuation put the 'a result in a reference, and throw an exception if the reference is not found (that's how very_unsafe_eval is defined), but that seems rather heavyweight.

Previously I had been using this polymorphic continuation-passing type, that ensures that an io computation must either terminate by calling the continuation, or diverge:

type 'a io = { apply : 'r . ('a -> 'r) -> 'r }

But, as I hinted at above, writing OCaml code to use that is cumbersome because you need to have the type io in scope.

Of course, I should also mention the following:

type 'a io = unit -> 'a

but it doesn't seem to behave well with deeply recursive functions.

One more alternative is to use that simplest type as a core, and wrap it in a CPS transformer in Coq to get the benefits of the former two definitions.

[Lysxia]

I've settled for ('a -> Obj.t) -> Obj.t.