Tutorial on GADTs

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.

1 Like

This was very helpful in helping me understand GADTs better. Thank you!

1 Like

May be i have misunderstood something however i believe GADTs also allow existentially quantified type variable(s) like 'c in the following :camel: 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 =
   | 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 *)
1 Like

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: