[Caml-list] Re: Wanted: GADT examples: string length, counting module x

[Goswin von Brederlow <goswin-v-b@web.de>]

oleg@okmij.org writes:

> 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

An interesting talk to read. But unless I'm mistaken that isn't using
ocamls new GADT types but implements it own.

MfG
        Goswin