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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 28E9A7EE51 for ; Tue, 30 Apr 2013 11:12:31 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.50 as permitted sender) identity=mailfrom; client-ip=209.85.214.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f50.google.com) identity=helo; client-ip=209.85.214.50; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f50.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Al8DAOSIf1HRVdYyk2dsb2JhbABSDoMvrD6SGXoIFg4BAQEBBwsLCRQEJIIfAQEEAScZARsSBAcBAwELBgULDQ0hIgERAQUBChIGExIJh2gBAwkGDKJyjDGBcYEMhHAKGScDClmHKQEFDI1cgTIHg08Dlx6BJo4fFimDeEE6gTc X-IPAS-Result: Al8DAOSIf1HRVdYyk2dsb2JhbABSDoMvrD6SGXoIFg4BAQEBBwsLCRQEJIIfAQEEAScZARsSBAcBAwELBgULDQ0hIgERAQUBChIGExIJh2gBAwkGDKJyjDGBcYEMhHAKGScDClmHKQEFDI1cgTIHg08Dlx6BJo4fFimDeEE6gTc X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="12722572" Received: from mail-bk0-f50.google.com ([209.85.214.50]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 30 Apr 2013 11:12:30 +0200 Received: by mail-bk0-f50.google.com with SMTP id ik5so122182bkc.23 for ; Tue, 30 Apr 2013 02:12:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:mime-version:in-reply-to:references:from:date:message-id :subject:to:cc:content-type; bh=AgaM/vxRVm2yIF9vCmcp4dbsQWxTvZe74gQCCMC95KQ=; b=S/DL5n5vV4oDkOJ7f8CsBp8yVTH4E71QrEunpYOhZSVneHPeIdiBxzC0S1e1sF+Ebr 1BOrVuP533plSD368CDso/zKYum/NeS/fcF5Pr2PRdEkLWW7L3+QA7kQLqd+GiK3Xcxa buMxgIaZyAvYo8jjOQEGDubGyX9uJVDfOeCUjdrqMNRouPOWati6L1A9+nSi5ZfFCuU7 CjBS9RscHdJhuCMwgycxF0GUAQyfIS63NrJZ5IQh81wkfv6mRvlSYc/DeUy6N3+y6W8I BTp+ROKrXK9070VFv+ZO7XhSo3C7Eq9BZ/3L5LaY/A2rCtuCmlrZyTbq4DPqdCr/Z7eF O03w== X-Received: by 10.205.99.130 with SMTP id cs2mr21484969bkc.118.1367313149693; Tue, 30 Apr 2013 02:12:29 -0700 (PDT) MIME-Version: 1.0 Received: by 10.205.83.144 with HTTP; Tue, 30 Apr 2013 02:11:49 -0700 (PDT) In-Reply-To: <1D6C7417-8F98-4979-B6AF-E8C10CC21F71@math.nagoya-u.ac.jp> 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> <517F6BB9.4070703@frisch.fr> <517F7AA7.1020108@frisch.fr> <1D6C7417-8F98-4979-B6AF-E8C10CC21F71@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Tue, 30 Apr 2013 11:11:49 +0200 Message-ID: To: Jacques Garrigue Cc: Alain Frisch , OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs > The only other thing it does is a slight strengthening of variance checking. > > Consider the type > type 'a t = T (* 'a bi-variant and injective *) > type 'a u = 'a t -> 'a t (* 'a t occurs both at positive and negative positions *) > > Originally, the parameter of u would have been bi-variant (or unrestricted) > since it is bi-variant in the definition of t. > However it is now invariant. > The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping. > This is a reasonable restriction, and it is necessary to allow some GADT > definitions where we use concrete types as indices. I'm not sure about this. In our work on variance of GADTs ( http://arxiv.org/abs/1301.2903 ), we defined equality exactly as the antisymmetric closure of the subtyping relation (as is done in the previous work by Simonet and Pottier), and all type constructors are functional: (a = b) implies (a t = b t). This means that in our formalization, you ('a u = 'a bivar -> 'a bivar) is bivariant, because ('a bivar = 'b bivar) for any 'a and 'b implies (a u = 'a bivar -> 'a bivar = 'b bivar -> 'b bivar = 'b u). This vision of invariance as still functional also plays nicely with the inversion principle: when you have (a t <= b t) when t covariant, you can deduce (a <= b), when t is contravariant you have (a >= b), and we can explain invariance as saying that you then have both, (a <= b) and (b <= a), which coincides with the algorithmic notion of "occurs both negatively and positively". The nice thing is that this inversion criterion is also complete, from (a <= b) and (b <= a) you can deduce (a t <= b t) for t invariant (in our system). What is the reason for adding your strengthening? What I understood so far is that unification, and therefore provable equality/inequalities, were orthogonal to variance (eg. (type 'a t = T) is both bivariant and injective). Is there a reason to tie them back together precisely in the invariant case? On Tue, Apr 30, 2013 at 10:18 AM, Jacques Garrigue wrote: > On 2013/04/30, at 17:02, Alain Frisch wrote: > >> On 04/30/2013 09:56 AM, Jacques Garrigue wrote: >>> On 2013/04/30, at 15:59, Alain Frisch wrote: >>> >>>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying. >>>> >>>> I'm only concerned with: >>>> >>>>> 3) The problem I describe in my first mail. I.e. when defining a type, >>>>> if you use type variables appearing in constrained type parameters, >>>>> you need the type constructors leading to the type variables to be >>>>> injective. This is PR#5985, and it is only fixed in branches/non-vanishing. >>>> >>>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs? >>> >>> Potentially yes. >>> But I don't know how it is in practice for code existing now. >>> Hence my question. >> >> Apart from GADTs, does your patch address the unsoundness with type constraints? > > Sure, this is exactly the same mechanism. > > The only other thing it does is a slight strengthening of variance checking. > > Consider the type > type 'a t = T (* 'a bi-variant and injective *) > type 'a u = 'a t -> 'a t (* 'a t occurs both at positive and negative positions *) > > Originally, the parameter of u would have been bi-variant (or unrestricted) > since it is bi-variant in the definition of t. > However it is now invariant. > The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping. > This is a reasonable restriction, and it is necessary to allow some GADT > definitions where we use concrete types as indices. > > Jacques Garrigue > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs