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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by yquem.inria.fr (Postfix) with ESMTP id 06F2DBB84
	for <caml-list@yquem.inria.fr>; Fri, 18 Jul 2008 11:47:57 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AiUBADgDgEhTkhUHjWdsb2JhbACSPQEBAQEJBQgYA5xe
X-IronPort-AV: E=Sophos;i="4.31,209,1215381600"; 
   d="scan'208";a="15233692"
Received: from smtp.bulldogdsl.com (HELO cht-smtp-001.bulldogdsl.com) ([83.146.21.7])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 18 Jul 2008 11:47:57 +0200
Received: by cht-smtp-001.bulldogdsl.com (Postfix, from userid 1011)
	id CBDEB4E6BF7; Fri, 18 Jul 2008 10:47:56 +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 DD0714E6BCD;
	Fri, 18 Jul 2008 10:47:53 +0100 (BST)
Message-ID: <488066C9.4050904@ed.ac.uk>
Date: Fri, 18 Jul 2008 10:47:53 +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: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Troublesome nodes
References: <487BAB0B.6030000@ed.ac.uk>	<20080717.094328.191385811.garrigue@math.nagoya-u.ac.jp>	<487F2609.1080708@ed.ac.uk> <20080718.113447.241468128.garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <20080718.113447.241468128.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 generative:01 datatypes:01 generative:01 datatype:01 rhs:01 datatypes:01 arbitrarily:01 subtyping:01 nat:01 sig:01 val:01 val:01 struct:01 nat:01 

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

Thanks for the explanation.  I agree that this means that datatypes are 
not useful for phantom types.

I don't yet understand exactly how private abbreviations are supposed to 
work.  The currently implemented behaviour doesn't accomplish what I 
understand to be the intention.  For example, given

    module Nat :
    sig
      type t = private int
      val z : t
      val s : t -> t
    end =
    struct
      type t = int
      let z = 0
      let s = (+) 1
    end

we can write

    # (((Nat.z : Nat.t :> int) - 1) :> Nat.t);;
    - : Nat.t = -1

Similarly, I'm surprised by the behaviour of coercions at parameterised 
types.  Given a private type

      type 'a t = private 'a

should we be able to coerce a value of type 'a t to type 'a?

Jeremy.