An concrete simple example to demonstrate GADT in OCaml?

Question

I've searched around for the concept of GADT in OCaml, why we need it and when to use it, etc.

I understand GADT is not only in OCaml but a more general term.

I've found

What are GADTs?

http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85

http://www.reddit.com/r/ocaml/comments/1jmjwf/explain_me_gadts_like_im_5_or_like_im_an/

etc, but some of them are in Haskell, and others do not have a good comparison example between no GADT and GADT.

So what I would like is a simple yet good concrete example where I can see if without GADT, things are bad.

Can I have that please?

Answer 1

GADTs are useful for two reasons.

The first one (and the most common one) is about dynamic typing: you can add some dynamic typing without losing static checking of it. It is not simple though, but you can be sure through it that your type conditions will be met. The simplest example of that is given in the ocaml manual. This was used for instance in the standard library to rewrite printf in a type safe manner (before that, it was a pretty horrible collection of Obj.magic)

The second reason you may want to use GADTs is when you have some complex invariant you want to maintain on your type structure. This is pretty hard to express though, and you often have to put a lot of effort to do that. Well, I don't have any example handy, but I once saw a friend write down an implementation of AVL-trees were it was proven by the typing system that balancing was right, which is pretty cool.

For more one the GADT feature, and its good use cases, You can read the pretty good blog post by Mads Hartmann.

Answer 2

I'm also in a search of good application of GADT, as most of the time, when I use them sooner or later I discover, that the same can be done without them, and usually in a much more cleaner way. So, this is not a complete survey, just a bit of my own experience.

1. Universal values, aka existentials. They allow you to create heterogenous containers and typesafe serialization. See, for examples Core's Univ and Univ_map modules.

2. Type-safe evaluators for syntax trees. Here GADTs are useful to remove some runtime checks.

3. Pure and type-safe Printf implementation, that is already a part of OCaml, was also rewritten using GADT

Here is a real life example of how GADT can be used. In the example, I use GADT to specify table relations, e.g., one_to_one, one_to_many, etc. Depending on the used relation the function type is inferred accordingly. For example, one_to_maybe_one relation, returns a function 'a -> 'b option, one_to_many creates a function with 'a -> 'b list. The same can be achieved by just creating several different functions, like link_one_to_one, link_one_to_many, etc instead of one function link ~one_to:relation. So, one can consider this approach as arguable.