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 q1DAO8Zp031357 for ; Mon, 13 Feb 2012 11:24:08 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAF3kOE+FBoIF/2dsb2JhbABDhRCrc4FyAQEEASMEGQMBNQEBAwsJAhoCGA4CAlcGiA+mVm2DQY1fAQaBL4pFCwcDBQIEBwIdAQMHAQESgywFQgyCezNjiEyMapJz X-IronPort-AV: E=Sophos;i="4.73,411,1325458800"; d="scan'208";a="143985616" 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; 13 Feb 2012 11:24:02 +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 53A986291; Mon, 13 Feb 2012 19:24:00 +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 1126540C1; Mon, 13 Feb 2012 19:24:00 +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=j/YNJrqY19Ah6UIEVa7Se+Gs4os=; b=0DS9wmmvchJhiBugHGhuQDEWV86l Xo32hfyzGAAgb+fM14hBQ7TYf7zOSwkOVmxRkNpN6ifx7idue7D/AF42Tn2M/7w4 /AThY4qifTRj7tTyGP9IruMQX31sbUBYxPw9DcAxVvQlAZBok9nT+WVqZRhEdrht C25KbRfZa6zlTrk= 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=gUqdJQaNoqHuf7Jwb3eGmnJqgMTtxwjhhAI4WPoGjmJ4tH9THHxqmdBJWL05zd4DRXmdqH1FraZo2/5vb3jy2npkhrMJylijoXk1QH7Tr7UpuPaxI5S7suroZDhtv7MGyoh+WdIharUc/ZDbQYs9NyhlUmOxonxaGA/lzvVpk1o=; 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 A8F153A13; Mon, 13 Feb 2012 19:23:59 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Mon, 13 Feb 2012 19:23:58 +0900 Cc: caml users Message-Id: References: <6A006A62-F9C0-4A90-90E5-B2EFD0177E88@math.nagoya-u.ac.jp> 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 q1DAO8Zp031357 Subject: [Caml-list] Re: Variance of GADT parameters On 2012/02/13, at 2:36, Gabriel Scherer wrote: > 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 β≤β', γ≤γ' > > 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'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? The proof looks fine. Subtyping in OCaml has not been much studied. You can find a short draft attempting to specify the current behavior on my publication page. Again I wonder whether you are not going to get problems with abstraction. At first sight, no: if when you define a GADT t, the type u is abstract, then it will have no supertype in any environment where we use t. But if you think more carefully, you realize that if in the future we allow (gadt-)unification between abstract types, everything breaks, since abstract types may end up having supertypes in a local environment. So it looks like the only types you can allow for instantiation are concrete datatypes and well-known types (abstract types defined in the initial environment or in the current module). Jacques Garrigue