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 q2L9mPwm021797
	for <caml-list@sympa-roc.inria.fr>; Wed, 21 Mar 2012 10:48:25 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AsAHAJWiaU/ZSMDzjWdsb2JhbABEjG2oegQDgQ8iAQEBAQkJCwkSBSSCCQEBBAE6PwULCyElDwEEDRshE4gFCQe3V4lshxUEmzqFU4dh
X-IronPort-AV: E=Sophos;i="4.73,623,1325458800"; 
   d="scan'208";a="150495596"
Received: from fmmailgate05.web.de ([217.72.192.243])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 21 Mar 2012 10:48:15 +0100
Received: from moweb002.kundenserver.de (moweb002.kundenserver.de [172.19.20.108])
	by fmmailgate05.web.de (Postfix) with ESMTP id AC0586BA1811
	for <caml-list@yquem.inria.fr>; Wed, 21 Mar 2012 10:48:12 +0100 (CET)
Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002)
 with ESMTPA (Nemesis) id 0MNt8d-1SCmz12NWF-006dGC; Wed, 21 Mar 2012 10:48:12
 +0100
Received: from mrvn by frosties.localnet with local (Exim 4.77)
	(envelope-from <goswin-v-b@web.de>)
	id 1SAI9L-0003Gc-NM; Wed, 21 Mar 2012 10:48:11 +0100
From: Goswin von Brederlow <goswin-v-b@web.de>
To: Raoul Duke <raould@gmail.com>
Cc: caml-list@yquem.inria.fr
References: <87aa3mawg1.fsf@frosties.localnet>
	<CAPFanBHcs4V2OHB1VjCvb+xizPbQ7NQfWH_GwAvfNfnQ1wtfLQ@mail.gmail.com>
	<CAGrdgiVpG45Kgf2u0PHgDzH=yEOAMmydbXP-qsnLYC3MTzZSEw@mail.gmail.com>
	<CAJ7XQb6Tq8Qa4K3_TQKKH+-MNnXoUBLS0T68LhzwdSBOxo=d3Q@mail.gmail.com>
Date: Wed, 21 Mar 2012 10:48:11 +0100
In-Reply-To: <CAJ7XQb6Tq8Qa4K3_TQKKH+-MNnXoUBLS0T68LhzwdSBOxo=d3Q@mail.gmail.com>
	(Raoul Duke's message of "Mon, 19 Mar 2012 09:22:26 -0700")
Message-ID: <87mx7a2skk.fsf@frosties.localnet>
User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE)
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Provags-ID:  V02:K0:Ga/m80Ltx4SaFgw3iXw1LtL9wxqvEpRgHk2UMoc2r4S
 Dbp7KRtxr4BooLibQeKGIpGIW5+69JxnFDZtnN3UkLQjsF0d23
 Gv3KeEQdFNitBOM5j2nd9wMSUp5I5RFnLftZjbnO1dZ1XYM8un
 Weyj5vYoIud4WX8olefrJq8VDkl5QI4u2jw+jw3BwtVSMHEkgM
 bCnaL19uED+/funAeBlkw==
Subject: Re: [Caml-list] Wanted: GADT examples: string length, counting module x

Raoul Duke <raould@gmail.com> writes:

> On Mon, Mar 19, 2012 at 9:13 AM, Jesper Louis Andersen
>> If you want to play with dependent types, there are two ways which
>> seem popular at the moment: Agda or Coq.
>
> and some not popular ones...
>
> http://www.ats-lang.org/
>
> http://sandycat.info/blog/deptypes-shen/
>
> et. al.

Neigther of which are examples for GADT in ocaml.

MfG
        Goswin