Troubles using GADTs (Type constructor tries to escape its scope!)

Learning
1

Hello,

I have some troubles using GADTs for a future project targeting Node with BuckleScript.
This project will use some Node libraries, and I would like to make the bindings flexible and as robust and type safe as possible.

In order to achieve these objectives, I thought about making (1) a “DSL” that would ease the build of a rather complex record, featuring some dynamical heterogeneous lists (hence the use of GADT), and deeply nested records, and (2) a “parser” for this object that would actually call the JavaScript functions (using extern and all).

But I’m currently facing a “The type constructor * would escape its scope” error.

Here is a small piece of code showing what I’m currently doing:

(* (1) *)
(* BuckleScript does not support OCaml's record literal in GADTs declaration, hence the *_record boilerplate *)
type ('a, 'b) y_record = { f: 'a -> 'b }

(* 'b seems to "escape" in the transform function below *)
type _ y = Y : ('a, 'b) y_record -> 'a y

type 'a x_record = { list: 'a y list }

type _ x = X : 'a x_record -> 'a x

(* Arbitrary use `int` here *)
let x: int x = X {
  list= [
    Y {f= (fun _ -> 42)};
    Y {f= (fun _ -> "foo")};
  ]
}

type z

external jsFunction: 'a -> z = ""

(* (2) *)
(* Raises "The type constructor b#11 would escape its scope" *)
let transform: type a. a x -> z = (fun (X x) ->
  jsFunction (x.list |> List.map (fun (Y {f}) -> f))
)

After some readings, like this super nice article, and the chapter 8 of the Ocaml manual, even if I somewhat understand what I’m doing wrong, I can’t really figure a way to (1) get rid off the error while keeping the same architecture or (2) find an other way to achieve the same objectives…

Any help would be greatly appreciated!

Edit: Made example closer from the actual code

2

One problem with your code is this line:

With a bit of simplification, this code is equivalent to

type _ f = F :  ('a -> 'b) -> 'a f

which means that you are forgetting the type returned by the function f when you construct F f.
In other words, if you have a value of type 'a f, you have a function that takes a value of type 'a as an argument and returns a black box of which you don’t know anything about the contents.

Consequently, the only thing that you can do with the result of f is to ignore it (except for polymorphic comparison).

Which leads to a much simpler implementation of your type _ y and its Y constructor:

type 'a y = 'a -> unit
let y f x = ignore(f x)

Beyond this point, I am not sure of what you are trying to achieve.

3

Thank you for your reply.

This works nicely!
I actually tried to use some tricks close to this one to make the code compile but wondered if it was the “proper” way to solve this issue in OCaml (I am very new to the language, having only used Haskell as a FP language so far).

The provided code is an over simplification of the actual code, so let me provide more informations.
I would like to mimic the OCaml server GraphQL API (an example can be found here), for the GraphQL-js library (Node is a must for the project).