From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2M624VM017649
	for <caml-list@sympa-roc.inria.fr>; Thu, 22 Mar 2012 07:02:04 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AvsLAO6+ak/RRAGzW2dsb2JhbABEpg8BkSMXBwQJBhcngg4pUoEkKIgPC7gojUKDIgSVXgGTDw
X-IronPort-AV: E=Sophos;i="4.73,628,1325458800"; 
   d="scan'208";a="150637899"
Received: from eeoth.pair.com ([209.68.1.179])
  by mail1-smtp-roc.national.inria.fr with SMTP; 22 Mar 2012 07:01:58 +0100
Received: (qmail 44173 invoked by uid 3366); 22 Mar 2012 06:01:57 -0000
Date: 22 Mar 2012 06:01:57 -0000
Message-ID: <20120322060157.44172.qmail@eeoth.pair.com>
From: oleg@okmij.org
To: goswin-v-b@web.de
CC: caml-list@inria.fr
X-Validation-by: oleg@okmij.org
Subject: [Caml-list] Wanted: GADT examples: string length, counting module x


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.