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 09A087EE51 for ; Tue, 30 Apr 2013 15:06:56 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.133; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.133; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-33.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.133; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-33.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Au8CAFnBf1GDbwiFlGdsb2JhbABSwhSBARYOAQEBAQcNCQkUBSOCHwEBAQMBJxM/EAshJQ8BBEmIIwaxXIcqhxSPGgeDTwOrWg X-IPAS-Result: Au8CAFnBf1GDbwiFlGdsb2JhbABSwhSBARYOAQEBAQcNCQkUBSOCHwEBAQMBJxM/EAshJQ8BBEmIIwaxXIcqhxSPGgeDTwOrWg X-IronPort-AV: E=Sophos;i="4.87,582,1363129200"; d="scan'208";a="12756297" Received: from ppsw-33.csi.cam.ac.uk ([131.111.8.133]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Apr 2013 15:06:55 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from kingston.cl.cam.ac.uk ([128.232.64.15]:52689) by ppsw-33.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.157]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1UXAGk-0007M2-i8 (Exim 4.80_167-5a66dd3) (return-path ); Tue, 30 Apr 2013 14:06:54 +0100 From: Leo White To: Gabriel Scherer Cc: Jacques Garrigue , OCaML List Mailing 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> <8738u8ba3j.fsf@kingston.cl.cam.ac.uk> Date: Tue, 30 Apr 2013 14:06:54 +0100 In-Reply-To: (Gabriel Scherer's message of "Tue, 30 Apr 2013 13:30:49 +0200") Message-ID: <87vc749ngx.fsf@kingston.cl.cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs >>> type 'a t = T;; >>> type _ g = G : 'a -> 'a t g;; >> >> 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 covariant). > > 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) 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. 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. This second reason also occurs in types with constraints, for example: type 'a s = 'b constraint 'a = 'b t 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.