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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 802BF7F1E1 for ; Sun, 13 Jan 2013 18:58:18 +0100 (CET) Received-SPF: None (mail1-smtp-roc.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=mail1-smtp-roc.national.inria.fr; envelope-from="edwin+ml-ocaml@etorok.net"; x-sender="edwin+ml-ocaml@etorok.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.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=mail1-smtp-roc.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 (mail1-smtp-roc.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=mail1-smtp-roc.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: AgEFAA318lCwCYo3/2dsb2JhbABEgmu7GRZzgh4BAQQBJwsBDQEBNgIPCxgJFg8JAwIBAgFFEwgCiA8HAwiiaoQ6AQWLfgaMdYQ5lg6BHI8tgnc X-IronPort-AV: E=Sophos;i="4.84,464,1355094000"; d="scan'208";a="189695382" Received: from mail.etorok.net ([176.9.138.55]) by mail1-smtp-roc.national.inria.fr with ESMTP; 13 Jan 2013 18:58:17 +0100 Received: from [IPv6:2a02:2f02:1022:9237:1e6f:65ff:fe23:db0d] (unknown [IPv6:2a02:2f02:1022:9237:1e6f:65ff:fe23:db0d]) by mail.etorok.net (Postfix) with ESMTPSA id F2B9F46B4 for ; Sun, 13 Jan 2013 18:58:16 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=etorok.net; s=MAILOUT; t=1358099897; bh=cX4aMYVia5xBqzOXcKCov/Nca+qQCBd+aCVCeCwS0Ys=; h=Message-ID:Date:From:MIME-Version:To:Subject:References: In-Reply-To:Content-Type:Content-Transfer-Encoding; b=c6V4vAt/Fqv2fFfTXDyxC+6SGpv6qPdvsyfLgEn6CwtMJm1zmNQvPK1GjmGcBfoYd xe+nacY2F61CQGXAGKWE7587DtFhiXTeOzg6tzgzX3Wl2PPtedDi5h2gaJ/uFFmj6u shlkvt7WuYcokH5cfuEYljL8EF8MNbNOFwPoa95M= Message-ID: <50F2F5B7.5040706@etorok.net> Date: Sun, 13 Jan 2013 19:58:15 +0200 From: =?windows-1252?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: caml-list@inria.fr References: <50E70504.6080502@etorok.net> <8E57EAA9-9610-4960-BF5E-B0DEE9299B88@math.nagoya-u.ac.jp> In-Reply-To: <8E57EAA9-9610-4960-BF5E-B0DEE9299B88@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 8bit 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/08/2013 07:19 AM, Jacques Garrigue wrote: > Hi Leo and Torok, > > A first remark is that a lot is already in the tutorial part of the manual, > with some extra details in the reference part: > http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.html#toc36 > http://caml.inria.fr/pub/docs/manual-ocaml-4.00/types.html (Polymorphic variant types) > > I agree that while the specification intends to be complete, it may not always > be sufficient to understand all the details. Thanks for the detailed explanation, it was very useful. > > > At some point, OCaml did give the type [< `Bar of int | … ] to the first example, meaning that > `Bar is accepted but not required, and there may be other tags. > This actually avoided Torok's problem: [< `Bar of int | `Foo] was an instance of [ `Bar of int | … ]. > However, there was a major drawback: it was extremely weak to typos. > For instance > let f (x : [`Bar of int | `Foo]) = match x with `Bat y -> y | _ -> 3 > would be accepted, but return always 3… > > So I decided to remove the [< `Bar of int | … ] from the type algebra. > This means that at some point, one has to choose between [> `Bar of int] (which allows > extra constructors, but requires `Bar), and [< `Bar of int | `Foo] (where `Foo could be replaced > by any concrete list of constructors). > Currently, this is done just after typing all the patterns. > If at that point you know the exhaustive list of tags, you get a [< something] type, > otherwise you get a [> something] type. > Note that type annotations outside of patterns are ignored for that; you should > write: > let f = function (`Bar x : [< `Bar of _ | `Foo]) -> x | _ -> 3 Could some of this be added to the advanced use part of the manual? > >> 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 omission in the syntax is intentional: this is the semantics we want to avoid. > The inability to catch typos seems to be too high a cost. Agreed. I don't want any changes to the language either, I'm happy with the way OCaml implement polymorphic variants; now that I understand more about how it works. The type errors given by the compiler could provide more details though. I've opened a bug on mantis with a patch that implements more detailed errors, like: Values do not match: val foo : [< `A of int | `B of string > `A ] -> unit is not included in val foo : [< `A of int | `B of string ] -> unit Type component [ `A of int ] does not match [< `A of int ] Types for tag `A are incompatible: the tag is mandatory in the first type only Values do not match: val f : [> `Bat of int ] -> int is not included in val f : [< `Bar of int ] -> int Type component [> `Bat of int ] does not match [< `Bar of int ] The second variant type is missing mandatory tag(s) `Bat Best regards, --Edwin