GADTs are http://en.wikipedia.org/wiki/Generalized_algebraic_data_type

marktangotango · on March 31, 2015

Upvoting, so obnoxious of the author of the post to not define them.

adultSwim · on March 31, 2015

I can't tell if you are serious or not. OP goes through them by example.

Original type:

  type 'a t = | Array of 'a array
              | Bytes of bytes

GADT'd (same functionality as before):

  type 'a t = | Array : 'a array -> 'a t
              | Bytes : bytes -> 'a t

Now using power of GADT to add constraint:

  type 'a t = | Array : 'a array -> 'a t
              | Bytes : bytes -> char t

Just jumping into it seems like a fine choice to make. Allows for a (narrow) introduction to GADTs without getting bogged down in their full complexity/limitations. Shows that it's useful before/without a theoretical discussion.

Still, I wouldn't have minded a little discussion introducing GADTs.

AceJohnny2 · on March 31, 2015

In the original version of the article (when I wrote my comment), the author hadn't defined them.