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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 29F6B7EE94 for ; Mon, 7 Jan 2013 12:28:59 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@hermes.cam.ac.uk) identity=pra; client-ip=131.111.8.151; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="lpw25@hermes.cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@hermes.cam.ac.uk) identity=mailfrom; client-ip=131.111.8.151; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="lpw25@hermes.cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-51.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.151; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="postmaster@ppsw-51.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aq4AAMWw6lCDbwiXmWdsb2JhbABFvVMWDgEBAQEBCAsLBxQngh8BBScRNAoDEAEKRlcGiCqwVYUokRUDm3aJE4Q/ X-IronPort-AV: E=Sophos;i="4.84,423,1355094000"; d="scan'208";a="167607975" Received: from ppsw-51.csi.cam.ac.uk ([131.111.8.151]) by mail4-smtp-sop.national.inria.fr with ESMTP; 07 Jan 2013 12:28:58 +0100 X-Cam-AntiVirus: no malware found X-Cam-SpamDetails: not scanned X-Cam-ScannerInfo: http://www.ucs.cam.ac.uk/email/scanner/ Received: from hermes-1.csi.cam.ac.uk ([131.111.8.51]:53402) by ppsw-51.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:25) with esmtpa (EXTERNAL:lpw25) id 1TsAsz-0000O3-ZP (Exim 4.72) (return-path ); Mon, 07 Jan 2013 11:28:58 +0000 Received: from prayer by hermes-1.csi.cam.ac.uk (hermes.cam.ac.uk) with local (PRAYER:lpw25) id 1TsAsz-0001Ge-V9 (Exim 4.72) (return-path ); Mon, 07 Jan 2013 11:28:57 +0000 Received: from [128.232.64.15] by webmail.hermes.cam.ac.uk with HTTP (Prayer-1.3.5); 07 Jan 2013 11:28:57 +0000 Date: 07 Jan 2013 11:28:57 +0000 From: Leo White To: =?ISO-8859-1?Q?T=F6r=F6k_Edwin?= Cc: caml-list@inria.fr Message-ID: In-Reply-To: <50E70504.6080502@etorok.net> References: <50E70504.6080502@etorok.net> X-Mailer: Prayer v1.3.5 Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset=ISO-8859-1 Sender: "L.P. White" Subject: Re: [Caml-list] strange type inference for polymorphic variants Hi This is an interesting example of one the problems with how polymorphic variants are implemented in OCaml. However, firstly I must address your confusion over the meaning of [< `A of a | `B of a > `A ]. The "> `A" here means that the type must include an `A tag. It is a lower bound for the variant types that can be used. Since the upper bound of the type ("< `A of a | `B of a") already tells us what type the `A tag must have there is no need to include that information in the lower bound. >Here is some simplified code that fails to compile: ># type a = string * string;; >type a = string * string ># module Bad3 : sig > val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit >end = struct > let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = () > let specific a b = false > let copy a b = match a, b with > | `A x, `A y -> > if not (specific (`A x) (`A y)) then > generic a b > | _, _ -> > generic a b >end;; >Error: Signature mismatch: > ... > Values do not match: > val copy : > [< `A of a | `B of a > `A ] -> [< `A of a | `C of a > `A ] -> > unit > is not included in > val copy : [< `A of a | `B of a ] -> [< `A of a | `C of a ] -> > unit The problem here is with how OCaml handles matches with default cases. Given the code: match foo with `Bar x -> x + 1 | _ -> 0 OCaml will conclude that foo has the type [> `Bar of int]. This means that foo must have a type that includes a Bar tag, since Bar is in the lower bound of the type. Conversly, given the code: match foo with `Bar x -> x +1 | `Foo -> 0 OCaml will conclude that foo has the type [< `Bar of int | `Foo ]. This means that foo does not have to have a type that includes a Bar tag, since Bar is only part of the upper bound. This is why your example includes a spurious "> `A". The match gives "a" the type [> `A of a], while the use of "generic" gives "a" the type [< `A of a | `B of a], when these are unified they become [< `A of a | `B of a > `A]. Interestingly, this problem is actually due to the syntax of OCaml. The formal system on which the implementation of polymorphic variants is based (see Section 6 of "Programming with Polymorphic Variants" by Jacques Garrique) is capable of expressing the type that a match with a default case should have. However, the OCaml syntax has no means to express this type In the syntax used in that paper, the example I gave above should actually have the type [0 < T | Bar: int]. In other words, "foo" can have any variant tags (there are essentially no lower or upper bounds), but if it has a Bar tag then that tag has an int type. I don't think that it would be difficult to use such a type within OCaml, but as I said the syntax has no means to express it. This is also the reason why a type such as [ `A of int or float ] (analagous to the [ `A of int & float ] that OCaml does support) can not be supported in OCaml. Personally, I wouldn't mind replacing the current polymorphic variant syntax with a more expressive one (and then slowly depreciating the old one). However, I imagine most people would consider this too large a change for too small a gain. Regards, Leo