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 6A4B07EE94 for ; Mon, 7 Jan 2013 13:48:45 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of edwin+ml-ocaml@etorok.net) identity=pra; client-ip=176.9.138.55; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="edwin+ml-ocaml@etorok.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of edwin+ml-ocaml@etorok.net designates 176.9.138.55 as permitted sender) identity=mailfrom; client-ip=176.9.138.55; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="edwin+ml-ocaml@etorok.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of postmaster@mail.etorok.net designates 176.9.138.55 as permitted sender) identity=helo; client-ip=176.9.138.55; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="postmaster@mail.etorok.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqwHAFLB6lCwCYo3/2dsb2JhbABFDoM5ugwWc4IeAQEEAScZAQEqCgIBAQ8LDgoJFg8JAwIBAgFFBg0BBwKIDQqmaIQ6AQWKZQaRFZYOhWuKXoI2QA X-IronPort-AV: E=Sophos;i="4.84,424,1355094000"; d="scan'208";a="167616750" Received: from mail.etorok.net ([176.9.138.55]) by mail4-smtp-sop.national.inria.fr with ESMTP; 07 Jan 2013 13:48:44 +0100 Received: from [172.30.42.2] (unknown [79.114.81.27]) by mail.etorok.net (Postfix) with ESMTPSA id EF4C646B5; Mon, 7 Jan 2013 13:48:42 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=etorok.net; s=MAILOUT; t=1357562923; bh=RwvQy4afbv/bPS0xAgsQTeKVi2WoG/bz3U1X/o3DFfg=; h=Message-ID:Date:From:MIME-Version:To:CC:Subject:References: In-Reply-To:Content-Type:Content-Transfer-Encoding; b=SCCQ8T3FXYb5iMgaPQ4rRuqR2x4FosPolRuvna9rN2+tpJEYBLYBoiaf3aUs80slv 1Q5ePVNtx9k5X1NCkAAUfQ2qftVLjAGwdXzLvmZXfHfqRZNPvMIhjLQLRVy8UFKnM4 UbD0CGnKEkP9QTBRHnm9DMEPz3r/quweO7wtxovg= Message-ID: <50EAC429.1020103@etorok.net> Date: Mon, 07 Jan 2013 14:48:41 +0200 From: =?ISO-8859-1?Q?T=F6r=F6k_Edwin?= User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.11) Gecko/20121122 Icedove/10.0.11 MIME-Version: 1.0 To: Leo White CC: caml-list@inria.fr References: <50E70504.6080502@etorok.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Virus-Scanned: clamav-milter 0.97.6 at mail X-Virus-Status: Clean Subject: Re: [Caml-list] strange type inference for polymorphic variants On 01/07/2013 01:28 PM, Leo White wrote: > 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. Thanks, I didn't see this explain in the manual. > > 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]. Thanks, that type makes sense now. Could the compiler be improved to realize that [< `A of a | `B of a > `A] and [< `A of a | `B of a] are the same type? > > > 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 Will read. > > 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. Best regards, --Edwin