CODEWITHSUNDEEP
ocamltype-inference
Vladimir Keleshev
Vladimir Keleshev

Reputation: 14295

OCaml: type inference with polymorphic variants

Function f argument type is [< 'A | 'B] that's what I want.

# let rec f = function
  | `A -> 0
  | `B -> let _ = f in 1
;;
val f : [< `A | `B ] -> int = <fun>

However, if I call it recursively with 'A it infers an undesired for me type [< 'A | 'B > 'A] which requires at least 'A:

# let rec f = function
  | `A -> 0
  | `B -> let _ = f `A in 1
;;
val f : [< `A | `B > `A ] -> int = <fun>

I still need to recursively call f 'A, but how do I keep the type [< 'A | 'B]?

Upvotes: 1

Views: 322

Answers (1)

ivg
ivg

Reputation: 35280

This is yet another instantiation of the let-polymorphism constraints, that hinders the usage of polymorphic recursive function. Since, OCaml 3.12 we have an explicit way to declare that your function is polymorphic.

Your case is a little bit more complex, since you have implicit type variable, that occurs inside the row-polymorphic type. Maybe there is a better way, but my approach is to make this type variable explicit, with the following type definition

type 'a t = 'a constraint 'a = [< `A | `B]

With such handy type, it is easy to write a proper annotation for a function:

let rec f : 'a . 'a t -> int = function
| `A -> 0
| `B -> let _ = f `A  in 1

Just in case, if you don't want to expose this 'a t, that's ok, since you're not required, 'a t is equal to [< 'A | 'B] it just makes 'a type variable explicit:

module M : sig
  val f : [< `A | `B] -> int
  end = struct
let rec f : 'a . 'a t -> int = function
  | `A -> 0
  | `B -> let _ = f `A  in 1
end;;

Without introducing 'a t type, you can make it with a little bit uglier (but this is of course a matter of taste) notation:

let rec f : 'a . ([< `A | `B] as 'a) -> int = function
  | `A -> 0
  | `B -> let _ = f `A  in 1

Of course, this will not scale, for non trivial types.

Upvotes: 2

Related Questions