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 q1B1pebd021396 for ; Sat, 11 Feb 2012 02:51:40 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAKLINU+FBoIF/2dsb2JhbABDhRSrZoFyAQEEASMEGQMBNQEBAwsJAhoCGA4CAlcGiA+oFm2DQYY4AQaBL4oGCCwFCgYFAgQHAh0BAwcBARKDLAVCDIJ7M2OIS4xpknM X-IronPort-AV: E=Sophos;i="4.73,399,1325458800"; d="scan'208";a="143797531" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 11 Feb 2012 02:51:33 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B335A62B0; Sat, 11 Feb 2012 10:51:32 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4A0C53A13; Sat, 11 Feb 2012 10:51:32 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=I7zXhK6ft3FRBhtysqfF+dZlB1g=; b=GfjduJGWAUKlndDfbboyxmcAtGVa IDEd1NF+BZZ96N6PyJtQPBmUYF/EPim09q0NaaX0lHebRgBUcm3/UmwSv6RTHE7j To2YZAXxHLvS4bAvhv7jSSItUUQy28txoTztnrDvHtcMsAn4nfuA22DgcCM76hLn eQjSOv+LJfPI02Y= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=UPeVkPmnFYjXGTuWeNNX5Nh8QyMBm6uTUn/Z/jcA0MASoYkzbfs8Yk1MqNm3SdXwYHtfP/NW5gV8KP+VXM6v8cJNp74R8CrPEevJsdCsu4mWSQmhCeeC86PWmINs3pt6mohZWpUowMo6oT1xJ2Vglo97mys++svhZnCgmoBpfZk=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; 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 F334639A3; Sat, 11 Feb 2012 10:51:31 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Sat, 11 Feb 2012 10:51:31 +0900 Cc: caml users Message-Id: <6A006A62-F9C0-4A90-90E5-B2EFD0177E88@math.nagoya-u.ac.jp> References: To: Gabriel Scherer X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1B1pebd021396 Subject: [Caml-list] Re: Variance of GADT parameters 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