How to extend and narrow down polymorphic types?

Learning
1

The gist is: I don’t think I understand how polymorphic types are supposed to work, repro Sketch.sh - Interactive ReasonML/OCaml sketchbook

I have a dependency, that I don’t control with types similar to:

type err = [ `Green | `Blue ]

type 'e factory = unit -> (string, 'e) result

I have module that I want to have an API similar to (a more complete and complex example is added here: Sketch.sh - Interactive ReasonML/OCaml sketchbook):

module type Worker = sig
  type 'e err2 = [ err | `My_err of 'e ]

  type 'a do_work1 =
    err factory -> (string -> ('a, err) result) -> ('a, err) result

  val do_work1 : 'a do_work1

  type 'e do_work_err = Err1 of err | Err2 of 'e

  type ('a, 'e) do_work2 =
    err factory ->
    (string -> ('a, 'e err2) result) ->
    ('a, 'e do_work_err) result

  val do_work2 : ('a, 'e) do_work2
end

In this case for example do_work calls the factory and passes its output to a callback. do_work2 is an extended version - it allows the callback to return a custom error as well (notice that do_work2 splits the errors into factory error and user/work error)

The issue is that I can’t figure out how polymorphic types are supposed to work - I thought that the last call should work - do_alpha returns a [ Green | Blue ] error and do_work know to handle [ Green | Blue | My_err ]:

module My_thing (Worker : Worker) = struct
  let do_alpha () s : (int, err) result = Ok (String.length s)

  let do_beta () s : (int, string Worker.err2) result = Ok (String.length s)

  let factory : err factory = fun () -> Ok "factory"

  let res1 = Worker.do_work1 factory (do_alpha ())

  (*
    not working - expected:
    let res11 = Worker.do_work1 factory (do_beta ())
  *)
  let res2 = Worker.do_work2 factory (do_beta ())

  (*
    not working - not expected:
    let res11 = Worker.do_work1 factory (do_beta ())
  *)
  let res22 = Worker.do_work2 factory (do_alpha ())
end

error:

let res22 = Worker.do_work2 factory (do_alpha ())
                                           ^^^^^^^^^^^^^
Error: This expression has type string -> (int, err) result
       but an expression was expected of type
         string -> (int, 'a Worker.err2) result
       Type err = [ `Blue | `Green ] is not compatible with type
         'a Worker.err2 = [ `Blue | `Green | `My_err of 'a ]
       The first variant type does not allow tag(s) `My_err
2

I have not analysed your code (there is a lot of it), so it may not be your point, but a variant of type [`A |`B] does not have an uncoerced intersection with one of type [`A|`B|`C]. These will intersect:

[>`A|`B] with [`A|`B|`C]
[`A|`B] with [<`A|`B|`C]
[>`A|`B] with [<`A|`B|`C]

You may be unnecessarily typing function arguments instead of letting them be inferred as contravariant.

3

You will need to manually coerce your error: (do_alpha () :> (int, [`Blue | `Green | `My_err of 'a]) result). See OCaml - Polymorphism and its limitations.

4

thanks @mefyl , this fixed the type error:

  let res22 =
    Worker.do_work2 factory
      (do_alpha () :> string -> (int, [ `Blue | `Green | `My_err of 'a ]) result)

or a convert function, that needs to be called in module Worker:

  let convert fn =
    (fn : string -> ('a, err) result :> string -> ('a, 'e err2) result)
 ...
 convert (do_alpha ())

but it is quite ugly and not nice to expect all calls to go through a conversion function;

Is it possible to specify this at the type level?

I kind of need to type the function types, because my real world use case is more complex. But I think that you are right that the problem might be related to the variance - is there any way to specify that within do_work2: err is contravariant to 'e err2 (mefyl’s example fixed the issue above with a coercion at the call site)?

  type err = [ `Green | `Blue ]

  type 'e err2 = [ err | `My_err of 'e ]

  type ('a, 'e) do_work2 =
    err factory -> (string -> ('a, 'e err2) result) -> ('a, 'e) result
5

I am not an expert on this but my main contribution would be that the less you can annotate your polymorphic types (whether function arguments or return values) the better, because polymorphic variants are naturally polymorphic. So if you put this in your ocaml REPL you will see that the type of this:

function | `A -> `X | `B -> `Y

is

[< `A | `B ] -> [> `X | `Y ].

In other words, in the absence of specific type annotation the function is covariant on its return value and contravariant on its arguments, which is what you want.

But in answer to your question, you can define a polymorphic type thusly:

type 'a t = [> `A] as 'a

Then the expression let x:'a t = `B reveals the type of x to be [> `A | `B ] t. But do you really need to do go about predefining all these types?

1 Like
6

this worked! creating a contravariance constrain on the polymorphic type allows do_work to be used with both err and 'e My_err:

  type err = [ `Green | `Blue ]
  type 'e err2 = [ err | `My_err of 'e ]

  type 'e do_work_err = Err1 of err | Err2 of 'e

  type ('a, 'c, 'e) do_work =
    err factory ->
    (string -> ('a, ([< 'e err2 ] as 'c)) result) ->
    ('a, 'e do_work_err) result

module My_thing (Worker : Worker) = struct
  let do_alpha () s : (int, err) result = Ok (String.length s)
  let do_beta () s : (int, string Worker.err2) result = Error (`My_err s)

  let res1 = Worker.do_work factory (do_beta ())
  let res2 = Worker.do_work factory (do_alpha ())
end

code example: Sketch.sh - Interactive ReasonML/OCaml sketchbook

if the type is on the val - it doesn’t even need the 'c constraint:

  val do_work :
    err factory ->
    (string -> ('a, [< 'e err2 ]) result) ->
    ('a, 'e do_work_err) result

(I do need the types, not even sure how to write code without first writing the types)

This created a new problem though, because I don’t know how to constrain a type to be polymorphic, but I’ll create a new thread for it