From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 04368BBC1 for ; Thu, 21 Feb 2008 01:29:38 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKhUvEfAXQInh2dsb2JhbACBWY8FAQEBCAopn2g X-IronPort-AV: E=Sophos;i="4.25,382,1199660400"; d="scan'208";a="7520655" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 21 Feb 2008 01:29:37 +0100 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1L0Tb0J028996 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 21 Feb 2008 01:29:37 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABJVvEdCbwQbmWdsb2JhbACBWY8FAQEBAQEGBAQLCBifbA X-IronPort-AV: E=Sophos;i="4.25,382,1199660400"; d="scan'208";a="9405942" Received: from out3.smtp.messagingengine.com ([66.111.4.27]) by mail3-smtp-sop.national.inria.fr with ESMTP; 21 Feb 2008 01:29:36 +0100 Received: from compute2.internal (compute2.internal [10.202.2.42]) by out1.messagingengine.com (Postfix) with ESMTP id A521D954EE; Wed, 20 Feb 2008 19:29:35 -0500 (EST) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute2.internal (MEProxy); Wed, 20 Feb 2008 19:29:35 -0500 X-Sasl-enc: SPhLO+BnDzOtG7k4fgcoya4fngJ+Nua4qd0lkkUnzR67 1203553775 Received: from sponge.machinephasesystems.com (dsl092-191-028.sfo1.dsl.speakeasy.net [66.92.191.28]) by mail.messagingengine.com (Postfix) with ESMTPSA id 14C947544; Wed, 20 Feb 2008 19:29:30 -0500 (EST) Date: Thu, 21 Feb 2008 01:29:23 +0100 (CET) From: Martin Jambon X-X-Sender: martin@martin.ec.wink.com To: David Teller Cc: OCaml Subject: Re: [Caml-list] Auto-closing polymorphic variants ? In-Reply-To: <1203541049.11853.36.camel@Blefuscu> Message-ID: References: <1203541049.11853.36.camel@Blefuscu> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Miltered: at concorde with ID 47BCC5F1.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ens-lyon:01 variants:01 variants:01 val:01 val:01 unify:01 wildcards:01 wildcard:01 ocamlc:01 wildcards:01 polymorphic:01 polymorphic:01 wrote:01 wrote:01 caml-list:01 On Wed, 20 Feb 2008, David Teller wrote: > Dear list, > > There are still a number of things I don't quite understand about > polymorphic variants. For instance, polymorphic variants seem to be open > by default. > > # let a = `a ;; > val a : [> `a ] = `a > # let b = `b ;; > val b : [> `b ] = `b > > I can only assume this was done to keep the property that in > if ... then some_p else some_q > it must be possible to unify the types of some_p and some_q, which > wouldn't be possible with closed types. > > However, as mentioned in the discussion regarding exceptionless error > management, in conjunction with wildcards, sanity checks become > irrelevant, which may lead to hard-to-track errors, e.g. > > # let safe_div x = function > | 0. -> `Div_by_zero > | y -> `Ok (x /. y) ;; > val safe_div : float -> float -> [> `Div_by_zero | `Ok of float ] = > > # let idiv x y = > match safe_div (float_of_int x) (float_of_int y) with > | `Success x -> x > | _ -> nan ;; > val idiv : int -> int -> float = > > > Here, because of the wildcard, ocamlc didn't notice that we wrote > `Success where no such variant could happen. > > Now, it seems to me that this wouldn't a real problem if we had a way to > auto-close safe_div during the match, i.e. something like > > # let idiv x y = > match close (safe_div (float_of_int x) (float_of_int y)) with > | `Success x -> x > ^^^^^^^^^ > | _ -> nan ;; > > This pattern matches values of type [> `Success of 'a ] > but is here used to match values of type [ `Div_by_zero | `Ok of > float ] > The second variant type does not allow tag(s) `Success > > Of course, we could do that by manually closing the type of safe_div, > but this would essentially mean duplicating information. > > Either > # let idiv x y = > match (safe_div (float_of_int x) (float_of_int y) : > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > [ `Success of float | `Div_by_zero ] ) with > | `Success x -> x > | _ -> nan ;; > This expression has type [> `Div_by_zero | `Ok of float ] > but is here used with type [ `Div_by_zero | `Success of float ] > The second variant type does not allow tag(s) `Ok > > or > # let idiv x y = > match(safe_div (float_of_int x) (float_of_int y) : > [`Div_by_zero | `Ok of float]) with > | `Success x -> x > ^^^^^^^^^^^ > | _ -> nan ;; > This pattern matches values of type [> `Success of 'a ] > but is here used to match values of type [ `Div_by_zero | `Ok of > float ] > The second variant type does not allow tag(s) `Success > > Unfortunately, I can't seem to find anything comparable to that "close" > operator in the documentation, nor any design pattern which would attain > the same effect. > > Does anyone have ideas on this subject ? Yes: don't use wildcards mixed with concrete cases: Good: function `A -> ... | `B -> ... Good: function _ -> ... Bad: function `A -> ... | _ -> ... Martin -- http://wink.com/profile/mjambon http://martin.jambon.free.fr