[Caml-list] phantom types and coercions

[Caml-list] phantom types and coercions

[David Chemouil]

Hello,



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

# let x = ((Expr 1) : n expr);;
val x : n expr = Expr 1
# (x:> z expr);;          (* okay *)
- : z expr = Expr 1
# let y  = ((Expr 1) : z expr);;  
val y : z expr = Expr 1
# (y :> n expr);;        (* ??? *)
- : n expr = Expr 1

So, we observe the same behavior whatever the variance specification is.


# type 'ph expr = Expr of int;;  (* without variance *)
type 'a expr = Expr of int
# let x = ((Expr 1) : n expr);;
val x : n expr = Expr 1
# (x:> z expr);;      (* ??? *)
- : z expr = Expr 1
# let y  = ((Expr 1) : z expr);;
val y : z expr = Expr 1
# (y :> n expr);;       (* ??? *)
- : n expr = Expr 1

# type (-'ph) expr = Expr of int;;  (* contravariance *)
type 'a expr = Expr of int
# let x = ((Expr 1) : n expr);;
val x : n expr = Expr 1
# (x:> z expr);;
- : z expr = Expr 1
# let y  = ((Expr 1) : z expr);;
val y : z expr = Expr 1
# (y :> n expr);;
- : n expr = Expr 1


We wonder whether it is a bug or not (anyway, this is rather
counter-intuitive)...?

dc


-- David Chemouil    [mailto:david.chemouil@irit.fr]
--
-- Zeno group              [http://www.irit.fr/zeno]
-- Institut de recherche en informatique de Toulouse
-------------------
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

Re: [Caml-list] phantom types and coercions

[Jacques Garrigue]

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