Indeed excellent! I finally found some time last week and read the three tutorials.
I would also recommend Raphael’s tutorials on lwt also on this website. It helped a lot when I started to use lwt.
It’s fun to know the GADT uses object types for parameters, but no object appears at runtime.
I have no ppx experience but I wonder whether/how GADT can be used in ppx.
This was very helpful in helping me understand GADTs better. Thank you!
May be i have misunderstood something however i believe GADTs also allow existentially quantified type variable(s) like 'c in the following 
example
(* 'a and 'b are universally quantified *)
(* 'c is existentially quantified *)
type ('a,'b) chain =
| Link : 'a * 'b -> ('a,'b) chain
| Append : ('a,'c) chain * ('c,'b) chain -> ('a,'b) chain
let rec length : type a b. (a,b) chain -> int =
function
| Link _ -> 1
| Append(p,q) -> length p + length q
I’m not sure this is really adressed in your tutorial. May be because my chain type is too weird.
It appears in the part2’s example Equal case though it’s not called existentially there.
type _ expr =
| Value : 'a v -> 'a expr
| Equal : 'a expr * 'a expr -> bool expr
| IfThenElse : bool expr * 'a expr * 'a expr -> 'a expr
(* more constructors as needed *)
As mentioned by @arbipher there’s something along those lines in part 2. But I also think it’d be worth pointing out explicitly so I’ll add a paragraph somewhere.
Thank you for this tutorial. I never tried to learn it before.
Trying to see what chatgpt can say about it, here is what I got:
decapode314.free.fr/dev/gadt.html
While surfing the internet I found some examples from OCamlPRO blog
Thanks, I added them to the list.
With the help of a chat-bot maybe I will also be able to understand lex/yacc and how xml-light works, the same for the technics used in olibrt.
Maybe I could succeed understand it with only the manual, but chat-bots are explaining it in a way that is easier to understand, and it make possible to understand it more quickly.
I don’t know if this is a good thing or not.
Hello, thank you for these helpful articles on the topic of GADTs. I’m reading the second part and I’m a little confused about the parity example. I’m wondering how one would write a cons function for adding element to a list of such type. My first (naive) attempt at writing such a function fails to compile 
(* types for the parity property *)
type odd = Odd
type even = Even
type ('previous, 'current) parity =
| O : (even, odd) parity
| E : (odd, even) parity
type (_, 'a) l =
| Nil : (even, 'a) l
| Cons : 'a * ('p, 'q) parity * ('p, 'a) l -> ('q, 'a) l
let cons : type parity1 parity2. 'a -> (parity1, 'a) l -> (parity2, 'a) l
= fun x -> function
| Nil -> Cons (x, O, Nil)
| Cons (_, O, _) as l -> Cons (x, E, l)
| Cons (_, E, _) as l -> Cons (x, O, l)
The resulting error message is:
At that point I’m not sure what prevents the compiler’s type system from equating odd to parity2 in the first branch. Is it even possible, within the constraints that the ocaml compiler put on the use of GADTs to write such a function?
My second attempt is to apply a technique described in the first part: have an existential constructor.
(* types for the parity property *)
type odd = Odd
type even = Even
type ('previous, 'current) parity =
| O : (even, odd) parity
| E : (odd, even) parity
type (_, 'a) l =
| Nil : (even, 'a) l
| Cons : 'a * ('p, 'q) parity * ('p, 'a) l -> ('q, 'a) l
type 'a any_parity_list =
| Any : (_, 'a) l -> 'a any_parity_list
let cons : 'a -> 'a any_parity_list -> 'a any_parity_list
= fun x -> function
| Any Nil -> Any (Cons (x, O, Nil))
| Any (Cons (_, O, _) as l) -> Any (Cons (x, E, l))
| Any (Cons (_, E, _) as l) -> Any (Cons (x, O, l))
This does compile 
but it feels quite heavy to use, especially since the section about this parity list type says at some point:
The functions that do not care about parity can simply ignore the
parityparameter. The functions that do care can match on it.
which gave me the impression that it is possible to write more generic functions without having to leverage another wrapping type?
for the function cons it’s not possible to ignore parity (unless you wrap into existentials), the intuitive reason is that in the signature
let cons : type parity1 parity2. 'a -> (parity1, 'a) l -> (parity2, 'a) l
the compiler won’t be able to relate parity1 to parity2 and so doesn’t know what parity to attach to, say, cons 'a' Nil.
you need to teach the compiler this by adding a parity parameter:
let cons
: type p q. (p, q) parity -> 'a -> (p, 'a) l -> (q, 'a) l
= fun pq x xs ->
match pq with
| E -> Cons (x, E, xs)
| O -> Cons (x, O, xs)
the parameter (p, q) parity shows how the two parities (input parity from the parameter, output parity to the return value) relate to each other. Now when you cons with Nil you have to add the constructor O as an explicit parameter and the compiler can infer all it needs.
let xs = cons E 'a' (cons O 'b' (cons E 'c' (cons O '\n' Nil)))
there might be a cleverer way of doing this maybe? if someone has one please comment.
and re:
The functions that do not care about parity can simply ignore the parity parameter.
consider iter which treats all elements the same and so doesn’t need to match on the parity constructor in the Cons:
let rec iter
: type p. ('a -> unit) -> (p, 'a) l -> unit
= fun f xs ->
match xs with
| Nil -> ()
| Cons (x, _, xs) -> f x; iter f xs
One option is to keep the full parity type available in the parity list:
type even = < even:yes; odd:no >
type odd = < even:no; yes:odd >
type (_,_) plist =
| []: (even,'elt) plist
| (::):
'elt * (<even: 'e; odd: 'o>, 'elt) plist ->
(<even: 'o; odd: 'e>, 'elt) plist
then cons is just
let cons x l = x :: l
and one can check that adding twice an element keep the same parity:
let cons_twice: type e o x.
x -> (<even:e;odd:o> as 'p, x) plist -> ('p, x) plist =
fun x l -> x :: x :: l
However, once the parity type has been projected to only the odd or even component, one needs to reintroduce the equation linking the odd and even types to switch the parity.
Note however that this not necessary if the parity stays the same. Reusing the definition
type odd = Odd
type even = Even
type ('previous, 'current) parity =
| O : (even, odd) parity
| E : (odd, even) parity
type (_, 'a) l =
| Nil : (even, 'a) l
| Cons : 'a * ('p, 'q) parity * ('p, 'a) l -> ('q, 'a) l
then adding twice an element do not require a parity argument:
let cons_twice: type x p. x -> (p,x) l -> (p,x) l =
fun x l ->
match l with
| Nil -> Cons(x,E, Cons(x,O, Nil))
| Cons(_,O,_) as r -> Cons(x,O, Cons(x, E, r))
| Cons(_,E,_) as r -> Cons(x,E, Cons(x, O, r))
Similarly, adding thrice an element requires to reintroduce the parity equation once
let switch: type e o. (e,o) parity -> (o,e) parity = function
| O -> E
| E -> O
let cons_thrice: type x p q. (p,q) parity -> x -> (p,x) l -> (q,x) l =
fun p x l ->
let p' = switch p in
Cons(x,p, Cons(x,p',Cons(x,p,l)))