[dpwm]

I thought GADTs would be useless to me when I first heard the explanation of GADTs as imposing additional constraints on ADTs. Whilst technically true, it feels like it's missing the point.

The real power of GADTs comes from the fact that you can use the type at compile time. This means that in OCaml I can do something like:

  type 'a t =
  | Int : int t
  | Float : float t

  let print : type a. a t -> (a -> string) =
    function
    | Int -> string_of_int
    | Float -> string_of_float

I can the do (print Float) and receive string_of_float. I can do (print Int) and receive string_of_int. Both have drastically different types, but due to the constraints that the GADT imposes it is fully type safe and the type is known at compile time.

Although this is a slightly contrived and useless example, there are scenarios where this can prove immensely useful that are not that far away and really aren't so useful when done with ADTs. Think serializing -- you would have to convert to the ADT first which isn't so useful. If you're interested in something useful, take a look at [0] (shameless plug), a very early alpha version of a similar idea allowing conversion from and to JSON.

EDIT: this is not inlined as I recall. False memory. The reason it isn't is probably because you can use existential types in which case the type would not be known at compile time.

[0] https://github.com/dpwm/typespec