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 93E167EE51 for ; Tue, 30 Apr 2013 12:12:49 +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: AvACABuYf1GDbwiFlGdsb2JhbABSDsIGgQIWDgEBAQEHDQkJFAUjgh8BAQEDAScTOAcFCwshJQ8BBEkuh3UGsRqHI4c8jxoHg08DqxpA X-IPAS-Result: AvACABuYf1GDbwiFlGdsb2JhbABSDsIGgQIWDgEBAQEHDQkJFAUjgh8BAQEDAScTOAcFCwshJQ8BBEkuh3UGsRqHI4c8jxoHg08DqxpA X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="12733435" Received: from ppsw-33.csi.cam.ac.uk ([131.111.8.133]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 Apr 2013 12:12:49 +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]:52542) 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 1UX7YG-0006xH-hJ (Exim 4.80_167-5a66dd3) (return-path ); Tue, 30 Apr 2013 11:12:48 +0100 From: Leo White To: Jacques Garrigue Cc: Gabriel Scherer , 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> Date: Tue, 30 Apr 2013 11:12:48 +0100 In-Reply-To: (Jacques Garrigue's message of "Tue, 30 Apr 2013 18:55:07 +0900") Message-ID: <8738u8ba3j.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 [Sorry if this is a repeat post] > But it seems to me that this contradicts the definition of injectivity. > Namely, if we follow your definition, and have 'a bivar = 'b bivar, then > clearly bivar is not injective. I think Gabriel meant that 'a bivar = 'b bivar were equal in the subtyiping relationship, rather than in the unification relationship. (Perhaps we should use a different symbol for subtyping equality). > 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. I don't see how this implies the need for the strengthening you describe. As I see it: type 'a t = T creates a type that is bi-variant in its parameter, so all occurences of 'a in: type 'a u = 'a t -> 'a t are in bi-variant positions, so u should also be bi-variant. > 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 = T;; > type _ g = 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. 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).