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 2A5327EE94 for ; Tue, 8 Jan 2013 06:19:26 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAAKr61CFBoIF/2dsb2JhbABFDr1Yc4IeAQEEASccATUCAwsLDgouVwYTiBEFDaZbgzCBEAKGGoYCB4xcg1hhiGKNLIEchE+KXoI2TQ X-IronPort-AV: E=Sophos;i="4.84,428,1355094000"; d="scan'208";a="167690932" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail4-smtp-sop.national.inria.fr with ESMTP; 08 Jan 2013 06:19:23 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 85F9E6325; Tue, 8 Jan 2013 14:19:19 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 49D7C2564; Tue, 8 Jan 2013 14:19:19 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from [192.168.0.41] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 06456252A; Tue, 8 Jan 2013 14:19:19 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) Content-Type: text/plain; charset=windows-1252 From: Jacques Garrigue In-Reply-To: Date: Tue, 8 Jan 2013 14:19:35 +0900 Cc: =?windows-1252?Q?T=F6r=F6k_Edwin?= , caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: <8E57EAA9-9610-4960-BF5E-B0DEE9299B88@math.nagoya-u.ac.jp> References: <50E70504.6080502@etorok.net> To: Leo White X-Mailer: Apple Mail (2.1499) Subject: Re: [Caml-list] strange type inference for polymorphic variants 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 var= iant types) I agree that while the specification intends to be complete, it may not alw= ays be sufficient to understand all the details. On 2013/01/07, at 20:28, Leo White wrote: > The problem here is with how OCaml handles matches with default cases. Gi= ven the code: >=20 > match foo with > `Bar x -> x + 1 > | _ -> 0 >=20 > OCaml will conclude that foo has the type [> `Bar of int]. This means tha= t foo must have a type that includes a Bar tag, since Bar is in the lower b= ound of the type. >=20 > Conversly, given the code: >=20 > match foo with > `Bar x -> x +1 > | `Foo -> 0 >=20 > OCaml will conclude that foo has the type [< `Bar of int | `Foo ]. This m= eans that foo does not have to have a type that includes a Bar tag, since B= ar is only part of the upper bound. I should explain a bit the rationale behind this behavior, which may seem c= ounter-intuitive. It is mostly about avoiding accepting meaningless programs. At some point, OCaml did give the type [< `Bar of int | =85 ] 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 instan= ce of [ `Bar of int | =85 ]. However, there was a major drawback: it was extremely weak to typos. For instance let f (x : [`Bar of int | `Foo]) =3D match x with `Bat y -> y | _ -> 3 would be accepted, but return always 3=85 So I decided to remove the [< `Bar of int | =85 ] 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 [< somethi= ng] type, otherwise you get a [> something] type. Note that type annotations outside of patterns are ignored for that; you sh= ould write: let f =3D function (`Bar x : [< `Bar of _ | `Foo]) -> x | _ -> 3 > Interestingly, this problem is actually due to the syntax of OCaml. The f= ormal system on which the implementation of polymorphic variants is based (= see Section 6 of "Programming with Polymorphic Variants" by Jacques Garriqu= e) is capable of expressing the type that a match with a default case shoul= d have. However, the OCaml syntax has no means to express this type >=20 > In the syntax used in that paper, the example I gave above should actuall= y have the type [0 < T | Bar: int]. In other words, "foo" can have any vari= ant tags (there are essentially no lower or upper bounds), but if it has a = Bar tag then that tag has an int type. >=20 > 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 t= o avoid. The inability to catch typos seems to be too high a cost. Another thing we do not allow in OCaml is empty variant types: you cannot u= nify [< `A] with [< `B]. Again, empty variant types could have applications, but the rationale is th= at usually this should be seen as an error. Jacques Garrigue