How to enforce constraints / subtype in a polymorpic function

Learning
1

Background: I’m attempting to make some convenience wrappers around running processes. Lwt_process provides with_process{,_in,_out} (which all use a different “process type” that share a common base). And I have a number of different convenience functions, so I don’t want to write each wrapper 3x with different names.

So I thought I’d just accept “the spawn function” which is one of the above, but I’m having trouble getting it to compile. Here’s a simplified example which compiles, using a fake parameterized process type:

type 'a some_proc = Foo of ('a * Unix.process_status)
let get_status: 'a some_proc -> Unix.process_status = function Foo (_, st) -> st

let run (type use_result) (type summary) (type proc)
  ~(spawn: string list -> (proc some_proc -> summary) -> summary)
  ~(use: proc some_proc -> use_result)
  ~(summarize: use_result -> (unit, string) result -> summary)
  (cmd: string list): summary =
    spawn cmd (fun proc ->
      let use_result = use proc in
      let proc_result = match (get_status proc) with
        | WEXITED 0 -> Ok ()
        | _ -> Error "command failed"
      in
      summarize use_result proc_result
    )

The idea being there’s a block function which the user provides to “do something with the running process”, and there’s also a summarize function which takes the result of the user’s block, the result of the process status, and spits out a single result value. I’ll provide a number of these for common cases, for example one which simply returns use_result and throws if the command failed, and another which returns a (use_result, string) result.

Now, if I change the some_proc type into a more realistic example using a class (to match the actual Lwt_process implementation):

type 'a some_proc = < status : Unix.process_status; .. > as 'a
let get_status: 'a some_proc -> Unix.process_status = fun proc -> proc#status

…then I get:

File "src/test.ml", line 41, characters 26-30:
Error: This type proc should be an instance of type
         < status : Unix.process_status; .. >

I agree, what I want to know is how can I tell ocaml that is is, via some kind of constraint / subtype annotation? And I’m also curious why the first one works. Is it because the class-based version is using subtyping while the initial version is just a poymorphic type? Am I using these words right? :wink:

2

I’d love to be wrong, but I don’t think that is possible.
However, do you really need it in this case ?
Your code compiles by just removing the (type proc) locally abstract type

type 'a some_proc = < status : Unix.process_status ; .. > as 'a
let get_status: 'a some_proc -> _ = function proc -> proc#status
let run (type use_result summary)
  ~(spawn: string list -> ('proc some_proc -> summary) -> summary)
  ~(use: 'proc some_proc -> use_result)
  ~(summarize: use_result -> (unit, string) result -> summary)
  (cmd: string list): summary =
    spawn cmd (fun proc ->
      let use_result = use proc in
      let proc_result = match (get_status proc) with
        | WEXITED 0 -> Ok ()
        | _ -> Error "command failed"
      in
      summarize use_result proc_result
    )
3

Aha, thanks! I should read more about abstract types, I had always assumed (type foo) was equivalent to using 'foo, with the added benefit that typos don’t accidentally introduce additional polymorphsm.

It looks like this distinction is described in https://caml.inria.fr/pub/docs/manual-ocaml/manual027.html :

The (type typeconstr-name) syntax construction by itself does not make polymorphic the type variable it introduces, but it can be combined with explicit polymorphic annotations where needed.

4

The type annotation that you wanted to write is

let run =  'use_result 'summary 'proc.
  spawn:(string list -> ('proc some_proc -> 'summary) -> 'summary)
  -> use:('proc some_proc -> 'use_result)
  -> summarize: ('use_result -> (unit, string) result -> 'summary)
  -> cmd:(string list) -> 'summary

With this version, the code compiles.
When subtyping is involved one cannot always use locally abstract type to enforce polymorphism, and it is necessary to use explicit universal quantification.