Hi all
I’m trying to wrap my head around GADTs. I’ve read chapters on them in Ocaml Manual and Real World Ocaml, also some tutorials on GADTs in Haskell, and I think I’m starting to get them. Now I’d like to study some actual usage in real projects.
Can someone recommend an open source project that makes a good use of GADTs (for any value of “good” 
)?
Thank you
Tomasz
A couple off the top of my head:
ocaml-asn1-combinators (typed ASN.1 embedding) ocaml-asn1-combinators/asn_core.ml at f10fc1d869be293a16a31b272fc71794849007a2 · mirleft/ocaml-asn1-combinators · GitHub
ctypes (typed embedding of the C type algebra) ocaml-ctypes/ctypes_static.ml at d5191b45ee69949167cabc0646b106bb0d61ba89 · ocamllabs/ocaml-ctypes · GitHub
ocaml-asp (typed embedding of context-free expressions) ocaml-asp/asp_unstaged.ml at 29a13a54dce754cd573a2057c3abdc358b6e35c1 · yallop/ocaml-asp · GitHub
Cheers,
Nicolas
If you want something a bit fancy and almost dependent types on OCaml.
I’m using a GADT in my library: ocaml-decimal/decimal.ml at 08c57183c8673b5058bd6010570e69f0201c03c7 · yawaramin/ocaml-decimal · GitHub
It’s a port of Python’s decimal module. The use case is to handle different exceptional conditions in decimal operations (overflow, underflow, etc.) in different ways. Some conditions can result in a value, others can result in no meaningful value. Using a GADT to model this behaviour.
You can see the handling being done here: ocaml-decimal/decimal.ml at 08c57183c8673b5058bd6010570e69f0201c03c7 · yawaramin/ocaml-decimal · GitHub
A few more examples randomly sampled from a very very long list:
metrics demonstrates how to restrict types to a known subset
docteur how to expose more or less capabilities
dune how to configure the output of a function (see also usage below)bimage expression language for defining filtersdeque for its encoding of the invariants of a datastructure (and its big brother)https://hg.sr.ht/~mmatalka/sqlite_io/browse/src/sqlite_io?rev=tip
Here is a little sqlite wrapper I made where you can express variables in a sql statement using GADTs
Not to miss out on the self-promotion train, here’s a shameless plug for an example of a free-software library using GADTs:
Thank you all, this really helps!
I believe my old blog post is relevant: Typing Tricks: Diff lists | Drup’s thingies ! I also have funny slides on the topic: GADTs gone mild.
IIRC, the graphql and routes libraries use that technique, as well as Format (from the stdlib) and various other libraries.
A distinct approach to the same problem can be found in my tyre library.
Also in the stdlib, Bigarray showcases a simple (and thus easy to grasp) usage.
For a more maximalist usage of GADT, slap and tensority both use types to check dimensions in matrix computations.
You might find this blog post interesting/useful: Jane Street Tech Blog - Why GADTs matter for performance
I found this example also helped a lot to understand the utility of GADTs.
This explanations of GADTs is amazing! It should be part of the official docs. It’s first one I have read that makes sense to me.
Another interesting use is the runtime selection of the implementation used by optint. @dinosaure has written an interesting document about it: https://blog.osau.re/articles/optint.html