[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2008-07-18 (09:47) |
From: | Jeremy Yallop <jeremy.yallop@e...> |
Subject: | Re: [Caml-list] Troublesome nodes |
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.