From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA20165; Wed, 3 Oct 2001 16:17:51 +0200 (MET DST)
X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA20161 for <caml-list@pauillac.inria.fr>; Wed, 3 Oct 2001 16:17:50 +0200 (MET DST)
Received: from favie.faith.gr.jp (favie.faith.gr.jp [61.127.175.250])
	by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f93EHmf03298
	for <caml-list@inria.fr>; Wed, 3 Oct 2001 16:17:48 +0200 (MET DST)
Received: from localhost (dhcp7.faith.gr.jp [192.168.1.17])
	by favie.faith.gr.jp (8.9.3/8.9.3) with ESMTP id XAA05403;
	Wed, 3 Oct 2001 23:17:29 +0900
To: david.chemouil@irit.fr
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] phantom types and coercions
In-Reply-To: <3BBAD886.3CCB5AC4@irit.fr>
References: <3BBAD886.3CCB5AC4@irit.fr>
X-Mailer: Mew version 1.94.2 on Emacs 20.7 / Mule 4.0 (HANANOEN)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Message-Id: <20011003231753S.garrigue@kurims.kyoto-u.ac.jp>
Date: Wed, 03 Oct 2001 23:17:53 +0900
From: Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>
X-Dispatcher: imput version 20000228(IM140)
Sender: owner-caml-list@pauillac.inria.fr
Precedence: bulk

From: David Chemouil <david.chemouil@irit.fr>

> we have noticed a strange (at least to us) behavior of the coercion
> operator over phantom types.
> 
> Here is an example:
> 
> # type n = [`Pos];;   (* non-negative number *)
> type n = [ `Pos]
> # type z = [`Neg | `Pos];;   (* integer *)
> type z = [ `Neg | `Pos]
> # type (+'ph) expr = Expr of int;;  (* phantom type *)
> type 'a expr = Expr of int

The problem is that this is not a phantom type. To be more precise, in
ocaml only abstract types behave as phantom types. Citing the
reference manual:

  The variance indicated by the + and - annotations on parameters are
  required only for abstract types. For abbreviations, variant types or
  record types, the variance properties of the type constructor are
  inferred from its definition, and the variance annotations are only
  checked for conformance with the definition.

You can see that the "+" does not appear in the output of the
compiler. In fact 'ph is "anyvariant", since it does not appear in the
type itself.

This behaviour is natural, since you would be able to fool the
compiler by matching Expr, and building a new one.

On the other hand, you can build a small ADT to get a real phantom
type.

module Expr : sig
  type +'a expr
  val pos_expr : int -> [`Pos] expr
  val neg_expr : int -> [`Neg] expr
  val add : 'a expr -> 'a expr -> 'a expr
  val get : 'a expr -> int
end = struct
  type 'a expr = int
  let pos_expr n = if n < 0 then invalid_arg "pos_expr"; n
  let neg_expr n = if n > 0 then invalid_arg "neg_expr"; n
  let add n1 n2 = n1 + n2
  let get n = n
end

Hope this helps,

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr