Ideas: allow users to use GADT for typing externals

[bobzhang]

We already allows users to use polymorphic varaiant for typing FFI, which can model some
dependent typed semantics. A more powerufl approach is to use GADT(extensible variants)
for this too. The technical challenging part is that we need see the type definition to generate readable code, below is my proposal, which I think is doable

external read : 'a t -> 'a = "" 
 [@@bs.val]
 [@@bs.constraint type 'a t = 
  | Structure : structure t 
  | Signature : signature t 
 ]

The syntax is a bit heavy,
question: how much would it be useful to type existing JS libraries?

CC @freebroccolo

[chenglou]

facebook/flow#443 (comment)

The flow typed repo is barer than the typescript counterpart. If we can somehow kill two birds with one stone by using and/or generating flow types that'd be a big win for both the js and the ocaml folks. Imagine js folks converting to ocaml and BS because they were already using flow-typed!

[bobzhang]

I reopened #637 about discussing generating .d.ts files for flow, this issue is about GADT : )

[jordwalke]

I'd like to see a complete (small) example of the difference between poly variants and GADTs (you mentioned extensible but I don't see any +=).

[ghost]

@bobzhang This looks very interesting! I would really love to have GADT support.

FWIW, there some experimental GADT support in gen_js_api but have not used that too extensively.

However, I have used a kind of hack for GADTs in my bucklescript Electron library. I use it for defining event types here. Then see it used here. The ns type there is used as a kind of "namespace" for the events.

What GADTs bring to the table that poly variants don't is the able to define event types that support subtyping. So in my example, App can respond to both default events from the node library as well as the Electron specific events.

The way it actually gets implemented is by using some metadata that I store alongside the file here. Then I wrote a babel plugin that does the post-processing. It's not a perfect solution but it does work very well.

[bobzhang]

@freebroccolo thanks for your feedback. note that gen_js_api will generate nontrivial stubs code and you might loose efficiency there. Unfortunately, GADT here will still only work for external, would it be useful then? the good thing is that we can unify the design of polymorphic variant.

[ghost]

@bobzhang If I'm understanding correctly, I think it could still be useful even if restricted to external since this could give you a way to do a crude simulation of intersection types for functions that need that to accurately type.

I'm not sure if intersection-style typing like that is enough on its own to justify supporting GADTs yet. But maybe the unification you mention with poly variants would be worth it.

By the way, I know that hack I described above (with babel for post-processing) is ugly but it is so easy to do that I wonder if it could be made more acceptable if there were some kind of proper BS support for it.

The basic idea is to use extensible variants (which could be GADTs) and provide some sort of metadata (maybe using t += | Foo [@bs "foo"]) on the constructors that describes how they should be translated to JS values. Then you'd collect these tags and do a post-processing pass in BS. Or maybe you could do it without post-processing somehow.

In my example above I am only translating them to JS string but there is no particular reason you couldn't also use boolean or number or something else.

[bobzhang]

@freebroccolo I have another idea to make use of GADT which seems more solid and simple:
suppose we have a js function

function add (x,y){
  return x + y
}

It works with both float and string, so we can type it as:

type  _ kind = 
  | Float : float kind 
  | String : string kind

external add : ('a kind [@bs.ignore]) -> 'a -> 'a -> 'a = "" [@@bs.val]

Here bs.ignore is very simple and the implementation does not need see the definition of kind which is more composable and solid.

so user can write code

let u : float = add Float 3.0 2.0
let v : string = add String "x" "y"

var u = add (3.0,2.0)
var v = add ("x","y") 

in your case, you can design a wrapper like this

external add : ('a kind [@bs.ignore]) -> string -> 'a -> 'a -> 'a = "" [@@bs.val]
let add k a b =add k (string_of_kind k) a b 

This is different from gen_js_api since it will still be as efficient as you wish?

[ghost]

@bobzhang this seems quite nice. It does look like it would probably work for most of the cases I had in mind. I guess this would just work without any issues with extensible variant GADTs too?

[bobzhang]

yes, simple and easy to maintain