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.7 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 07513BBC1 for ; Wed, 20 Feb 2008 21:57:34 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAIgivEfAXQInh2dsb2JhbACQXAEBAQgKKZgyhy4 X-IronPort-AV: E=Sophos;i="4.25,382,1199660400"; d="scan'208";a="22844027" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 20 Feb 2008 21:57:33 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1KKvX0m022612 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 20 Feb 2008 21:57:33 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGIjvEdC+VytkGdsb2JhbACQXAEBAQEHBAQJChEHmDeHLg X-IronPort-AV: E=Sophos;i="4.25,382,1199660400"; d="scan'208";a="7516334" Received: from ug-out-1314.google.com ([66.249.92.173]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Feb 2008 21:57:32 +0100 Received: by ug-out-1314.google.com with SMTP id k40so891053ugc.18 for ; Wed, 20 Feb 2008 12:57:32 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:subject:from:to:content-type:date:message-id:mime-version:x-mailer:content-transfer-encoding:sender; bh=MtenL/AcTjH65Dxm+DdRev1ALMdPWMPJEkGR8SPIV/0=; b=OmhB0Ov6s6DMWF1IB5jvhy6BBtUnL7q+BRNmjrBUOwETC+keSpeIBjbtFOo7/JVhdYvNuC7Bak3OhPKcrKTiSE3phuWzDUCKrRDQHfJYsqJ+fvFuqb1LTZwrwWxgd9GSzNL4UJN1OpbTmodYQDcAUwAyKyxdOSQXZZb2Z8OmPC8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:from:to:content-type:date:message-id:mime-version:x-mailer:content-transfer-encoding:sender; b=GKjf5MHtOK69jfypLeU6iDCnjsWLohCQGhTI9aUDOM92LDlH8O2uhG6KKPALeJqJHJssbq4a1HL7g2nxE8c0yM7ABBFjDO3RBIeyf/0r0xY3rw242m3ZnUVW9XX3PhELu0rbhd9KtVtjA5fxxljHJwqkJ2PdcfcLH0rDIpO1BJU= Received: by 10.66.218.15 with SMTP id q15mr489579ugg.36.1203541052440; Wed, 20 Feb 2008 12:57:32 -0800 (PST) Received: from ?192.168.0.12? ( [82.235.58.110]) by mx.google.com with ESMTPS id e20sm14463380fga.1.2008.02.20.12.57.29 (version=SSLv3 cipher=RC4-MD5); Wed, 20 Feb 2008 12:57:30 -0800 (PST) Subject: Auto-closing polymorphic variants ? From: David Teller To: OCaml Content-Type: text/plain Date: Wed, 20 Feb 2008 21:57:29 +0100 Message-Id: <1203541049.11853.36.camel@Blefuscu> Mime-Version: 1.0 X-Mailer: Evolution 2.12.1 Content-Transfer-Encoding: 7bit Sender: David Teller X-Miltered: at concorde with ID 47BC943D.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 univ-orleans:01 variants:01 val:01 val:01 unify:01 wildcards:01 wildcard:01 ocamlc:01 polymorphic:01 polymorphic:01 wrote:01 int:01 int:01 variant:02 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 ? Thanks, David