[Peaker]

Why do they reduce the amount of code?

They add the ability for constructors to carry constraints, which aids expressivity in some cases.

But the majority of GADT uses purely add safety. Can use ordinary ADT without a type-variable that is correlated with the data constructor, and crash at runtime if the constructors don't match.

[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

[tom_mellior]

> Why do they reduce the amount of code? [...] crash at runtime if the constructors don't match.

You answered yourself: If you cannot have these runtime type mismatches, you don't need to write the corresponding bookkeeping and checking code.

[Peaker]

You don't have to write it - you just have to avoid -Wall :-)