From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <jeremy.yallop@ed.ac.uk>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled 
	version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by yquem.inria.fr (Postfix) with ESMTP id 83AF9BB84
	for <caml-list@yquem.inria.fr>; Thu, 17 Jul 2008 12:59:26 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AlQAAEvDfkhTkhUHmmdsb2JhbACBWZBtAQEBAQkFCAcRA50k
X-IronPort-AV: E=Sophos;i="4.31,203,1215381600"; 
   d="scan'208";a="13197655"
Received: from smtp.dslgb.com (HELO cht-smtp-001.bulldogdsl.com) ([83.146.21.7])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 17 Jul 2008 12:59:26 +0200
Received: by cht-smtp-001.bulldogdsl.com (Postfix, from userid 1011)
	id 7C81F4E5BEB; Thu, 17 Jul 2008 11:59:25 +0100 (BST)
Received: from [192.168.123.191] (host-84-9-232-55.dslgb.com [84.9.232.55])
	by cht-smtp-001.bulldogdsl.com (Postfix) with ESMTP id 99FD54E5AE8;
	Thu, 17 Jul 2008 11:59:22 +0100 (BST)
Message-ID: <487F2609.1080708@ed.ac.uk>
Date: Thu, 17 Jul 2008 11:59:21 +0100
From: Jeremy Yallop <jeremy.yallop@ed.ac.uk>
User-Agent: Mozilla-Thunderbird 2.0.0.14 (X11/20080509)
MIME-Version: 1.0
To: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Cc: darioteixeira@yahoo.com, caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Troublesome nodes
References: <831.74975.qm@web54604.mail.re2.yahoo.com>	<487BAB0B.6030000@ed.ac.uk> <20080717.094328.191385811.garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <20080717.094328.191385811.garrigue@math.nagoya-u.ac.jp>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
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 abbreviation:01 node:01 sig:01 struct:01 wrote:01 wrote:01 

Jacques Garrigue wrote:
> From: Jeremy Yallop <jeremy.yallop@ed.ac.uk>
>> 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. *)

> So the above code really defines a phantom type.

Yes.

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.

type super_node_t = [`S]

module M :
sig
   type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
end =
struct
   type super_node_t = [`S]
   type ('a, 'b) t = 'a constraint 'a = [< super_node_t ]
end

let f x = (x : [<super_node_t] :> ([< super_node_t], _) M.t)

Jeremy.