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 2EF247EE51 for ; Tue, 30 Apr 2013 11:55:14 +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: AgUFALCTf1GFBoIFdGdsb2JhbABSgz2+V4EYDgEMFQg8gh8BAQQBJxwBLgcCAwsLNBIhNgYTG4dpAwkFrVyDMoESAoUzDUyHNQeMRIIjMweCbmGJE4wqgWSBJopliD8 X-IPAS-Result: AgUFALCTf1GFBoIFdGdsb2JhbABSgz2+V4EYDgEMFQg8gh8BAQQBJxwBLgcCAwsLNBIhNgYTG4dpAwkFrVyDMoESAoUzDUyHNQeMRIIjMweCbmGJE4wqgWSBJopliD8 X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="15475115" 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; 30 Apr 2013 11:55:11 +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 5E29C6297; Tue, 30 Apr 2013 18:55:09 +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 C2842394C; Tue, 30 Apr 2013 18:55:08 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject: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 tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 6E6A72564; Tue, 30 Apr 2013 18:55:08 +0900 (JST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: Date: Tue, 30 Apr 2013 18:55:07 +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> <517F6BB9.4070703@frisch.fr> <517F7AA7.1020108@frisch.fr> <1D6C7417-8F98-4979-B6AF-E8C10CC21F71@math.nagoya-u.ac.jp> To: Gabriel Scherer X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/04/30, at 18:11, Gabriel Scherer wrote: >> The only other thing it does is a slight strengthening of variance check= ing. >>=20 >> Consider the type >> type 'a t =3D T (* 'a bi-variant and injective *) >> type 'a u =3D 'a t -> 'a t (* 'a t occurs both at positive and nega= tive positions *) >>=20 >> Originally, the parameter of u would have been bi-variant (or unrestrict= ed) >> 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. >=20 > 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 =3D b) implies (a t =3D b t). This means that in our > formalization, you ('a u =3D 'a bivar -> 'a bivar) is bivariant, because > ('a bivar =3D 'b bivar) for any 'a and 'b implies (a u =3D 'a bivar -> 'a > bivar =3D 'b bivar -> 'b bivar =3D 'b u). >=20 > This vision of invariance as still functional also plays nicely with > the inversion principle: when you have (a t <=3D b t) when t covariant, > you can deduce (a <=3D b), when t is contravariant you have (a >=3D b), > and we can explain invariance as saying that you then have both, (a <=3D > b) and (b <=3D 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 <=3D b) and (b <=3D a) you > can deduce (a t <=3D b t) for t invariant (in our system). But it seems to me that this contradicts the definition of injectivity. Namely, if we follow your definition, and have 'a bivar =3D 'b bivar, then clearly bivar is not injective. So there are two solutions: either we do not allow a bi-variant type to be injective (breaking our simple statement that concrete types are injective in all their parameters), or we consider bi-variance + injectivity is some intermediary state, where we can use both directions of subtyping, but not strong (unification) equality. > 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 =3D T) is both bivariant and > injective). Is there a reason to tie them back together precisely in > the invariant case? The theoretical reason is above. The practical reason is to make easier to define indices. If we keep the bi-variance in an invariant context, then the following type definition is refused: type 'a t =3D T;; type _ g =3D G : 'a -> 'a t g;; In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but= 'a appears in a covariant position. Jacques Garrigue=