A bestiary of GADT examples?

Ecosystem
1

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.

4 Likes
2

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:

8 Likes
3

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!)

3 Likes
4

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:

https://gopiandcode.uk/logs/log-ways-of-sql-in-ocaml.html

4 Likes
5

We use a lot of GADTs in Coq
For instance coq/tac2ffi.ml at 14946eb0cbce09c1a63d36aac21ccb1161fbd869 · coq/coq · GitHub used to have arbitrary-arity functions
Slightly simplified:

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

6

'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.

2 Likes
7

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.

2 Likes
8

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
2 Likes
9

In owi, to allow the user to define host functions usable from Wasm, we also use GADTs.

1 Like
10

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

4 Likes
11

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.

1 Like
12

I’ve revisited Typing Tricks: Diff lists various times for implementing heterogeneous lists and maps.

edit: found some related libs in this comment.