Somehow typed tagless interpreters (embeddings of a typed language) and length-parameterized lists with the append function are the most popular examples of GADTs. Neither of them seem to be particularly good or compelling examples. One can write typed interpreters in the final-tagless style, with no GADTs. Writing append function whose type says the length of the resulting list is the sum of the lengths of the argument lists is cute. However, this example does not go too far, as one discovers when trying to write List.filter for length-parameterized lists.
The ML2010 talk on GADT emulation specifically used a different illustrating example: a sort of generic programming, or implementing N-morphic functions: http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf Polymorphic functions must operate uniformly on their arguments, which means they can't use a specific efficient operation if the argument happens to be of a convenient type (like int of float array). N-morphic functions can take such an advantage. The running example of the talk combined value and the shape information in the same data type: type 'a sif = Int of (int,'a) eq * int | Flo of (float,'a) eq * float val add_sif : 'a sif -> 'a sif -> 'a sif Shape may well be separated from the value: type 'a shape = Int of (int,'a) eq | Flo of (float,'a) eq val add_sif : 'a shape -> 'a -> 'a -> 'a and so we pass values to add_sif without `boxing' and wrapping. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
