Jacques Garrigue wrote:
From: Jeremy Yallop <[EMAIL PROTECTED]>
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.
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
