I’ve written a three-part tutorial on GADTs. The first part shows the very basic. It is intended for anyone who already knows OCaml but hasn’t written a GADT before. The second part is a collection of different techniques you can use when making your own GADT. It is intended as a follow-up of the …

[image] mobileink: Ok, I think I see see where you’re coming from. Problem is, F and S are not values. They’re unary ctors. So the type of v depends on the type of the arg used to parameterize the ctor. Which again is not the same as depending on the value of case. Well F and S are constructo…

Oh man, I completely misread that. Thank you and sorry about the noise!

[image] raphael-proust: have to say, I don’t know what the “Generalized” part of the name means The Wikipedia article on GADTs has a Haskell example that suggests to me that “Specializable” would be more informative than “Generalized”. GADT ctors can produce e.g. Expr bool or Expr int, but …

Incredible tutorial! I’d already read a couple other materials on the subject (RWO, and that hlist article everyone links to on diff-list typing tricks). This was very clarifying as to why and how we might use 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 ha…

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 :camel: example (* 'a and 'b are universally quantified *) (* 'c is existentially quantified *) type ('a,'b) chain = | Link : 'a * 'b -> ('a,'b) chain |…

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

Tutorial on GADTs

Learning

raphael-proust October 1, 2026, 12:18pm 33

I’ve written a supplement to the tutorial:

It compares GADTs and Phantom Types. It includes a (compulsory?) mention of Tyxml in discussion of Phantom Types. If anyone has other good examples to share I might add them.

Topic		Replies	Views
Narrowing variant types alternatives Learning gadt , adt	11	5353	May 21, 2024
ChatGPT explains GADTs Learning gadt	4	1297	March 24, 2023
Telling the type checker that two GADTs are equal Learning gadt	6	339	March 24, 2025
A short GADT puzzle Learning gadt	12	1621	November 24, 2022
Structural equality for GADTs Learning gadt	22	2750	January 13, 2022

Tutorial on GADTs

Related topics