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 8C3227EE51 for ; Tue, 30 Apr 2013 13:31:35 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.52 as permitted sender) identity=mailfrom; client-ip=209.85.214.52; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f52.google.com) identity=helo; client-ip=209.85.214.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f52.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai0DAC2rf1HRVdY0k2dsb2JhbABSDsIGeggWDgEBAQEHCwsJFAQkgh8BAQQBJxkBGxYHAQMMBgULAwouIgERAQUBHAYTCBOHaAEDCQajHIwxgXGBDIR2ChknDVmHKQEFDI8OB4NPA5cej0UWKYN4QTo X-IPAS-Result: Ai0DAC2rf1HRVdY0k2dsb2JhbABSDsIGeggWDgEBAQEHCwsJFAQkgh8BAQQBJxkBGxYHAQMMBgULAwouIgERAQUBHAYTCBOHaAEDCQajHIwxgXGBDIR2ChknDVmHKQEFDI8OB4NPA5cej0UWKYN4QTo X-IronPort-AV: E=Sophos;i="4.87,580,1363129200"; d="scan'208";a="15490948" Received: from mail-bk0-f52.google.com ([209.85.214.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 30 Apr 2013 13:31:30 +0200 Received: by mail-bk0-f52.google.com with SMTP id je9so177470bkc.39 for ; Tue, 30 Apr 2013 04:31:30 -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=q/c0dE2Wg2d0uXkpZpCQbxdVBMJVm0Y8ia71PRtcgaY=; b=V1NM1T1RUCWkzKq1s5Eer9iMVqHUX14cKHCKKK+8HgSn18VsDThPFiqzmLfIVTTTQI /swdDtq5YFbrb0rGGbtj/DZYkFzzDB/4EFv59J3KOh5kqKkBnXRF+OnR3tIcSCUGvohx ByaeXX6GGL7kocOk8B0z2wmtPtsFUQTNqA6rbb8403EFXvTaxbkkHvzuLNReR3FHjnny wBmCBc/+uCcVlx9Pueno6Gf+Batig+J46v7wRwwRUTgkS6S+bucVmzX2SRZVkYFVMFF7 sbyLSnWZ9RFBIvoZmbgxWDgqcNrPqaYRtxwq4RYllzPQyu/syJTJ1NLmkLgZIV3FPixx kYBw== X-Received: by 10.204.74.138 with SMTP id u10mr2747491bkj.113.1367321489992; Tue, 30 Apr 2013 04:31:29 -0700 (PDT) MIME-Version: 1.0 Received: by 10.205.83.144 with HTTP; Tue, 30 Apr 2013 04:30:49 -0700 (PDT) In-Reply-To: <8738u8ba3j.fsf@kingston.cl.cam.ac.uk> 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> From: Gabriel Scherer Date: Tue, 30 Apr 2013 13:30:49 +0200 Message-ID: To: Leo White Cc: Jacques Garrigue , OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs Indeed, the (=) in my message above where in the context of the work where it is define as ((<=) and (>=)), so in a sense "equality in the sense of subtyping rather than unification". Sorry for the confusion. I'll now mark this relation as <=>. >> 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). 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) In particular, the following does not type-check: let extract : int t g -> int = function | G n -> n The G constructor at type ('b t) has type (exists 'a ['a t <=> 'b]. 'a); so in the G branch the type-checker introduces the hypothesis ('a t <=> int t) for an existential variable 'a. This does not allows to deduce ('a <=> int) and therefore the body does not type-check. However, in the OCaml type system, GADT type equalities are understood in the unification sense (because it is the one that mixes well with the inference engine), so the constructor G at type ('b g) would have type (exists 'a. ['a t = 'b]), with (=) in the unification sense. As Jacques said, this means that we must either reject the definition of ('b g) as is currently done, or stop considering ('a t) injective. PS: Note that you could understand type parameter constraints in the same way, which makes them safe without requiring injectivity, but Didier remarked that this will only delay failure as code writers generally assume injectivity. It's before to fail at definition site than at usage site if you know you should fail anyway. On Tue, Apr 30, 2013 at 12:12 PM, Leo White wrote: > [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).