Troublesome nodes
[
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:   (:) 
From:  Jeremy Yallop <jeremy.yallop@e...> 
Subject:  Re: [Camllist] 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.