From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2MGweK7017999 for ; Thu, 22 Mar 2012 17:58:40 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkkCAABZa0/ZSMD4k2dsb2JhbABEtzwiAQEBAQkJCwkUAySCCQEBAwEBOj8FCwshJQ8BBCg0iAUJB7h4jUKDIgSbOo01 X-IronPort-AV: E=Sophos;i="4.73,630,1325458800"; d="scan'208";a="137301720" Received: from fmmailgate07.web.de ([217.72.192.248]) by mail4-smtp-sop.national.inria.fr with ESMTP; 22 Mar 2012 17:58:34 +0100 Received: from moweb001.kundenserver.de (moweb001.kundenserver.de [172.19.20.114]) by fmmailgate07.web.de (Postfix) with ESMTP id 25CD7F6DF98 for ; Thu, 22 Mar 2012 17:58:34 +0100 (CET) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002) with ESMTPA (Nemesis) id 0Lcxfc-1SbKif1saO-00j0XK; Thu, 22 Mar 2012 17:58:33 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1SAlLM-0001yP-FB; Thu, 22 Mar 2012 17:58:32 +0100 From: Goswin von Brederlow To: oleg@okmij.org Cc: goswin-v-b@web.de, caml-list@inria.fr References: <20120322060157.44172.qmail@eeoth.pair.com> Date: Thu, 22 Mar 2012 17:58:32 +0100 In-Reply-To: <20120322060157.44172.qmail@eeoth.pair.com> (oleg@okmij.org's message of "22 Mar 2012 06:01:57 -0000") Message-ID: <87sjh08tdz.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:KFOUMpELG6H5X2lXjnoVZu5vKukEGRSkuA5luWIGqud G8R4mLiE2YgiqGY/H0/YJqFTWbdEK+QNoRcdmcliPruACIg5+/ n8e+TdHDdiMVqu9t5RJ0terOAe+F3Qm2h5kXfNk3yepUCc6y3I 2xM4Ps0a65/c4/rpKSgn8zXxpsoOJ4ik+60pjswZjFjdY+WY4h XF9gUJP86PHakUEBE8jow== Subject: [Caml-list] Re: Wanted: GADT examples: string length, counting module x 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