Polymorphic variant being generalised

Community
1

Hi,
I am trying to make the following compile.

$ cat hello.mli 
type error = [ `Msg of string ]
val to_string : int -> (string, [> `Msg of string ]) result
val f : int -> (string -> ('a, [> error ]) result) -> ('a -> 'b) -> ('b, [> error]) result

$ cat hello.ml
type error = [`Msg of string]

let to_string i = 
  if i < 10 then Result.ok (string_of_int i) else Result.error (`Msg "invalid number")

let f : int -> (string -> ('a, [> error]) result) -> ('a -> 'b) -> ('b, [> error]) result = 
  fun i f1 f2 -> Result.bind (to_string i) (fun s -> f1 s) |> function 
    | Ok a -> Ok (f2 a) 
    | Error e -> Error e

However, I keep getting the following compilation error,

Values do not match:
       val f :  int -> (string -> ('a, [> error ] as 'c) result) -> ('a -> 'b) -> ('b, 'c) result
       is not included in
       val f : int -> (string -> ('a, [> error ]) result) -> ('a -> 'b) -> ('b, 'c) result

It seems the ocaml compiler generalizes (?) [> error] to 'c which makes it not compile to the given hello.mli file. Is there a way to fix this without changing the signature?

Also does 'c still conform to [> error] after it being generalized to 'e?

2

The inferred type of f indicates that if the f1 argument returns more than the tags in error, then so will f itself. The 'c type variable is expressing that relationship. The type without it is not correct. You either need to constrain f1 by removing < or constrain f with 'c.

2 Likes
3

@jjb’s reply is excellent, but let’s give a couple extra details. Your example boils down to something like:

apply : (unit -> [> error]) -> [> error])

When you write [> error], you have to understand this as a universal quantification: an instance of [> error] is any type which contains at least error (for example [ error ] or [ error | `Foo | `Bar ]. As with polymorphic type variables in signature, the caller gets to choose the instance they want at function application time. The two separate occurrences of [> error] correspond to two distinct/independent quantifications.

So the caller could instantiate this to, for example:

apply : (unit -> [ error | `Foo ]) -> [ error | `Bar ]

and clearly this is incorrect (with the “obvious” implementation fun f -> f ()): if the function parameter returns `Foo, then the return type must allow `Foo. In other words, the two occurrences of [> error] must be instantiated with the same type. This corresponds to the following, less general (and more correct) signature:

val apply : (unit -> ([> error ] as 'a)) -> ([> error ] as 'a)

which can also be written

val apply : (unit -> ([> error ] as 'a)) -> 'a
4 Likes
4

Thanks. This clarifies it.

I tried some examples in utop and it seems to work, i.e. 'a in val apply : (unit -> ([> error ] as 'a)) -> 'a restricts instances of 'a to [>error].

For posterity, here is the sample usage of the function apply.

utop # apply (fun () -> `Foo);;
- : [> error ] = `Foo

utop # apply (fun () -> `Bar);;
- : [> `Bar | `Foo ] = `Bar

utop # apply (fun () -> "hello");;
Line 1, characters 17-24:
Error: This expression has type string but an expression was expected of type
         [> error ]

utop # apply (fun () -> 222);;
Line 1, characters 17-20:
Error: This expression has type int but an expression was expected of type
         [> error ]

utop # apply (fun () -> `AAA);;
- : [> `AAA | `Foo ] = `AAA