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 q3H1qiYV021101 for ; Tue, 17 Apr 2012 03:52:45 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0EAKjLjE+FBoIF/2dsb2JhbABEsj2CCQEBBAEnEwYDATUBAQMLCzQSVwaIHASmGIQ0hiSJAgEGkUmIXI0VkDWCdg X-IronPort-AV: E=Sophos;i="4.75,432,1330902000"; d="scan'208";a="140438783" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail4-smtp-sop.national.inria.fr with ESMTP; 17 Apr 2012 03:52:38 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8570162E5; Tue, 17 Apr 2012 10:52:35 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4A7AD40C3; Tue, 17 Apr 2012 10:52:35 +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=1nfilMGukGLJDuY+1A8CCwPJ76Q=; b=2klmoDwFBt2T8JxJWZfoQ5ihLDgC Mx8SdS5aijiNzJH5RacuGhIqNLfmF4k4hoIZAHwsg1erbXsja1ApAX9GXaP0HMV0 MBEKhWzhkWMgd2QkWzYD9ZCh75vO56Dw2rpJgdlUCX3NfC0ro7/WOyKsV3oYkh3W wBuwk/iQq6+SEdw= 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=hqfAGMC3MHbqIuOqRihsa6Q7Sll5gK3m7pvFEaPKooEaELQTuLQ1Ff+45Ptpd79SXM2MID9qQunR+DlU8x7Bp0m1+Je8T0aZxHpcKgE7LkXR/T0/67q7sQojEhxzojsmtOUW+MRJz8bY9reqkQGV6UeY83zVk9nTgZ1p4tMwN68=; 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 D8C9C40C2; Tue, 17 Apr 2012 10:52:34 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Tue, 17 Apr 2012 10:52:34 +0900 Cc: caml-list@inria.fr Message-Id: <08857D21-9495-4332-8BB9-315368430349@math.nagoya-u.ac.jp> References: To: Sebastien Mondet X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q3H1qiYV021101 Subject: Re: [Caml-list] Potential Feature Request: "Remove poly-variants from match-with statements" On 2012/04/17, at 0:24, Sebastien Mondet wrote: > I don't know if it is theoretically sound or possible, but > it would be helpful, if the typing of match-with statements with polymorphic > variants was able to remove one or more variants from the "catch-all" cases > > In the following code, it would mean that three_is_a_lot would be typed like > three_is_a_lot_2 without having to write all the cases. > > > # let how_much = function > | 1 -> `One > | 2 -> `Two > | 3 -> `Three > | n -> `A_lot;; > > val how_much : int -> [> `A_lot | `One | `Three | `Two ] = > > # let three_is_a_lot x = > match how_much x with > | `Three -> `A_lot > | any -> any;; > > val three_is_a_lot : int -> [> `A_lot | `One | `Three | `Two ] = > > # let three_is_a_lot_2 x = > match how_much x with > | `Three -> `A_lot > | `One | `Two | `A_lot as any -> any;; > > val three_is_a_lot_2 : int -> [> `A_lot | `One | `Two ] = > > > The practical use-case for us is that we use polymorphic variants to encode "semantic" errors in an Error/Result monad. This has been asked for repeatedly. I admit this could be useful in some cases but there are difficulties. One first question is, what are you really asking for? If you just want to be able to omit the pattern before "as", then it is probably doable (not easy, as in your example one has to detect that while the return type of how_much is open, other cases cannot happen), but would not add any expressivity. If you want the real thing, i.e. the ability to have functions that "skim" a variant type, then this gets much more difficult. let remove_Three = function `Three -> failwith "Three" | any -> any What kind of type should we give to this function? Probably something like: [`Three | 'a] -> [ 'a ] Note here that 'a is a new kind of type variable, that can only be used as a polymorphic variant row variable. Such type systems have been studied in the literature, and I think there is even an Haskell extension doing that, but this can easily get complicated. OCaml avoids introducing such new type variables by requiring that if two types share the same row variable they must be identical. In particular this rules out the above type. Removing this restriction would be a major design change. Jacques Garrigue