From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 6F29DBBAF for ; Sat, 30 Oct 2010 07:15:01 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhYBAO9Gy0zRVdW2kGdsb2JhbACTTo1yCBUBAQEBCQkMBxEDH6IWi3GFb4kFAQEDBYU/BIRVhX+DbIIIgyk X-IronPort-AV: E=Sophos;i="4.58,262,1286143200"; d="scan'208";a="64591050" Received: from mail-yx0-f182.google.com ([209.85.213.182]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Oct 2010 07:15:00 +0200 Received: by yxl31 with SMTP id 31so2497860yxl.27 for ; Fri, 29 Oct 2010 22:14:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:subject:mime-version :content-type:from:in-reply-to:date:content-transfer-encoding :message-id:references:to:x-mailer; bh=rGd8bKYNI9jl788TDgPBMICRXgc8mZQhgxKcAh9wA7g=; b=uQhWHADoATbzuQINewW1btDW1/jTZJu0DezYNR3MmcpYjn+FfKyErPX+8AV0zzzxMe OXe+9zqDxi92DWdk57zrYLcu5g798WVpXH5f1LwrC6MI2iXkXXY4pwil5xTL9wTyiNpK Pve8tAVpkvdlBOUPt/EadYrhNfJS92WwA3n0k= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date :content-transfer-encoding:message-id:references:to:x-mailer; b=dPusjysSsj0OMxinyB3IVd3mLH79WlDt+ORD4+wkV/2enWPtIPVDt6RMtdrsIfwUBB hUjPfR6egrrtB14eozYdPKrFLfaEMaDicxM2GzhmYgXoK0srZKeVX4OQ8KLm0bas3R3O 0FIioQkfNAV6CklWEqEp4bkWwRZV7LkBPrUd4= Received: by 10.151.149.9 with SMTP id b9mr23788057ybo.114.1288415699699; Fri, 29 Oct 2010 22:14:59 -0700 (PDT) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id z30sm2449084yhc.9.2010.10.29.22.14.57 (version=TLSv1/SSLv3 cipher=RC4-MD5); Fri, 29 Oct 2010 22:14:58 -0700 (PDT) Sender: Jacques Garrigue Subject: Re: [Caml-list] Re: Generalized Algebraic Datatypes Mime-Version: 1.0 (Apple Message framework v1081) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Sat, 30 Oct 2010 14:14:56 +0900 Content-Transfer-Encoding: quoted-printable Message-Id: References: <904846.44200.qm@web111513.mail.gq1.yahoo.com> To: caml-list@inria.fr X-Mailer: Apple Mail (2.1081) X-Spam: no; 0.00; datatypes:01 jacques's:01 bool:01 bool:01 syntax:01 constructors:01 existential:01 syntax:01 unification:01 coq:01 haskell:01 existential:01 wrote:01 wrote:01 matched:01 On 2010/10/30, at 8:01, Jacques Le Normand wrote: > On Fri, Oct 29, 2010 at 5:37 PM, bluestorm = wrote: > Note that, as in Jacques's examples, the constructor function was not = curryfied. (type t =3D A of bool * int) would generate a function (A : = bool * int -> t). It doesn't help the already tricky confusion between = (A of bool * int) and (A of (bool * int))... > By the way, it is unclear if > | App : ('a -> 'b) t -> 'a t -> 'b t > would be accepted in Jacques proposal. If not, I think going back to a = "of ..." syntax would be wiser. >=20 > It is accepted. In fact, that constructor is part of an example on my = webpage. > If there's any doubt, you can always download the source and try it = out. Actually, curryfied constructors are not allowed, so this is not = accepted. (Existential types are allowed, which may have confused the other = Jacques) To go back to the main subjec,t the syntax with an explicit return type = was chosen because it is closer to the way gadts are implemented here than a syntax = based on constraints. Namely the the type of the expression matched get = refined through unification with the return type of the corresponding case. It also happens to be the usual syntax in Coq and Haskell, so this should not come as a shock to most people. If the risk of confusion with constructors-as-functions is deemed = problematic, a syntax like App of ('a -> 'b) t * 'a t : 'b t seems OK too. Actually this would have the advantage of allowing the scope of = existential variables to be explicit. I.e. one could write App of 'a. ('a -> 'b) t * 'a t : 'b t Jacques Garrigue