Open source projects using GADTs

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” :wink:)?

Thank you
Tomasz

4 Likes

A couple off the top of my head:

Cheers,
Nicolas

1 Like

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

3 Likes

A few more examples randomly sampled from a very very long list:

6 Likes

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

1 Like

Not to miss out on the self-promotion train, here’s a shameless plug for an example of a free-software library using GADTs:

1 Like

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.

4 Likes

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.

5 Likes

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

1 Like