Hi, > The first problem is that phantom types must be implemented in terms > of abstract (or at least generative) types. A simple example to > illustrate the problem: the types > > int t > and > float t > > denote the same type given the alias declaration > > type 'a t = unit > > but different types given the abstract type declaration > > type 'a t > > The clause "= private 'a" in your declaration above indicates that `t' > denotes an alias, not an abstract type.
What mislead me was a simple experiment I made where declaring 't' private had the same effect as making it abstract for purposes of creating module values (thus forcing you to constructor functions), while at the same time keeping the 't' open for purposes of pattern-matching. Suppose you have a simple module that prevents the user from mixing the proverbial apples and oranges: module Fruit: sig type 'a t val apples: int -> [`Apples] t val oranges: int -> [`Oranges] t val (+): 'a t -> 'a t -> 'a t end = struct type 'a t = int let apples n = n let oranges n = n let (+) = (+) end open Fruit let foo = apples 10 let bar = oranges 20 let sum = foo + bar (* oops! *) Now, if you un-abstract 't' by declaring "type 'a t = int" in the sig, then the rogue unification makes the compiler accept the erroneous top-level statements. However, if instead you declare it as "type 'a t = private int", then rogue unification is prevented, but the type is not completely hidden. You can thus have your cake and eat it too. (Please correct me if my interpretation of 'private' is off). > Weak (ungeneralised) type variables are not allowed at module-level > bindings. You'll see a similar error message if you try to compile a > module containing the following binding, for example > > let x = ref None > > The solution to this problem is usually to change the form of the > offending expression, for example by eta-expanding a term denoting a > function. In your case, though, the solution is to change the > declaration of the abstract type `t' to indicate that the type > parameters do not occur negatively in the right-hand side. This takes > advantage of a novel feature of OCaml -- the "relaxed value > restriction" -- which uses a subtype-based analysis rather than a > simple syntactic check to determine whether bindings can be made > polymorphic. Thanks for the explanation. The solution I adopted was to use the '+' covariance modifier (is that its name?) *only* for parameter 'a, because parameter 'b should always be "terminated" via a make_basic or make_complex function: (there is no equivalent "termination" function for parameter 'a because I want to allow documents to be composed from other documents adlib). type (+'a, 'b) t constraint 'a = [< super_node_t ] val make_basic: ('a, [< `Basic]) t -> ('a, [`Basic]) t val make_complex: ('a, [< `Basic | `Complex]) t -> ('a, [`Complex]) t Also, I found it is alright to use ungeneralised type variables in intermediate expressions, as long as the final expression generalises it: (this is actually analogous to what happens when you declare "let x = ref None"; it is fine as long as sooner or later you make the type concrete) let doc = let n1 = bold [text "hello"] in (* 'b is weak *) let n2 = mref "ref" [n1] in (* 'b is still weak *) make_complex n2 (* 'b is now concrete *) Cheers, Dario Teixeira __________________________________________________________ Not happy with your email address?. Get the one you really want - millions of new email addresses available now at Yahoo! http://uk.docs.yahoo.com/ymail/new.html _______________________________________________ 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