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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

In this example, you use GADTs to safely provide runtime type
information on untagged data. This can also be seen as a specific case
of the "runtime type information" promoted by Alain Frisch [1] or
equivalently as a dual (in the sum-of-data vs. product-of-functions
sense) of type-classes, where you have a predicate over a subset of
the types ("sif" being read as an "is_a_number" type constraint) whose
instances are closed / fixed at class definition time, to which
operations can be added modularly: `add` now, `mult` later. This can
then be related to Pottier and Gauthier's "concretization" of
type-classes mentioned in my previous message.

[1] http://www.lexifi.com/blog/dynamic-types
[2] http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf

> One can write typed interpreters in the
> final-tagless style, with no GADTs.

Isn't this true of all GADTs examples? You have already shown that
GADTs can be relatively-practically expressible with equality types. I
suspect the justification for GADTs is not increased expressivity, but
a simpler/more familiar way to implement those
type-information-passing techniques -- just as ordinary algebraic
datatypes could be expressed with functional encodings, but are more
practical and convenient to use in the usual case. Besides, there is
the down-to-earth efficiency benefit of directly using first-order
data instead of functional encodings.

On Thu, Mar 22, 2012 at 7:01 AM,  <oleg@okmij.org> wrote:
>
> 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
>