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 BBDA47EE51 for ; Tue, 30 Apr 2013 10:18:45 +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: AgMFAPB7f1GFBoIFdGdsb2JhbABSwhSBGA4BDBUIPIIfAQEEASccATUCAwsLGBwSVwYTG4d1Ba00gzKBEgKGC4c1B41ofzMHgm5hiROODpRKgWQ X-IPAS-Result: AgMFAPB7f1GFBoIFdGdsb2JhbABSwhSBGA4BDBUIPIIfAQEEASccATUCAwsLGBwSVwYTG4d1Ba00gzKBEgKGC4c1B41ofzMHgm5hiROODpRKgWQ X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="15453935" 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 10:18:44 +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 469656137; Tue, 30 Apr 2013 17:18:43 +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 D2800396F; Tue, 30 Apr 2013 17:18:40 +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 tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id ABD46396A; Tue, 30 Apr 2013 17:18:40 +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: <517F7AA7.1020108@frisch.fr> Date: Tue, 30 Apr 2013 17:18:39 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <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> To: Alain Frisch X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs 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: >>=20 >>> It's reassuring to see that the conservative solution (not assuming inj= ectivity of user defined abstract types) does not seem too bad for now, eve= n if not very satisfying. >>>=20 >>> I'm only concerned with: >>>=20 >>>> 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-van= ishing. >>>=20 >>> Do you think that fixing this unsoundness (without injectivity annotati= ons) would lead to reject existing programs? >>=20 >> Potentially yes. >> But I don't know how it is in practice for code existing now. >> Hence my question. >=20 > Apart from GADTs, does your patch address the unsoundness with type const= raints? 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 =3D T (* 'a bi-variant and injective *) type 'a u =3D 'a t -> 'a t (* 'a t occurs both at positive and negati= ve 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=