From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 0D283BB84 for ; Fri, 18 Jul 2008 04:34:54 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEALydf0iCNhAB/2dsb2JhbACveQ X-IronPort-AV: E=Sophos;i="4.31,207,1215381600"; d="scan'208";a="27436778" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail4-smtp-sop.national.inria.fr with ESMTP; 18 Jul 2008 04:34:52 +0200 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m6I2YeFb014911; Fri, 18 Jul 2008 11:34:41 +0900 (JST) Date: Fri, 18 Jul 2008 11:34:47 +0900 (JST) Message-Id: <20080718.113447.241468128.garrigue@math.nagoya-u.ac.jp> To: jeremy.yallop@ed.ac.uk Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Troublesome nodes From: Jacques Garrigue In-Reply-To: <487F2609.1080708@ed.ac.uk> References: <487BAB0B.6030000@ed.ac.uk> <20080717.094328.191385811.garrigue@math.nagoya-u.ac.jp> <487F2609.1080708@ed.ac.uk> X-Mailer: Mew version 5.2 on Emacs 22.1 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; nodes:01 node:01 generative:01 datatypes:01 generative:01 abstraction:01 datatypes:01 datatype:01 rhs:01 arbitrarily:01 subtyping:01 abbreviation:01 syntax:01 syntax:01 node:01 From: Jeremy Yallop > Jacques Garrigue wrote: > > From: Jeremy Yallop > >> Dario Teixeira wrote: > >>> type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ] > >> I don't think this is quite what you want yet, although it's getting > >> close! > >> > >> The first problem is that phantom types must be implemented in terms > >> of abstract (or at least generative) types. > > > > This is actually the other way round: abstract and private types allow > > phantom types, but abbreviations and normal datatypes (generative > > ones) don't. > > Thanks for the correction! I haven't yet properly internalized private > rows. It seems that private rows allow phantom types because there is > abstraction (and hence generativity) involved. > > However, it seems to me that normal (generative) datatypes also allow > phantom types. If `t' is a unary generative datatype constructor then > `int t' and `unit t' are not unifiable, even if the type parameter does > not occur on the rhs of the definition of `t'. For example: > > type 'a t = T > let f ((_ : int t) : unit t) = () (* Wrong. *) However let f x = (x : int t :> unit t) (* Ok *) For datatypes, variance is inferred automatically, and if a variable does not occur in the type you are allowed to change it arbitrarily through subtyping. > On a related note, does Dario's declaration above become ambiguous with > the introduction of private type abbreviations? The following program > passes typechecking in 3.10.2, but not in 3.11+dev12, perhaps because > `t' is interpreted as a private type abbreviation rather than as a > private row type. I detailed the change in my answer to his mail. In 3.11 the distinction is syntactic: only explicit variant or object types give rise to private rows. By the way, I forgot to mention that aliases (as keyword) of those were not allowed until now, so I have to fix it to make the syntax for private rows work. (There are useful examples using this syntax.) type ('a, 'b) t = private [< super_node_t ] as 'a Cheers, Jacques Garrigue