From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id CA28ABBAF for ; Fri, 29 Oct 2010 18:03:06 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiIBABSNykzUGyoCkWdsb2JhbACTW415FQEBAQEJCwoHEQMfvyiFSASKU4MIGQ X-IronPort-AV: E=Sophos;i="4.58,260,1286143200"; d="scan'208";a="85752700" Received: from smtp2-g21.free.fr ([212.27.42.2]) by mail1-smtp-roc.national.inria.fr with ESMTP; 29 Oct 2010 18:03:06 +0200 Received: from [192.168.1.3] (unknown [82.237.71.191]) by smtp2-g21.free.fr (Postfix) with ESMTP id 632D34B01A6 for ; Fri, 29 Oct 2010 18:02:59 +0200 (CEST) Message-ID: <4CCAF032.7020706@inria.fr> Date: Fri, 29 Oct 2010 18:02:58 +0200 From: Xavier Leroy User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.12) Gecko/20100915 Thunderbird/3.0.8 MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Generalized Algebraic Datatypes References: <904846.44200.qm@web111513.mail.gq1.yahoo.com> <129751088.61814.1288367649864.JavaMail.root@zmbs4.inria.fr> In-Reply-To: <129751088.61814.1288367649864.JavaMail.root@zmbs4.inria.fr> X-Enigmail-Version: 1.0.1 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; datatypes:01 syntax:01 syntax:01 coq:01 syntaxes:01 superset:01 haskell-like:01 wrote:01 syntactic:01 caml-list:01 algebraic:03 jacques:03 generalized:04 declarations:04 xavier:06 Jacques Le Normand wrote: > Assuming I understand this syntax, the following currently valid type > definition would have two interpretations: [...] Don't take the syntax from my 2008 CUG talk too seriously, it was just a mock-up for the purpose of the talk. Besides, it's too early for a syntax war :-) This said, Coq could be another source of syntactic inspiration: it has several equivalent syntaxes for inductive type declarations (a superset of GADTs), one Haskell-like, others more Caml-like. - Xavier Leroy