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 first part or for programmers who have written GADTs before but feel like they still have things to learn. The third part is a gallery of GADTs found in the public OCaml software ecosystem. It’s intended for anyone who wants to see practical-use examples.
I’m still struggling with the concept. Syntactically as I understand things what distinguishes a GADT from a variant is just ->- is that correct?
Nice post! One thought on Part 2, which alludes to a correspondence between hlists and tuples. Maybe it would be helpful to illustrate how far the similarity goes, as in the example below: for both stringify_hlist and stringify_tuple, the compiler is able to infer the correct argument type, and unlike with a regular list, it knows that both of these pattern-matches are exhaustive.