From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 29C25800BE for ; Fri, 6 Jan 2017 02:39:14 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A+hl1OhLQa/0++yRpLNmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgeLPTxwZ3uMQTl6Ol3ixeRBMOAuq4C0bKd6P+ocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbQhFgDWwbalsIBmqogncuMsbipZ+J6gszRfEvmFGcP?= =?us-ascii?q?lMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLD?= =?us-ascii?q?QheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2UxLjlj?= =?us-ascii?q?sJOCAl/2HWksxwjbxUoBS9pxxk3oXYZJiZOOdicq/BeN8XQ3dKUMRMWCxbGo6z?= =?us-ascii?q?c4QAAfcBM+laoYfzqFgArRWgCwerH+7v1iZIhnrq0a06z+gsEwfL1xEgEdIUt3?= =?us-ascii?q?TUqc34OqMIXu+p1anI0CvMb+hL0jn88ofIaAohofCDXbJtb8Xa1E4iFwzfgVWK?= =?us-ascii?q?s4zlPjyV1vkTvGWA6upvT/6vi249pwF3uDevycAsi4nTiY4M11DI7z92z5ovKd?= =?us-ascii?q?26UE52eNipG4ZTuSGCL4Z6X80vTm9ytCs70LEKpJC2cDQQxJkn3xLSa/+Kf5KV?= =?us-ascii?q?7h/jV+udOyp0iGxmdb6lmhq/8Uqtx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+?= =?us-ascii?q?N4/ki72DaP0wDT6uZfIUAoj6bbLoQuwqIwlpYJt0TMBCD2mEL2jaCMb0kk5/Kk?= =?us-ascii?q?5P77bbn8pJ+cL5d4igD4MqswhsyyGfk0PwYAUmSB+OmwzqDv8EPlTLlQjvA6iq?= =?us-ascii?q?zZv4rbJcQfqK65GQhV0oM75hawFTimys4YnXgILFJYZh2KlI3pNEvSIPD4F/u/?= =?us-ascii?q?hU6jkDhsx/HGJLLtG4jNImLZn7j9Z7p96VZcxBIpzd9D/5JUFq0BIPXrV0Dtrt?= =?us-ascii?q?PYCxs5PxWww+bmE9V9ypgTWXmPA6+cKKPdq0WE5uMpI+mWZY8aoizxK/Y/562m?= =?us-ascii?q?sXhsv14ZZuGD0JAUZWrwSvJnJ17fa3fngdobOW0LuRMjRer2zkCEUHtTane+Uq?= =?us-ascii?q?Y26ys0To6rW9TtXIeo1Z6I1z6mE4YeSWlcEFGDDHqgI4qNQe0NZz+fCspojjxC?= =?us-ascii?q?U7GuTJ4okAzovQS8yaIxfbmcwTERqZ+2jIs93ObUjxxnsGUsV8k=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A1AADg825YlwWCBoVeGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgw0BAQEBAYIKjkmTU493hzgBhiECghAQAQEBAQEBAQE?= =?us-ascii?q?BAQESAQEBAQEIFghNgjMaAYIbAQUjBBkDAS4HAQEOCxgCAhgOAgJXBi6IVK8Ma?= =?us-ascii?q?IFrOoMIBwKEXhqCEQEBAQEBAQEDAQEBAQEBAQEXAQiBC4c8CIJXhEaDCC2CMYZ?= =?us-ascii?q?2B4kWiwKIFokukFqOI4QkNoFCLzMPAYIIgiGBeWSIZgEBAQ?= X-IPAS-Result: =?us-ascii?q?A0A1AADg825YlwWCBoVeGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgw0BAQEBAYIKjkmTU493hzgBhiECghAQAQEBAQEBAQEBAQESAQEBAQEIF?= =?us-ascii?q?ghNgjMaAYIbAQUjBBkDAS4HAQEOCxgCAhgOAgJXBi6IVK8MaIFrOoMIBwKEXhq?= =?us-ascii?q?CEQEBAQEBAQEDAQEBAQEBAQEXAQiBC4c8CIJXhEaDCC2CMYZ2B4kWiwKIFokuk?= =?us-ascii?q?FqOI4QkNoFCLzMPAYIIgiGBeWSIZgEBAQ?= X-IronPort-AV: E=Sophos;i="5.33,323,1477954800"; d="scan'208";a="207145477" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 06 Jan 2017 02:39:12 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 64826643A for ; Fri, 6 Jan 2017 10:39:09 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id D55D94148; Fri, 6 Jan 2017 10:39:08 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=j3zPK2voBsk5OT7pXF+ZJ38WcEI=; b=M9fa7kum/hbZVbjtgS14V5+KFmTc xMU9+1FE6HsI7u2cPQ7R+XPoHPeM1aiqSr1rfEWe0mXSp7v2xdth7yOSXbgpu8Kr DyepIDAcQusawGcf/CG6oFzFBUNm58KyI4PO/lJOxjxQ1pCOHNsJiqKUQ0RMRSoo uNMO95UCh1VxNPk= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=fAqvAGbjY9xPZ3cpStKXN5lTBjTVVVFDJaAM7TrZfPEB5GC/aA5oLMt14oEf8IN/KHE5iAWHJ9Y7xMgAMVMYCCq2ERPMz/qJsOBAJaKGD+NNXLNzvGC35jZuapHC52YdkxONGaH2hna1W81SoM5Pu12dnhacgMH8gTkMcviOjaw=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 1544AB70; Fri, 6 Jan 2017 10:42:51 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> Date: Fri, 6 Jan 2017 10:39:23 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <85E36448-5530-4745-8A83-FD6D4CA4531B@math.nagoya-u.ac.jp> References: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> To: Nils Becker X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] GADT+polymorphic variants quirk On 2017/01/03 23:05, Nils Becker wrote: >=20 > hi, >=20 > i am the OP of the stackoverflow question referred to by anton. >=20 >> I would suggest avoid using polymorphic variants here, using rather >> a simple encoding: >>=20 >> type whole =3D Whole >> type general =3D General >>=20 >> type _ num =3D >> | I : int -> _ num >> | F : float -> general num >=20 > i tried this simpler proposal and it does seem to work nicely. however, > what i'm really interested in is encoding somewhat more elaborate > subtyping relationships. for example, how would you handle the case > where there is a 'rational' number type inbetween integers and reals? i > don't see how your proposal can be generalized to that? >=20 > i tried to generalize the solution proposed by anton like this: >=20 > type integer =3D [ `Integer ] > type rational =3D [ integer | `Rational ] > type real =3D [ rational | `Real ] >=20 > type _ num =3D > | N : int -> [> integer ] num > | Q : int * int -> [> rational ] num > | R : float -> real num You can encode any finite set type using core types. The idea is just to use presence and absence. type pre =3D Pre type abs =3D Abs type integer =3D pre * abs * abs (* integer * rational * real *) type rational =3D pre * pre * abs type real =3D pre * pre * pre However, in this case we are only taking about a linear inheritance hierarc= hy, which can be expressed more compactly. For instance type real =3D Real type =E2=80=99a rat =3D Rational of =E2=80=98a type rational =3D int * int rat type integer =3D int rat In general, any linear hierarchy can be encoded using type level natural nu= mbers type zero =3D Zero type =E2=80=98a succ =3D Succ of =E2=80=98a which in this case would give type real =3D zero type rational =3D zero succ type integer =3D zero succ succ This scheme can be extended to any n-ary tree hierarchy, using a n-ary cons= tructor in place of succ. Jacques