This problem was originally raised in a thread in the ocaml-beginners list [1], but since polymorphic variants, covariant constraints, and recursive knots were brought into the discussion, I reckon it deserves the attention of some heavy weights. Moreover, the problem is trickier than first appearances suggest.
So, what's the situation? I want to create a data structure holding document nodes. There are four different kinds of nodes, two of which are terminals (Text and See), and two of which are defined recursively (Bold and Mref). Moreover, both See and Mref produce links, and there is an additional constraint that a link node may *not* be the immediate ancestor of another link node. Using conventional union types, a node could be modelled like this:
module Old_node = struct type seq_t = super_node_t list and super_node_t = | Nonlink_node of nonlink_node_t | Link_node of link_node_t and nonlink_node_t = | Text of string | Bold of seq_t and link_node_t = | Mref of string * nonlink_node_t list | See of string end
The problem with this representation is that it introduces an unwanted scaffolding for nodes. Moreover, it prevents the use of constructor functions for nodes, since non-link nodes may be represented in the tree in a context-dependent fashion: either directly such as Bold [...], or as Nonlink_node (Bold [...]). Note that preserving the link/nonlink distinction in the structure is helpful for pattern matching purposes, but the extra scaffolding is just a pain.
One alternative is to use polymorphic variants, and to take advantage of the fact that new types can be built as the union of existing ones. Ideally, one could do something like this:
type seq_t = super_node_t list and nonlink_node_t = [ `Text of string | `Bold of seq_t ] and link_node_t = [ Mref of string * nonlink_node_t list | See of string ] and super_node_t = [nonlink_node_t | link_node_t]
However, this fails with an error "The type constructor nonlink_node_t is not yet completely defined". Jon Harrop suggested untying the recursive knot, but the solution has a few drawbacks of its own [2].
Another alternative is to flatten the structure altogether and to annotate the constructor functions with phantom types to prevent the violation of the no-parent constraint:
module Node: sig type seq_t = node_t list and node_t = private | Text of string | Bold of seq_t | Mref of string * seq_t | See of string
type +'a t
val text: string -> [> `Nonlink] t val bold: 'a t list -> [> `Nonlink] t val mref: string -> [< `Nonlink] t list -> [> `Link] t val see: string -> [> `Link] t end = struct type seq_t = node_t list and node_t = | Text of string | Bold of seq_t | Mref of string * seq_t | See of string
type +'a t = node_t
let text txt = Text txt let bold inl = Bold inl let mref ref inl = Mref (ref, inl) let see ref = See ref end
This works fine, but because the link/nonlink distinction is lost, making even a simple Node_to_Node translator becomes a mess:
and convert_super_node node = match node with | Node.Text _ | Node.Bold _ -> (convert_nonlink_node node :> [`Link | `Nonlink] Node.t) | Node.See _ | Node.Mref _ -> convert_link_node node end
So, I am looking for a solution that meets the following conditions:
- It satisfies the "no link node shall be parent of another" constraint; - the structure should be pattern-matchable; - but nodes should be created via constructor functions.
Any ideas?
Thanks in advance and sorry for the long post! 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
Dario Teixeira wrote: > Ideally, one could do something like this:
> type seq_t = super_node_t list > and nonlink_node_t = > [ `Text of string > | `Bold of seq_t ] > and link_node_t = > [ Mref of string * nonlink_node_t list > | See of string ] > and super_node_t = [nonlink_node_t | link_node_t]
> However, this fails with an error "The type constructor nonlink_node_t is > not yet completely defined".
Here's a slight variation of this scheme that might suit your needs. The idea is to move the recursion from the type level to the module level, sidestepping the restriction that you can't extend types in the same recursive group.
module rec M : sig type seq_t = M.super_node_t list type nonlink_node_t = [ `Text of string | `Bold of seq_t ] type link_node_t = [ `Mref of string * nonlink_node_t list | `See of string ] type super_node_t = [ nonlink_node_t | link_node_t ] end = M
Dario Teixeira wrote: > Ideally, one could do something like this:
> type seq_t = super_node_t list > and nonlink_node_t = > [ `Text of string > | `Bold of seq_t ] > and link_node_t = > [ Mref of string * nonlink_node_t list > | See of string ] > and super_node_t = [nonlink_node_t | link_node_t]
> However, this fails with an error "The type constructor nonlink_node_t is > not yet completely defined". Jon Harrop suggested untying the recursive > knot, but the solution has a few drawbacks of its own [2].
How about just define
type seq_t = super_node_t list and nonlink_node_t = [ `Text of string | `Bold of seq_t ] and link_node_t = [ `Mref of string * nonlink_node_t list | `See of string ] and super_node_t = [`Test of string |`Bold of seq_t | `Mref of string * nonlink_node_t list | `See of string]
or similar ... not sure whether this satisfies your requirements though.
Thanks Jeremy, that's quite ingenious. However, I've hit a problem in the definition of the constructor functions (the full code + compiler error is below). Now, I know that nonlink_node_t is a subset of super_node_t, and therefore any variant valid for nonlink_node_t is also acceptable for super_node_t. But how do I tell this to the compiler? (Note that having users of the module manually casting types with :> is something I would rather avoid).
Thanks again, Dario
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
val text: string -> nonlink_node_t val bold: super_node_t list -> nonlink_node_t val see: string -> link_node_t val mref: string -> nonlink_node_t list -> link_node_t end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
let text txt = `Text txt let bold seq = `Bold seq let see ref = `See ref let mref ref seq = `Mref (ref, seq) end
open Node let foo = text "foo" let bar = bold [text "bar"]
Error: This expression has type Node.nonlink_node_t but is here used with type Node.super_node_t The first variant type does not allow tag(s) `Mref, `See
__________________________________________________________ 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
The ingenious use of a recursive module signature seems to be the source of the problem here. If one defines 'bar' inside the module Node, it works fine [but is clearly useless].
What surprises me is that the code (below) also gives the exact same error. In other contexts, I have managed to get such annotations (see the definition of the bold function) to 'work', but not here. I am quite puzzled by this, so if you do get an answer to your question offl-ist, I would appreciate if you could forward it on.
Jacques
PS: because I am actually using metaocaml for other projects, I am using ocaml 3.09 for my tests, so it is possible that something is different in 3.10.
module Node : sig type nonlink_node_t type link_node_t type super_node_t
val text: string -> nonlink_node_t val bold: super_node_t list -> nonlink_node_t val see: string -> link_node_t val mref: string -> nonlink_node_t list -> link_node_t end = struct type 'a p1 = [ `Text of string | `Bold of 'a list ] type 'a p2 = [ `See of string | `Mref of string * 'a p1 list ] type 'a p3 = [ 'a p1 | 'a p2 ]
type super_node_t = super_node_t p3 type nonlink_node_t = super_node_t p1 type link_node_t = super_node_t p2
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq) end;;
> Thanks Jeremy, that's quite ingenious. However, I've hit a problem in the > definition of the constructor functions (the full code + compiler error > is below). Now, I know that nonlink_node_t is a subset of super_node_t, > and therefore any variant valid for nonlink_node_t is also acceptable for > super_node_t. But how do I tell this to the compiler? (Note that having > users of the module manually casting types with :> is something I would > rather avoid).
> Thanks again, > Dario
> module rec Node: > sig > type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] > type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] > type super_node_t = [ nonlink_node_t | link_node_t ]
> val text: string -> nonlink_node_t > val bold: super_node_t list -> nonlink_node_t > val see: string -> link_node_t > val mref: string -> nonlink_node_t list -> link_node_t > end = > struct > type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] > type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] > type super_node_t = [ nonlink_node_t | link_node_t ]
> let text txt = `Text txt > let bold seq = `Bold seq > let see ref = `See ref > let mref ref seq = `Mref (ref, seq) > end
> open Node > let foo = text "foo" > let bar = bold [text "bar"]
> Error: This expression has type Node.nonlink_node_t > but is here used with type Node.super_node_t > The first variant type does not allow tag(s) `Mref, `See
> __________________________________________________________ > 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
Dario Teixeira wrote: > module rec Node: > sig > type nonlink_node_t = [ `Text of string | `Bold of > Node.super_node_t list ] > type link_node_t = [ `See of string | `Mref of string * > nonlink_node_t list ] > type super_node_t = [ nonlink_node_t | link_node_t ]
> val text: string -> nonlink_node_t > val bold: super_node_t list -> nonlink_node_t > val see: string -> link_node_t > val mref: string -> nonlink_node_t list -> link_node_t > end = > struct > type nonlink_node_t = [ `Text of string | `Bold of > Node.super_node_t list ] > type link_node_t = [ `See of string | `Mref of string * > nonlink_node_t list ] > type super_node_t = [ nonlink_node_t | link_node_t ]
> let text txt = `Text txt > let bold seq = `Bold seq > let see ref = `See ref > let mref ref seq = `Mref (ref, seq) > end
> open Node > let foo = text "foo" > let bar = bold [text "bar"]
> Error: This expression has type Node.nonlink_node_t > but is here used with type Node.super_node_t > The first variant type does not allow tag(s) `Mref, `See
This problem is apparently easy to solve. Just don't expect an exact super_node_t list argument for the bold function. Instead use val bold : [< super_node_t] list -> nonlink_node_t in the signature and let bold seq = `Bold (seq :> super_node_t list) in the body of the Node module's definition.
Dario Teixeira wrote: > and convert_super_node node = match node with > | #nonlink_node_t -> (convert_nonlink_node node :> super_node_t) > | #link_node_t -> (convert_link_node node :> super_node_t)
You need to rebind the matched value within the pattern in order to refine the type on the rhs:
and convert_super_node node = match node with | #nonlink_node_t as node -> (convert_nonlink_node node :> super_node_t) | #link_node_t as node -> (convert_link_node node :> super_node_t)
Thank you all for your help! I think we're almost there: with Wolfgang's suggestion, the Node module complies with the original constraints, as the code below shows: (the compiler complains -- as it should! -- when on the last line I try to nest two link nodes directly)
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
val text: string -> nonlink_node_t val bold: [< super_node_t] list -> nonlink_node_t val see: string -> link_node_t val mref: string -> nonlink_node_t list -> link_node_t end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq) end
open Node
let foo1 = text "foo" (* valid *) let foo2 = bold [text "foo"] (* valid *) let foo3 = mref "ref" [text "foo"] (* valid *) let foo4 = mref "ref" [see "ref"] (* invalid *)
Now, the icing on the cake would be the possibility to build a Node_to_Node set of functions without code duplication. Ideally, I would like to do something as follows:
module Node_to_Node = struct open Node
let rec convert_nonlink_node = function | `Text txt -> Node.text txt | `Bold seq -> Node.bold (List.map convert_super_node seq)
and convert_link_node = function | `See ref -> Node.see ref | `Mref (ref, seq) -> Node.mref ref (List.map convert_nonlink_node seq)
and convert_super_node node = match node with | #nonlink_node_t -> (convert_nonlink_node node :> super_node_t) | #link_node_t -> (convert_link_node node :> super_node_t) end
But this fails on the last line:
Error: This expression has type [< `Bold of 'a list & Node.super_node_t list | `Text of string ] as 'a but is here used with type [< `Mref of string * 'a list | `See of string ] These two variant types have no intersection
Do you see any way around it?
Thanks again for all your time and attention! Cheers, Dario
__________________________________________________________ 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
Wolfgang Lux wrote: > This problem is apparently easy to solve. Just don't expect an exact > super_node_t list argument for the bold function. Instead use > val bold : [< super_node_t] list -> nonlink_node_t > in the signature and > let bold seq = `Bold (seq :> super_node_t list) > in the body of the Node module's definition.
Indeed, works like a charm. You don't even need the coercion in the body of 'bold' for it to work.
This will hopefully allow me to remove some coercions from my own code, and use subtype annotations in the types.
For the sake of future reference, I'm going to summarise the solution to the original problem, arrived at thanks to the contribution of various people in this list (your help was very much appreciated!). This might came in handy in the future if you run into a similar problem.
So, we have a document composed of a sequence of nodes. There are four different kinds of nodes, two of which are terminals (Text and See) and two of which are defined recursively (Bold and Mref). Both See and Mref produce links, and we want to impose a constraint that no link node shall be the immediate ancestor of another link node. An additional constraint is that nodes must be created via constructor functions. Finally, the structure should be pattern-matchable, and the distinction between link/nonlink nodes should be preserved so that Node-to-Node functions do not require code duplication and/or ugly hacks.
Using conventional variants, the structure can be represented as follows. Alas, this solution is not compatible with constructor functions and requires unwanted scaffolding:
module Ast = struct type super_node_t = | Nonlink_node of nonlink_node_t | Link_node of link_node_t and nonlink_node_t = | Text of string | Bold of super_node_t list and link_node_t = | Mref of string * nonlink_node_t list | See of string end
Below is the solution that was finally obtained. Nodes are represented using polymorphic variants, and the module itself is recursive to get around the "type not fully defined" problem:
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
val text: string -> nonlink_node_t val bold: [< super_node_t] list -> nonlink_node_t val see: string -> link_node_t val mref: string -> nonlink_node_t list -> link_node_t end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq) end
If you try it out, you will see that this solution enforces the basic node constraints. The values foo1-foo4 are valid, whereas the compiler won't accept foo5, because a link node is the parent of another:
open Node let foo1 = text "foo" let foo2 = bold [text "foo"] let foo3 = mref "ref" [foo1; foo2] let foo4 = mref "ref" [bold [see "ref"]] let foo5 = mref "ref" [see "ref"]
Now, suppose you need to create an Ast-to-Node sets of functions (a likely scenario if you are building a parser for documents). The solution is fairly straightforward, but note the need to use the cast operator :> to promote link/nonlink nodes to supernodes:
and convert_link_node = function | Ast.Mref (ref, seq) -> Node.mref ref (List.map convert_nonlink_node seq) | Ast.See ref -> Node.see ref
and convert_super_node = function | Ast.Nonlink_node node -> (convert_nonlink_node node :> Node.super_node_t) | Ast.Link_node node -> (convert_link_node node :> Node.super_node_t) end
Finally, another common situation is to build functions to process nodes. The example below is that of a node-to-node "identity" module. Again, it is fairly straightforward, but note the use of the operator # and the need to cast link/nonlink nodes to supernodes:
module Node_to_Node = struct open Node
let rec convert_nonlink_node = function | `Text txt -> text txt | `Bold seq -> bold (List.map convert_super_node seq)
and convert_link_node = function | `See ref -> see ref | `Mref (ref, seq) -> mref ref (List.map convert_nonlink_node seq)
and convert_super_node = function | #nonlink_node_t as node -> (convert_nonlink_node node :> super_node_t) | #link_node_t as node -> (convert_link_node node :> super_node_t) end
Best regards, 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
Sorry, but in the meantime I came across two problems with the supposedly ultimate solution I just posted. I have a correction for one, but not for the other.
The following statements trigger the first problem:
let foo1 = text "foo" let foo2 = see "ref" let foo3 = bold [foo1; foo2]
Error: This expression has type Node.link_node_t but is here used with type Node.nonlink_node_t These two variant types have no intersection
The solution that immediately comes to mind is to make the return types for the constructor functions open: (I can see no disadvantage with this solution; please tell me if you find any)
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
val text: string -> [> nonlink_node_t] val bold: [< super_node_t] list -> [> nonlink_node_t] val see: string -> [> link_node_t] val mref: string -> nonlink_node_t list -> [> link_node_t] end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq) end
The second problem, while not a show-stopper, may open a hole for misuse of the module, so I would rather get it fixed. Basically, while the module provides constructor functions to build nodes, nothing prevents the user from bypassing them and constructing nodes manually. The obvious solution of declaring the types "private" results in an "This fixed type has no row variable" error. Any way around it?
Thanks once more for your time, 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
> Sorry, but in the meantime I came across two problems with the supposedly > ultimate solution I just posted. I have a correction for one, but not > for the other.
> The following statements trigger the first problem:
> let foo1 = text "foo" > let foo2 = see "ref" > let foo3 = bold [foo1; foo2]
> Error: This expression has type Node.link_node_t but is here used with type > Node.nonlink_node_t > These two variant types have no intersection
> The solution that immediately comes to mind is to make the return types > for the constructor functions open: (I can see no disadvantage with > this solution; please tell me if you find any)
I believe that is the correct solution. Sorry I didn't reach it sooner myself!
> module rec Node: > sig > type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t > list ] type link_node_t = [ `See of string | `Mref of string * > nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
> val text: string -> [> nonlink_node_t] > val bold: [< super_node_t] list -> [> nonlink_node_t] > val see: string -> [> link_node_t] > val mref: string -> nonlink_node_t list -> [> link_node_t] > end = > struct > type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t > list ] type link_node_t = [ `See of string | `Mref of string * > nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ]
> let text txt = `Text txt > let bold seq = `Bold (seq :> super_node_t list) > let see ref = `See ref > let mref ref seq = `Mref (ref, seq) > end
> The second problem, while not a show-stopper, may open a hole for misuse of > the module, so I would rather get it fixed. Basically, while the module > provides constructor functions to build nodes, nothing prevents the user > from bypassing them and constructing nodes manually. The obvious solution > of declaring the types "private" results in an "This fixed type has no row > variable" error. Any way around it?
I was going to suggest boxing every node in an ordinary variant type with a single private constructor:
type 'a t = private Node of 'a constraint 'a = [< Node.super_node_t ]
> I was going to suggest boxing every node in an ordinary variant type with a > single private constructor:
> type 'a t = private Node of 'a constraint 'a = [< Node.super_node_t ]
Thanks for the suggestion, Jon. Boxing every node is actually very welcome anyway, because later I would like to classify nodes into two different classes, "Basic" and "Complex" (these are orthogonal to the existing link/nonlink distinction), and the only way I see of doing this is via some phantom type trickery (more on that in a later message).
Anyway, going back to your boxing suggestion, how can it actually be applied to the signature of the Node module? As you can see below, I have define type 'a t (without the "Node" constructor -- is it really necessary?), but what is the syntax for saying that the constructors text, bold, see, and mref, return a kind of 'a t without breaking the existing restrictions?
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ] type 'a t = private 'a constraint 'a = [< super_node_t ]
val text: string -> [> nonlink_node_t] val bold: [< super_node_t] list -> [> nonlink_node_t] val see: string -> [> link_node_t] val mref: string -> nonlink_node_t list -> [> link_node_t] end =
Sorry for the stream of questions. As you may have noticed, this thread has gone deep into uncharted territory as far as the Ocaml documentation goes. In fact, I have the feeling the only existing documentation for these subjects lies within the collective wisdom of the people on this list...
Best regards, 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
After some trial and error in the top-level, I think I got the hang of the 'constraint' declaration (is there other documentation for it besides the couple of lines in the Reference Manual?). Note that besides the already discussed link/nonlink distinction between nodes, there is now also an orthogonal distinction between basic/complex nodes (all nodes except for Mref are basic; any document that uses Mref thus becomes "contaminated" and cannot use basic-only functions; the inverse, however, is not true). I took advantage of Jon's suggestion of boxing all return types into a single Node.t to implement this latter distinction using phantom types (is there even an alternative technique?).
Now, the code below seems correct, and running "ocamlc -i node.ml" produces the type signatures you would expect, and without error messages. However, running "ocamlc -c node.ml" fails with a "The type of this expression contains type variables that cannot be generalized" error on the declaration of foo3. Moreover, if you comment out the top-level declarations and try to compile only the module declaration, you will also get different results whether you run "ocamlc -i" or "ocamlc -c". The former displays the module's signature as expected, but the latter produces this error message:
Type declarations do not match: type ('a, 'b) t = ('a, 'b) Node.t constraint 'a = [< super_node_t ] is not included in type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
I find this behaviour a bit odd. What is going on?
Best regards, Dario Teixeira
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ] type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
val text: string -> ([> nonlink_node_t], [> `Basic]) t val bold: ([< super_node_t], 'a) t list -> ([> nonlink_node_t], 'a) t val see: string -> ([> link_node_t], [> `Basic]) t val mref: string -> (nonlink_node_t, 'a) t list -> ([> link_node_t], [> `Complex]) t
val make_basic: ([< super_node_t], [< `Basic]) t -> (super_node_t, [`Basic]) t val make_complex: ([< super_node_t], [< `Basic | `Complex]) t -> (super_node_t, [`Complex]) t end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ] type ('a, 'b) t = 'a constraint 'a = [< super_node_t ]
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq)
let make_basic n = (n :> (super_node_t, [`Basic]) t) let make_complex n = (n :> (super_node_t, [`Complex]) t) end
open Node
let foo1 = text "ola" let foo2 = bold [text "ola"] let foo3 = mref "ref" [foo1; foo2]
let basic1 = make_basic foo1 let basic2 = make_basic foo2
let complex1 = make_complex foo1 let complex2 = make_complex foo2 let complex3 = make_complex foo3
__________________________________________________________ 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
Dario Teixeira wrote: > type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
I don't think this is quite what you want yet, although it's getting close!
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.
The second problem is indicated by the error message you reported:
"The type of this expression contains type variables that cannot be generalized"
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.
The final type declaration, then, is
type (+'a, +'b) t constraint 'a = [< super_node_t ]
in the signature and
type (+'a, +'b) t = 'a constraint 'a = [< super_node_t ]
> 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
> Dario Teixeira wrote: > > type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ]
> I don't think this is quite what you want yet, although it's getting > close!
> The first problem is that phantom types must be implemented in terms > of abstract (or at least generative) types.
This is actually the other way round: abstract and private types allow phantom types, but abbreviations and normal datatypes (generative ones) don't. So the above code really defines a phantom type.
Jacques Garrigue wrote: > From: Jeremy Yallop <jeremy.yal...@ed.ac.uk> >> Dario Teixeira wrote: >>> type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ] >> I don't think this is quite what you want yet, although it's getting >> close!
>> The first problem is that phantom types must be implemented in terms >> of abstract (or at least generative) types.
> This is actually the other way round: abstract and private types allow > phantom types, but abbreviations and normal datatypes (generative > ones) don't.
Thanks for the correction! I haven't yet properly internalized private rows. It seems that private rows allow phantom types because there is abstraction (and hence generativity) involved.
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. *)
> So the above code really defines a phantom type.
Yes.
On a related note, does Dario's declaration above become ambiguous with the introduction of private type abbreviations? The following program passes typechecking in 3.10.2, but not in 3.11+dev12, perhaps because `t' is interpreted as a private type abbreviation rather than as a private row type.
type super_node_t = [`S]
module M : sig type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ] end = struct type super_node_t = [`S] type ('a, 'b) t = 'a constraint 'a = [< super_node_t ] end
let f x = (x : [<super_node_t] :> ([< super_node_t], _) M.t)
Thanks for the clarification, Jacques. So I guess my initial interpretation of 'private' was correct. But is 'private' also applicable when a type is declared using a constraint? In my Node module, for example, type 't' is declared abstract in the signature:
type (+'a, 'b) t constraint 'a = [< super_node_t ]
In the implementation, the type is declared as follows:
type (+'a, 'b) t = 'a constraint 'a = [< super_node_t ]
Is it possible in this case to make signature equal to the implementation except for a 'private' declaration? (Being able to pattern-match on values of type 't' would be very handy, that is why I would prefer to use 'private' instead of making the type fully abstract).
Note: I am running Ocaml 3.11+dev12. Jeremy just sent a message where he reports that the compiler behaviour in this matter changed between 3.10 and 3.11.
Thank you for your time, 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
> Thanks for the clarification, Jacques. So I guess my initial interpretation > of 'private' was correct. But is 'private' also applicable when a type > is declared using a constraint? In my Node module, for example, type 't' > is declared abstract in the signature:
> type (+'a, 'b) t constraint 'a = [< super_node_t ]
> In the implementation, the type is declared as follows:
> type (+'a, 'b) t = 'a constraint 'a = [< super_node_t ]
> Is it possible in this case to make signature equal to the implementation > except for a 'private' declaration? (Being able to pattern-match on values > of type 't' would be very handy, that is why I would prefer to use 'private' > instead of making the type fully abstract).
> Note: I am running Ocaml 3.11+dev12. Jeremy just sent a message where > he reports that the compiler behaviour in this matter changed between > 3.10 and 3.11.
This is indeed possible in 3.11, due to the addition of private abbreviations. Note however that the behaviour of private abbreviations is not as transparent as private types or rows: the only practical difference between an abstract type and a private abbreviation is that you can explicitely coerce from the private abbreviation to its definition. You cannot use pattern matching directly without coercion.
So if you write
type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t ]
then you must write (x : (_,_) t :> [> ]) if you want to use pattern matching on x.
Another side-effect of the addition of private abbreviations is that now the distinction between private rows and private abbreviations is syntactic. In particular
type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t ]
defined a private row in 3.10, but it is a private abbreviation in 3.11 (with of course a different semantics). If you need the private row semantics, you should now write it as
> Jacques Garrigue wrote: > > From: Jeremy Yallop <jeremy.yal...@ed.ac.uk> > >> Dario Teixeira wrote: > >>> type ('a, 'b) t = private 'a constraint 'a = [< super_node_t ] > >> I don't think this is quite what you want yet, although it's getting > >> close!
> >> The first problem is that phantom types must be implemented in terms > >> of abstract (or at least generative) types.
> > This is actually the other way round: abstract and private types allow > > phantom types, but abbreviations and normal datatypes (generative > > ones) don't.
> Thanks for the correction! I haven't yet properly internalized private > rows. It seems that private rows allow phantom types because there is > abstraction (and hence generativity) involved.
> 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.
> On a related note, does Dario's declaration above become ambiguous with > the introduction of private type abbreviations? The following program > passes typechecking in 3.10.2, but not in 3.11+dev12, perhaps because > `t' is interpreted as a private type abbreviation rather than as a > private row type.
I detailed the change in my answer to his mail. In 3.11 the distinction is syntactic: only explicit variant or object types give rise to private rows. By the way, I forgot to mention that aliases (as keyword) of those were not allowed until now, so I have to fix it to make the syntax for private rows work. (There are useful examples using this syntax.)
Jacques Garrigue wrote: > From: Jeremy Yallop <jeremy.yal...@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
> 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
Thanks once more for your help, Jacques. I had no idea this problem would prove to be such a challenge!
> So if you write
> type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t ]
> then you must write (x : (_,_) t :> [> ]) if you want to use pattern > matching on x.
The 'private' declaration you suggested does work on some simpler examples, but the 3.11 compiler won't accept it for the Node module. This is the code:
module rec Node: sig type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ] type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t ]
val text: string -> ([> nonlink_node_t], [> `Basic]) t val bold: ([< super_node_t], 'a) t list -> ([> nonlink_node_t], 'a) t val see: string -> ([> link_node_t], [> `Basic]) t val mref: string -> (nonlink_node_t, 'a) t list -> ([> link_node_t], [> `Complex]) t
val make_basic: ('a, [< `Basic]) t -> ('a, [`Basic]) t val make_complex: ('a, [< `Basic | `Complex]) t -> ('a, [`Complex]) t end = struct type nonlink_node_t = [ `Text of string | `Bold of Node.super_node_t list ] type link_node_t = [ `See of string | `Mref of string * nonlink_node_t list ] type super_node_t = [ nonlink_node_t | link_node_t ] type (+'a, 'b) t = 'a constraint 'a = [< super_node_t ]
let text txt = `Text txt let bold seq = `Bold (seq :> super_node_t list) let see ref = `See ref let mref ref seq = `Mref (ref, seq)
let make_basic n = n let make_complex n = n end
And this is the error:
Type declarations do not match: type (+'a, 'b) t = ('a, 'b) Node.t constraint 'a = [< super_node_t ] is not included in type (+'a, 'b) t = private 'a constraint 'a = [< super_node_t ]
> By the way, I forgot to mention that aliases (as keyword) of those > were not allowed until now, so I have to fix it to make the syntax for > private rows work. (There are useful examples using this syntax.)
> type ('a, 'b) t = private [< super_node_t ] as 'a
With 3.11+dev12, the above declaration produces a "Unbound type parameter .." error. When you say you have to fix it, do you mean this will actually be a valid declaration in 3.11 final? And will this solution allow for easier pattern-matching of Node values, without the need for coercion?
Speaking of coercion, the exact syntax for it in combination with '#' patterns elludes me. Take for example a simple, "identity", Node-to-Node module listed below. How can coercion be applied?
module Node_to_Node = struct open Node
let rec convert_nonlink_node = function | `Text txt -> text txt | `Bold inl -> bold (List.map convert_super_node inl)
and convert_link_node = function | `Mref (ref, inl) -> mref ref (List.map convert_nonlink_node inl) | `See ref -> see ref
and convert_super_node = function | #nonlink_node_t as node -> (convert_nonlink_node node : ('a, 'b) t :> (super_node_t, 'b) t) | #link_node_t as node -> convert_link_node node end
Best regards, 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
|
