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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id DCAE37EE51 for ; Sat, 4 May 2013 14:28:39 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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: Aj8EAKj9hFGFBoIFdGdsb2JhbABQDsJ0gRIOAQwVCDyCHwEBBAEnHAE1AgMLCxgcEiE2BgESh3oDCQWve4RFAoRnDUuHNgeMW4IjMweCcmGJG4wwgWSMEYdvTg X-IPAS-Result: Aj8EAKj9hFGFBoIFdGdsb2JhbABQDsJ0gRIOAQwVCDyCHwEBBAEnHAE1AgMLCxgcEiE2BgESh3oDCQWve4RFAoRnDUuHNgeMW4IjMweCcmGJG4wwgWSMEYdvTg X-IronPort-AV: E=Sophos;i="4.87,611,1363129200"; d="scan'208";a="16035730" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 May 2013 14:28:37 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 523C4635F; Sat, 4 May 2013 21:28:34 +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 D0DCE252A; Sat, 4 May 2013 21:28:33 +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 tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 799BE2503; Sat, 4 May 2013 21:28:33 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) Content-Type: text/plain; charset=windows-1252 From: Jacques Garrigue In-Reply-To: Date: Sat, 4 May 2013 21:28:49 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <517E2818.5040506@frisch.fr> <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> <0BC2A384-6D0F-49F2-BD68-5C840BA0888A@math.nagoya-u.ac.jp> <44ACA8B7-8DCC-4948-8D8A-7C7A7FB0B4AF@math.nagoya-u.ac.jp> To: Gabriel Scherer , Leo P White X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/05/04, at 16:09, Gabriel Scherer wrote: >> One way to solve this is to check that the type identified by 'a can >> actually be handled as a real variable (its internal variables do >> not occur out of it), which would solve the discrepancy. >=20 > If I understand correctly, you are saying that this "constraint", in > absence of injectivity, could be handled semantically like GADTs with > non-injective equations, that is as quantifying locally on a ("true") > existential variable? I did not think of it that way, but this is something like that. By abstracting on the (common) part of the types which contains abstract type constructor, we can fall back to exact variance information. > Handling existential variables (in fact local type constructors) > attached to GADT constructors is well-understood as they have clear > introduction sites and scopes, exactly where their constructor is > matched. When you say that checking the "constraint" case is painful, > is it related to the fact that there is no such corresponding > term-level marker? Well yes, you have to find the common parts yourself. Actually this is not that bad. I have committed a fix, which works by recursing on the body of the definition, trying to find equal types inside the constrained parameters. If the variance at this point is correct, one doesn't need to look inside. This may be a bit expensive, but usually constraints are not big. In theory one could do even better, by abstracting on the "real" variance of abstract types. Then the variance of an occurence becomes a set of paths (composition of variances) from the root of the type definition. However, this just looks too complicated to me... > On Sat, May 4, 2013 at 8:46 AM, Jacques Garrigue > wrote: >> Ironically, I have just found that lablgtk2 does not compile with the fi= xed version. >> lablgtk2 does not use GADTs, but it uses constrained type parameters in = classes. >>=20 >> The problem is as follows: >>=20 >> gobject.mli: >> type -'a gobj >>=20 >> gContainer.mli: >> class virtual ['a] item_container : >> object >> constraint 'a =3D < as_item : [>`widget] obj; .. > >> method add : 'a -> unit >> =85 >> end >>=20 >> File "gContainer.mli", line 126, characters 6-665: >> Error: In this definition, a type variable cannot be deduced >> from the type parameters. This problem is now fixed, without needing to change lablgtk2 sources. On 2013/04/30, at 22:06, Leo White wrote: >>>> type 'a t =3D T;; >>>> type _ g =3D G : 'a -> 'a t g;; >>>=20 >>> I don't see why this could not be allowed without the restriction you >>> propose. I thought that this was rejected in 4.00 because 4.00 used >>> bi-variance as an (unsafe) approximation of non-injective. Since we now >>> track injectivity separately from variance g be accepted (with 'a covar= iant). >>=20 >> In our work, this GADT definition would be accepted, and: >> (1) matching on the constructor G does not give any information on the >> value of the existential type 'a >> (2) the parameter of g (not 'a, the one marked _ above) may marked >> covariant or invariant, because the constructor t is upward-closed but >> not downward-closed (private types) >=20 > I don't think the argument to G needs to be given an existential type, > as long as the parameter of g is marked invariant. >=20 > The parameter to g should be marked invariant for two reasons: > 1) It is constrained in the result type of a GADT constructor which, as > discussed on this list previously, forces it to be invariant (at least > for now, see Gabriel's paper for further details). > 2) Marking it as anything other than invariant, would entail marking > 'a as bi-variant, when it is in fact covariant. >=20 > This second reason also occurs in types with constraints, for example: >=20 > type 'a s =3D 'b constraint 'a =3D 'b t >=20 > here 'b is covariant (used in covariant and bi-variant positions), but > marking 'a as any variance other than invariant would entail marking 'b > as bi-variant. Sorry for the slow answer. The implementation was not correct yet... I think there is a misunderstanding here. The problem is that 'b has two variances: its internal one, inferred from its occurrences inside the body of the type, and its external one, defined by its occurences inside parameters of the type. For the definition to be correct, we need the external variance to be at least as rigid as the internal one. The extra difficulty is that our knowledge of variances is only approximati= ve (due to abstraction), and we have to use lower bounds on external variances, and an upper bounds on internal variances (to be sure that we are safe). Here the lower bound says just that the external variance of 'b is the composition of invariant and injective, while the internal one is covariant. If invariant o injective were defined as only injective, it would be less rigid than the internal version, hence the need to have invariant o injective =3D invariant. (But for the converse, we only have injective o invariant =3D injective) Actually I realized that just positive, negative and injective are not suff= icient. To fully accommodate the need for upper and lower bounds, we end up needing 7 different variance flags! may_pos, may_neg : the variable may appear at positive or negative occurrences in the real definition; this is an upper bound, corresponding to variance annotations on abstract types may_weak: needed to make type inference principal pos, neg: we now that the variable appears at positive or negative occurrences in the real definition; this is a lower bound inj: either pos, or neg, or parameter of a concrete definition; does not disappear by expansion inv: pos and neg simultaneously in a concrete definition; needed the above composition inv o inj =3D inv We have the hierarchy unknown < inj < pos \/ neg < pos /\ neg < inv. Of course not all combinations are valid, (for instance pos implies may_pos, etc=85) but this is still mind boggling. But those are not sufficient to solve the lablgtk2 problem above: calling 'b the row variable of [> `widget], its internal variance is neg o pos o may_neg, but its external variance is inv o pos o may_neg. The result is may_pos internally, but externally the result is may_pos /\ may_neg, whose lower bound is just "unknown". Hence the need to "abstract" on common types, when their internal variables do not escape. The variance of 'a internally is neg, and externally inv, so all is fine. This is a bit complicated, but the full specification is clear enough. Thanks to the detection of common types, the fact that the only flags for abstract types are may_pos and may_neg is not too much a problem for constrained parameters. Jacques Garrigue=