From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1CHakKk030277 for ; Sun, 12 Feb 2012 18:36:46 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkMBAKP3N09KfVK2kGdsb2JhbABDDoUCql0IIgEBAQEJCQ0HFAQjgXIBAQEEEgIPBBkBGx0BAwwGAwILDQICJgICIgERAQUBHAYTCBqjLwqLJkuCcINrP4hzAgULgSSKEQgsBQoDAwUCBAMECgECBwUGAQMGAgEBhwuBFgSVMo4lPYNLOA X-IronPort-AV: E=Sophos;i="4.73,408,1325458800"; d="scan'208";a="143911866" Received: from mail-we0-f182.google.com ([74.125.82.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 12 Feb 2012 18:36:41 +0100 Received: by werm13 with SMTP id m13so5122032wer.27 for ; Sun, 12 Feb 2012 09:36:41 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=urTcZezUaNV3t96S34IyyTexp9Dw7GF3W2yPweEbTBU=; b=AVcbkgUbKhXnOqIKh1pu0hu638ZjDhPZ81FrsKssIOepXDJ3CKYHAW0++8PN3GlZTK kXVudqiAHU/lNUHd+fupFh7sdth+ciYTQKWTqOgPYwnRbVmbefNVv0KElyrJWkYJWVuS LYVwc+K967+mQVrYR4dxcnWJ/xY+SNJCtBnQQ= Received: by 10.180.85.105 with SMTP id g9mr13875491wiz.12.1329068201261; Sun, 12 Feb 2012 09:36:41 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.61.7 with HTTP; Sun, 12 Feb 2012 09:36:01 -0800 (PST) In-Reply-To: <6A006A62-F9C0-4A90-90E5-B2EFD0177E88@math.nagoya-u.ac.jp> References: <6A006A62-F9C0-4A90-90E5-B2EFD0177E88@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Sun, 12 Feb 2012 18:36:01 +0100 Message-ID: To: Jacques Garrigue Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1CHakKk030277 Subject: [Caml-list] Re: Variance of GADT parameters Thank you, Jacques and Jeremy, for the examples. Indeed that looks quite subtle. I found it helpful to write an informal proof of covariance of the following type: type +_ expr = | Val : 'a -> 'a expr | Prod : 'a expr * 'b expr -> ('a * 'b) expr Or, in a more explicit formulation using imaginary syntax with explicit existential variables and equalities. type +'a expr = | Val of 'b . 'b with ('a = 'b) | Prod of 'b 'c. 'b expr * 'c expr with ('a = 'b * 'c) The informal proof goes as follow: assuming α ≤ α', we wish to show that α expr ≤ β expr. For a given (t : α expr): - if (t) is (Val (v : α)), then by α ≤ α' we have (v : α') so (Val v : α' expr) - if (t) is Prod((t1 : β expr), (t2 : γ expr)), with (α = β * γ), then we have (β * γ ≤ α'). *By inversion* we know that there must exist β', γ' with α' = β' * γ', β ≤ β' and γ ≤ γ'. We therefore have (t1 : β' expr), (t2 : γ' expr), and therefore (Prod(t1,t2) : α' expr) The core of the proof is an inversion lemma for subtyping at product types: if β*γ ≤ α' then α' is of the form β'*γ' with β≤β', γ≤γ' I believe this is true of OCaml product types, and can be generalized to some other OCaml types. It would not be true if we had a top type, and it would be unsafe to coerce (Prod (t1, t2)) into (⊤ expr) – this is clear if we remove the Val case: if expr only had a Prod case, one could write a function (⊤ expr → ⊥), with no case at all, that would be accepted by the type-checker as ⊤ and ∃βγ.β*γ do not overlap. The strength of the inversion lemma depends a lot on the details of the theory. For example, if α = int and α ≤ α', do we have α' = int? And if α ≥ α'? I believe the answer to the α ≤ α' case is "yes", which would make the (type +_ expr = Const : int -> int expr) case correctly covariant, but as Jacques showed the answer is no in the contravariant case α ≥ α', we have (int ≥≠ private int). I think this technique of inversion can be generalized to arbitrary GADT constructors type (α₁,α₂..αm) t = ... | C of ∃β₁β₂...βn. σ with (α₁ = τ₁, α₂ = τ₂... αm = τm) I'm under the impression that they give something that looks a bit like my previous conditions, with additional restrictions – eg. restricted to types where suitable inversion principles apply. In particular, existential variables of the instances of the parameters (that is, the set of βi that appear in each τj) must not overlap – this rules out the (('a,+'a) eq) example of Jeremy. I'm going to think a bit more about this. What do you think of the "proof" in the Prod case? Is there such an inversion principle for the OCaml type theory? On Sat, Feb 11, 2012 at 2:51 AM, Jacques Garrigue wrote: > On 2012/02/10, at 19:11, Gabriel Scherer wrote: > >> I've been playing with GADTs and noticed that the condition on >> parameter variance is very restrictive. >> >> The two following examples fail: >> >>   type +_ const = >>   | Const : int -> int expr >> >>   type +_ expr = >>   | Const : 'a -> 'a expr >>   | Prod : 'a expr * 'b expr -> ('a * 'b) expr >> >>   Error: In this GADT definition, the variance of some parameter >>   cannot be checked >> >> I looked at the source, and this is what I could infer of the current >> typer behavior: parameter variance check will fail (on non-invariant >> parameters) as soon as they appear *instantiated* (not just >> a variable) in one of the GADT branch return type. The two examples >> above fail for this reason: `const` parameter is instantiated with int >> and `expr` with ('a * 'b). >> >> Would it be possible to relax this condition a bit? Intuitively, I >> would say that: >> 1. variables that do not appear in the instantiations of the return >>   type always satisfy their variance constraint (for the branch) >> 2. variables that appear covariantly in the instantiations of the >>   return type should satisfy their constraints on the argument types >> 3. variables that appaear contravariantly should satisfy the >>   *reversed* constraints on the argument type >> >> For example, with a GADT having some argument type σ('a) using >> a variable instantiated in its return type : >> >>   type +_ t = | C : σ('a) -> ('a -> unit) t >> >> If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' → >> unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a >> appears *contravariantly* in σ. >> >> Is the above condition sound? It would allow my two examples above. If >> not, or if it's not reasonable to implement, is there a weaker >> condition that would make those example work? >> >> Having a powerful enough variance inference is important if we want to >> use GADTs to implement abstract data types – that's how I ran into >> this problem. > > As Jeremy pointed already, the question of variance in presence of GADTs > is devilishly complicated. > Your conditions are much too simple to be sufficient. > They seem to be the conditions we already have for constrained types. > > I'm ready to buy anything, but at least I need a proof of soundness. > > At the very least, the conditions seem to be > 1) an instantiated type cannot include type variables that appear elsewhere in the return type >     (Jeremy's example) > 2) if an instantiated type is marked as contravariant, it should not be possible to smuggle >     a value of this type through the arguments >     (the example in the ocamlgadt tutorial) > 3) something similar for the contravariant case > > However this is completely unclear whether this would be sufficient. > > For your first example, the contravariant version is clearly unsound: > > type pint = private int > type -_ const = Const : int -> int const > > let eval : type a. a t -> a = fun (Const c) -> c > let make_pint (x : int) : pint = eval (Const x :> pint const) > > I think that your examples are ok, but I'm not sure how to generalize that. > >        Jacques Garrigue >