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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 1433A7FC01 for ; Mon, 26 Jan 2015 05:06:01 +0100 (CET) Received-SPF: None (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkwIAMK8xVSFBoIFVmdsb2JhbABahDHMLgKBUQEBAQEBBgEXCwoFFy6EDQEFOgYDATUBAQ4LGBwSQxQGiD69F4VYAopghEkBAQEBAQEBAwEBAQEBAQEBEwEGj0UzB4MWgROKC44JgRWNaoM9hB9ggkIBAQE X-IPAS-Result: AkwIAMK8xVSFBoIFVmdsb2JhbABahDHMLgKBUQEBAQEBBgEXCwoFFy6EDQEFOgYDATUBAQ4LGBwSQxQGiD69F4VYAopghEkBAQEBAQEBAwEBAQEBAQEBEwEGj0UzB4MWgROKC44JgRWNaoM9hB9ggkIBAQE X-IronPort-AV: E=Sophos;i="5.09,466,1418079600"; d="scan'208";a="118572647" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 26 Jan 2015 05:05:49 +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 DF242669E; Mon, 26 Jan 2015 13:05:46 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id ED00741B8; Mon, 26 Jan 2015 13:05:45 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=Skwl3XH/g6XVaDytAuxGNEXrSEE=; b=K49jgm5yT7xFfR4tGm5RuXL2HSJu 4vdHkgzZ7rYBuAUhzYI8sRG6xLacFQ4SRlH9b4iIv34JZ/fCGN6qQZQq5tYake2v 9oRK1EZkaQQcfz91Ex2riYIqLJGDJhwXIqvr7xjfkpsiyoqvEJYPIfxpy0No769/ E4cA+h5bi5YgSwI= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=S7cVeMzlGJuTB/bQsOzv/8mK1diK6SYYdEijA1nMvP3Ryz55ff3vdnGm6X/nBxp9Iyd3k1HVErvcYEstQdKWiAPKLd5mRAHMSCO0k1J+mTTbmyoMnJKucVVj0+docQIXdCcHkCAMKKFaeFYTQKQiuxybgXD/jnEwnr8ynrUPEcw=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id C5BC241B6; Mon, 26 Jan 2015 13:05:45 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 8.1 \(1993\)) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <02B4AAD3-9AD1-42F8-BDCA-FFAA7EA43F03@gmail.com> Date: Mon, 26 Jan 2015 13:05:44 +0900 Cc: David Allsopp , OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: References: <02B4AAD3-9AD1-42F8-BDCA-FFAA7EA43F03@gmail.com> To: Jordo X-Mailer: Apple Mail (2.1993) Subject: Re: [Caml-list] Explicit Arity with Polymorphic Variants On 2015/01/26 04:57, Jordo wrote: >=20 > You've listed some good examples of why this would be difficult to implem= ent and some examples of how this would be confusing to developers. But I a= m having a hard time seeing how you have demonstrated why polymorphic varia= nts cannot assume two forms - each incompatible with the other, with any pa= rticular form being completely inferred. I am not claiming that a distincti= on between the two forms is not needed at the type level - the two forms wo= uld be incompatible with each other at the type level just as they are inco= mpatible for standard variants. My question was why does a distinction at t= he type level require a type *definition* (which was your original claim). = For the sake of experimentation, assume you can create any syntax you need = that would unambiguously express which of the two forms is being reasoned a= bout in all situations. Indeed, there is no theoretical difficulty in introducing multi-argument po= lymorphic variants, and they were considered at some point. However, for this to work this should imperatively be supported at the type= level too: multi-argument polymorphic variant should have a type incompati= ble with single-argument ones. So this means making the type algebra more complex, adding extra syntax bot= h at the value/pattern and type level, and extending the unification and ty= pe inference algorithms, for something that doesn't seem that useful (if yo= u need performance, you're better served by normal variants anyway). Of course you're free to try to add them to the compiler :-) Jacques=