Tutorial on GADTs

Learning
, ,
21

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
22

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

1 Like
23

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 =
   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.

1 Like
24

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
25

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.

26

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