Question on continuations

Learning
, ,
1

Is it possible to define printf in terms of sprintf without the use of ksprintf (or any of the other formatted output functions with continuations)?

My actual use case involves a custom GADT, not format strings, but I think the aspect of what I’m struggling with in my use case can be simplified down to this question. I have a function run : 'a Type.t -> 'a that interprets the arguments it’s passed, and I want to effectively wrap a call to run in another function that invokes run and does something with its result. I also want that function’s type signature to be 'a Type.t -> 'a. I think this might not be possible because I don’t have a function like krun : (k -> 'a) -> 'a Type.t -> 'a and the reason I don’t have that function is that I don’t have (or want to have) an exposed type k that represents an interpreted result (in the case of ksprintf, k is string).

2

Just from your description, I don’t see what is the problem. For example, the function run is wrapped inside run2. What am I missing?

Cheers,
Nicolas

type _ ty =
  | Int : int ty
  | String : string ty
let run : type t. t ty -> t = function
  | Int -> 42
  | String -> "Hey"
let run2 : type t. t ty -> t = fun t ->
  let x = run t in
  match t with
  | Int -> x * 2
  | String -> x ^ x
3

A key aspect of this is that the arity of 'a is not known, as with format strings. In the example you give, the GADT only supports simple types, but in format strings as well as with the Type.t I actually have, you could also have something like run (type_ : (string -> int -> bool) Type.t) "foo" 5 and it would return a boolean value.

The closest I’ve been able to come up with, again with the format string example, is something of a poor man’s version:

module Args = struct
  type 'a t =
    | [] : string t
    | ( :: ) : 'a * 'b t -> ('a -> 'b) t
end

let printf (type a) (fmt : (a, _, _) format) (args : a Args.t) =
  let rec apply : type t. t -> t Args.t -> string =
    fun f args ->
      match args with
      | [] -> f
      | hd :: tl -> apply (f hd) tl
  in
  Out_channel.output_string stdout (apply (Printf.sprintf fmt) args)
;;
4

You can implement an interpreter yourself, that call sprintf once all argument has been interpreted, but this is mostly equivalent to rewriting a specialized version of ksprintf.

Without more context, your requirement feels a bit contradictory to me. Typically, the function that you want to write

is an interpreter with a continuation argument.

In particular, if you want to call a function on the result of the interpreter, you need to have a type for this result, thus I don’t know how you expect to not expose the type of the result of the interpreter.