CODEWITHSUNDEEP
polymorphismocamlvariant
Sventimir
Sventimir

Reputation: 2056

How to enforce constrained polymorphism on a function in OCaml

I'm working with yojson library and I'm trying to write a function which given some json, retruns a list, if it's a list or an error otherwise. Crucially, I want the function to work on any Yojson's subtype (Yojson.Basic, Yojson.Safe, Yojson.Raw etc). I have written the following type declaration:

val expect_list : ([< Yojson.t ] as 'j) -> ('j list, exn) result

It seems straightforward to implement:

let expect_list = function
| `List js -> Ok js
| #Yojson.t -> Error (Failure "Not a list!")

Now OCaml agrees that the argument has type [< Yojson.t ], but insists on the result having the monomorphic type Yojson.t. This is bad, because when I input Yojson.Safe.t I want to be able to constrain result to the same type, which I cannot figure out how to do. I can think of no reason why it shouldn't be possible…

Upvotes: 1

Views: 83

Answers (1)

octachron
octachron

Reputation: 18902

The issue is that the type scheme [< Yojson.t] does not match any of the type Yojson.Safe.t nor Yojson.Basis.t type because the recursion in the Yojson.t type is closed.

One option is thus to avoid over-constraining the expect_list function:

let expect_list = function
| `List js -> Ok js
| x -> Error (Failure "Not a list!")

then expect_list will have the type

val expect_list : [> `List of 'a ] -> ('a, exn) result

and behaves as expected when applied to a subtype of Yojson:

let safe_expect_list (x: Yojson.Safe.t) = expect_list x

val safe_expect_list : Yojson.Safe.t -> (Yojson.Safe.t list, exn) result

Another option is to define an open-recursion variant of the Yojson.t type. This can be done by adding a type parameter 'mu to the definition of the type and replacing all recursive occurrence of Yojson.t in the definition by this parameter 'mu:

type 'mu rt =[ 
    `Assoc of (string * 'mu) list
  | `Bool of bool
  | `Float of float
  | `Floatlit of string
  | `Int of int
  | `Intlit of string
  | `List of 'mu list
  | `Null
  | `String of string
  | `Stringlit of string
  | `Tuple of 'mu list
  | `Variant of string * 'mu option
]

A first observation is that the scheme [< _ rt ] matches all the types Yojson.t, Yojson.Safe.t and Yojson.Base.t:

let test (x: Yojson.Safe.t) (y: Yojson.t) : [< _ rt ] * [< _ rt ] = x, y

because it doesn't add any constraints on the argument of the variant that corresponds to the "recursive hole" 'mu.

We can thus use that type as a finer constraint in the expect_list function

let expect_list = function
| `List js -> Ok js
| #rt -> Error (Failure "Not a list!")

val expect_list : [< 'a rt ] -> ('a list, exn) result

The difference with the #Yojson.t pattern is that the #rt pattern does not impose any constraint on the type of the elements of the list under the `List constructor contrarily to the #Yojson.t pattern which requires the type of the elements of the list to be exactly Yojson.t.

This version also has the expected behavior when applied to a variant of the yojson type:

let safe_expect_list (x: Yojson.Safe.t) = expect_list x;;

val safe_expect_list : Yojson.Safe.t -> (Yojson.Safe.t list, exn) result

One way to understand why this open-recursion type is useful in general is that the standard Yojson.t type can be defined as

type t = 'mu rt as 'mu

In other words, the open-recursion type constructor rt defines one layer of the recursive structure of the Yojson.t and the standard type can be obtained by stating that all layers are the same.

Upvotes: 3

Related Questions