Is there someplace a bestiary of GADT examples ? I’d like to find such a thing in order to more-fully understand the universe of possibilities for using GADTs in programming. I’ve never used 'em, and while, sure, reading about the theory is great, and reading a few example is cool, it would be complementary to have a bottom-up understanding (lots of examples) as well as a top-down one.
We do seem to have a home-grown ‘GADT’-iary: Open source projects using GADTs
A couple of new and interesting ones since that thread:
- [ANN] Petrol 1.0.0 - A high-level typed SQL API for OCaml designed to go fast!
- ocaml_sql_query/sql.ml at 0516ea6c7d80a6fcf61c4d9ba551b9f0b780d9ff · yawaramin/ocaml_sql_query · GitHub by yours truly to model ‘a query can return either nothing or some resultset’
Not exactly examples of GADTs “in the wild”, but I’ve found @yallop 's slides (from the Advanced Functional Programming course at Cambridge) to be interesting for seeing “GADT design patterns”: https://www.cl.cam.ac.uk/teaching/1617/L28/lecture-8-slides.pdf , https://www.cl.cam.ac.uk/teaching/1617/L28/lecture-9a-slides.pdf. (I hope it is OK to link those here!)
I haven’t got round to properly publicising it, but I actually wrote blog post about the internal development process of Petrol, and how I gradually moved from Caqti, to macros, to GADTs which may be useful:
We use a lot of GADTs in Coq
For instance coq/tac2ffi.ml at 14946eb0cbce09c1a63d36aac21ccb1161fbd869 · coq/coq · GitHub used to have arbitrary-arity functions
type ('arg,'result,'f) arity = | One : ('arg, 'result, 'arg -> 'result) arity | More : ('arg, 'result, 'f) arity -> ('arg, 'result, 'arg -> 'f) arity type ('arg, 'result) nary = Nary : ('arg, 'result, 'f) arity * 'f -> ('arg, 'result) nary type value = | Closure of (value, value) nary | SomeInt of int let to_nary = function | Closure f -> f | SomeInt _ -> failwith "can't apply someint" let rec apply : type f. (value,value,f) arity -> f -> value list -> value = fun arity f args -> match args, arity with | , _ -> Closure (Nary (arity, f)) | [arg], One -> f arg | arg :: args, More arity -> apply arity (f arg) args | arg :: args, One -> let f = f arg in let Nary (arity, f) = to_nary f in apply arity f args let apply_val f args = let Nary (arity, f) = to_nary f in apply arity f args let addf x y = match x, y with | SomeInt x, SomeInt y -> SomeInt (x + y) | _ -> failwith "addf got non-ints" let addval = Closure (Nary (More One, addf)) let addval' = Closure (Nary (One, fun x -> Closure (Nary (One, fun y -> addf x y)))) let () = assert (apply_val addval [SomeInt 1; SomeInt 2] = apply_val addval' [SomeInt 1; SomeInt 2]) let () = assert (apply_val addval [SomeInt 1; SomeInt 2] = SomeInt 3)
Or coq/evd.ml at 14946eb0cbce09c1a63d36aac21ccb1161fbd869 · coq/coq · GitHub
a record where some fields are nontrivial if and only if some other field is nontrivial
or around coq/grammar.ml at 14946eb0cbce09c1a63d36aac21ccb1161fbd869 · coq/coq · GitHub which replaced some Obj.magic in the camlp5 engine this file is derived from.
I guess you can find more by looking at https://github.com/search?q=repo%3Acoq%2Fcoq+GADT&type=commits
'a Lwt.t promise states and several other types in Lwt are internally GADTs. See lwt/lwt.ml at cc05e2bda6c34126a3fd8d150ee7cddb3b8a440b · ocsigen/lwt · GitHub. This is mainly to use the existential types capability of GADTs.
You can also check a protocol implementation with GADT here (which proves that a client should never send something to another client): bob/state.ml at main · dinosaure/bob · GitHub. A detailled article is available here: Dinosaure's website - GADTs and state machine
Also, I re-implemented a
printf function with a promotion mechanism of certains values (à la C) here: conan/fmt.ml at main · mirage/conan · GitHub. You can also check the implementation of the decision tree which helps us to regognize MIME type, it’s a GADT too: conan/tree.ml at main · mirage/conan · GitHub.
Finally, you can check this typed lambda calculus: mirage-lambda/typedtree.ml at a89b265b552f8b63ff725fc942f41a276fabb4f5 · mirage/mirage-lambda · GitHub and the transformation from a simple lambda-calculus with a typed one (and where we prove that variables are bounds via the De-Bruijn indice).
EDIT: Ah and probably the most complicated GADT I ever see which has a real application, a zipper on an AST where the path is a GADT.
Menhir generates code with gadts using the method described in this paper
In that case, the specific technique used is ADTs without allocation, of which a more simple example is the following :
type 'a number = | Float : float number | Int : int number let show_number : type n. n number -> n -> string = fun witness n -> match witness with | Float -> string_of_float n | Int -> string_of_int n
Hi @Chet_Murthy !
Arthur Wendling (Tarides) has an implementation of Kaplan/Tarjan 99 (Purely Functional, Real-Time Deques with Catenation), which makes a non-trivial use of OCaml’s GADT. See https://github.com/art-w/deque
I have used GADTs in rotor to implement a rich identifier type for different syntactic elements of the OCaml language, as well as some custom zipper types over the OCaml compiler typed AST.