I’m trying to write a module that type safely generates json schema. As a reference I use https://github.com/sikanhe/reason-graphql, GADT has already blown my mind, but now I came across a construction I don’t understand at all. It looks like something between a variant and a list match, could somebody explain what exactly it is.
and arglist(_, _) =
| []: arglist('a, 'a)
| ::(arg('a), arglist('b, 'c)): arglist('b, 'a => 'c);
Also I’m curios about and, I haven’t found anything about it in the doc.
There are a few things going on here. [] and :: are constructors for the built-in list variant in OCaml. The best way to think of these is that they work exactly like regular variant constructors, except the compiler lets them have those special names.
In Reason syntax, type list('a) = | [] | ::('a, list('a)) is basically equivalent to type list('a) = | Nil | Cons('a, list('a)). In Reason/OCaml syntax, you can use those special constructor names in your own type, which will let you use list syntax to construct your custom type instead of the built-in list type.
(In Reason/OCaml, true, false, and () are also special variant names, and the compiler will also let you use those as names in your own variant too.)
What the GADT part does is allow you to create a heterogeneous list. You could use it to construct a list like this (in Reason syntax): [1, "a", 1.5].
ReScript does not allow you to redefine those constructors. But you can achieve the same thing using normal variant constructor names:
type rec arglist<_, _> =
| Nil: arglist<'a, 'a>
| Cons('a, arglist<'b, 'c>): arglist<'b, 'a => 'c>
let x = Cons(1, Cons("a", Cons(1.5, Nil)))
You don’t get to use the built-in list syntax, but it should otherwise function identically.
I would advise to keep this file in OCaml since there’s no reason Rescript would drop OCaml support any time soon and this would allow to keep using a nice API in rescript like:
list{1, "a", 1.5}
Regarding and, it allows to define mutually recursive types, for example:
type rec foo = {bar: bar}
and bar = Int(int) | Foo(foo)
GADTs are arguably the most advanced feature in ReScript (and OCaml). You will likely never need to use them if you’re developing a typical app, only something very complex (like the GraphQL PPX).
Other people can probably explain them better than me. But the basic idea is that the : assigns a new type to the variant constructor.
In this example, Nil: arglist<'a, 'a> doesn’t actually do anything special, since arglist<'a, 'a> is already the normal type for the constructor. Cons('a, arglist<'b, 'c>): arglist<'b, 'a => 'c> is what makes the heterogeneous list possible.
The value Cons(1, Cons("a", Cons(1.5, Nil))) has a type of arglist<int, int => string => float => int>. Notice that the int => string => float is a function type, but it doesn’t actually exist as a value, only as a type. It’s what the type-checker uses to track the type of each value of the list.
Again, this is a very advanced feature. If it doesn’t make sense, don’t worry. It takes most people a while to learn it. For most practical applications, you will never need to use it anyway.
List type has two type variables, one for the content of the list and one for the unification variable at the end. In the following, I will note 'ty the type of the content and 'v is the unification variable.
An empty list is a list where there is no content: 'ty = 'v
A cons is a list where we added one element to the type.
type ('ty,'v) t =
| Nil : ('v, 'v) t
| Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t
As johnj said GADT is a very advanced feature and mostly needed for library creators. Talking about heterogeneous list I have been breaking my brain for three days and then decided that t I don’t actually need it
