Private types in 3.11, again

Private types in 3.11, again

[Dario Teixeira]

Hi,

(Note: this problem is similar to one I've posted before; there are however
differences.  Also, my apologies for the problem requiring a long introduction
before actually being presented).

Consider a sequence of nodes such as those present in an inline context in
XHTML.  Some of these nodes are leaf nodes (Text and Href), while others are
built from a list of existing nodes (Bold and Mref).  Moreover, some nodes
create hyperlinks (Href and Mref).  A straightforward Ocaml representation
could be as follows:


type node_t =
	| Text of string
	| Bold of node_t list			(* recursive! *)
	| Href of string
	| Mref of string * node_t list		(* recursive! *)


There is furthermore an important restriction: a link node may not be the
ancestor of another link node, no matter how deep the ancestry level (in
similarity with the W3C rules for XHTML).  While this restriction could be
enforced by runtime checking, I very much prefer to represent nodes in such
a way that the type system itself would ensure the impossibility of creating
illegal values.

Below is the best solution I could come up with so far (note that this code
requires 3.11).  It uses a phantom type to "taint" link nodes, making them
unsuitable to be descendants of other link nodes.  Also, note the use of
'private' to allow pattern-matching by external code without breaking the
phantom type restrictions.


module Node:
sig
	type node_t =
		private
		| Text of string
		| Bold of node_t list
		| Href of string
		| Mref of string * node_t list

	type +'a t = private node_t

	val text: string -> [> `Nonlink ] t
	val bold: 'a t list -> 'a t
	val href: string -> [> `Link ] t
	val mref: string -> [< `Nonlink ] t list -> [> `Link ] t
end =
struct
	type node_t =
		| Text of string
		| Bold of node_t list
		| Href of string
		| Mref of string * node_t list

	type +'a t = node_t

	let text txt = Text txt
	let bold seq = Bold seq
	let href lnk = Href lnk
	let mref lnk seq = Mref (lnk, seq)
end


So far so good.  Now consider a function that takes a node and returns
another node, in all identical except that all occurrences of Text (either
in the parent or in all descendants if the node is defined recursively)
are replaced by the capitalised version.  Moreover, I want to place this
function in a different module, called Foobar:


module Foobar:
sig
        open M
        val capitalise_node: 'a t -> 'a t
end =
struct
        open M
        let capitalise_node node =
                let rec capitalise_node_aux forbid_link node = match (forbid_link, node) with
                        | (_, Text txt)                 -> text (String.capitalize txt)
                        | (x, Bold seq)                 -> bold (List.map (capitalise_node_aux x) seq)
                        | (false, Href lnk)             -> href lnk
                        | (false, Mref (lnk, seq))      -> mref lnk (List.map (capitalise_node_aux true) seq)
                        | _                             -> failwith "oops"
                in capitalise_node_aux false node
end


Unfortunately, the code above fails to compile, producing this error:


Error: This expression has type [> `Link | `Nonlink ] M.t list
       but is here used with type [< `Nonlink ] M.t list
       The second variant type does not allow tag(s) `Link


For the Foobar module to work, I have to remove the 'private' declaration in
module Node, which of course breaks the phantom type.  Note that the function
above will also compile fine if it is defined inside Node instead of Foobar
(but which is useless to me).

So my question is how can I make the Foobar code behave as if it were defined
inside Node.  Based on a previous thread [1], I'm guessing there is a solution,
but I've been unable to hit on its exact formulation.


Thanks in advance for any light you may shed on this issue.  It is much
appreciated!

Kind regards,
Dario Teixeira


[1] http://groups.google.com/group/fa.caml/browse_thread/thread/d9c5e30b973db187#

Re: [Caml-list] Private types in 3.11, again

[Dario Teixeira]

Hi,

> So my question is how can I make the Foobar code behave as if it were
> defined inside Node.  Based on a previous thread [1], I'm guessing there
> is a solution, but I've been unable to hit on its exact formulation.

There have been no replies yet to my question, but I'm still stuck with
this little problem.  The offending code is below; though it doesn't
compile, I reckon that all it needs is a suitable type annotation.  I'm
guessing this because the function capitalise_node function will compile
fine if placed inside the Node module.  Any ideas on how to solve this?

Thanks in advance!
Best regards,
Dario Teixeira


module Node:
sig
	type node_t =
		private
		| Text of string
		| Bold of node_t list
		| Href of string
		| Mref of string * node_t list

	type +'a t = private node_t

	val text: string -> [> `Nonlink ] t
	val bold: 'a t list -> 'a t
	val href: string -> [> `Link ] t
	val mref: string -> [< `Nonlink ] t list -> [> `Link ] t
end =
struct
	type node_t =
		| Text of string
		| Bold of node_t list
		| Href of string
		| Mref of string * node_t list

	type +'a t = node_t

	let text txt = Text txt
	let bold seq = Bold seq
	let href lnk = Href lnk
	let mref lnk seq = Mref (lnk, seq)
end


module Foobar:
sig
	open Node
	val capitalise_node: 'a t -> 'a t
end =
struct
	open Node
	let capitalise_node node =
		let rec capitalise_node_aux forbid_link node = match (forbid_link, node) with
			| (_, Text txt)			-> text (String.capitalize txt)
			| (x, Bold seq)			-> bold (List.map (capitalise_node_aux x) seq)
			| (false, Href lnk)		-> href lnk
			| (false, Mref (lnk, seq))	-> mref lnk (List.map (capitalise_node_aux true) seq)
			| _				-> failwith "oops"
		in capitalise_node_aux false node
end

Re: [Caml-list] Private types in 3.11, again

[Dario Teixeira]

Hi again,

I ditched the regular variants in favour of polymorphic variants, hoping
the coercion trick described by Jacques Garrigue would help [1].  I've also
simplified the formulation as much as possible.  Anyway, I'm still stuck
with the same problem: while function 'sprint' works alright inside the
Node module, its clone 'sprint2' fails to compile when placed outside.
Is this a case where no amount of explicit annotations and coercions will
work or am I missing something obvious?

Thanks in advance!
Regards,
Dario Teixeira

[1] http://groups.google.com/group/fa.caml/msg/855011402f1ca1b5


module Node:
sig
	type elem_t = [ `Text of string | `Bold of elem_t list ]
	type +'a t = private elem_t

	val text: string -> [> `Basic ] t
	val bold: 'a t list -> [> `Complex ] t
	val sprint: 'a t -> string
end =
struct
	type elem_t = [ `Text of string | `Bold of elem_t list ]
	type +'a t = elem_t

	let text str = `Text str
	let bold seq = `Bold seq
	let rec sprint = function
		| `Text str	-> Printf.sprintf "(Text %s)" str
		| `Bold seq	-> Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint seq))
end


module Foobar:
sig
	val sprint2: 'a Node.t -> string
end =
struct
	let rec sprint2 node = match (node : _ Node.t :> [> ]) with
		| `Text str	-> Printf.sprintf "(Text %s)" str
		| `Bold seq	-> Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint2 (seq : _ Node.t list :> [>] list)))
end

Re: [Caml-list] Private types in 3.11, again

[Jacques Carette]

Hmmm, a variant of your code may be exhibiting a bug in ocaml 3.11.0.

In your signature, change the +'a t signature to
    type +'a t = private [< elem_t ]
and remove all annotations from the definition of sprint2.  Then, as 
defined, one gets the error message

File "bug2.ml", line 26, characters 0-223:
Error: Signature mismatch:
       Modules do not match:
         sig
           val sprint2 :
             ([< `Bold of 'a list | `Text of string ] as 'a) -> string
         end
       is not included in
         sig val sprint2 : 'a Node.t -> string end
       Values do not match:
         val sprint2 :
           ([< `Bold of 'a list | `Text of string ] as 'a) -> string
       is not included in
         val sprint2 : 'a Node.t -> string

which is not very informative, especially since expanding 'a Node.t 
gives exactly what the compiler reports as the first argument of sprint2.

To coax the compiler to be more helpful, on places the definition of 
sprint2 outside a module (but still in the same file as Node), and 
instead the result is:

File "bug2.ml", line 30, characters 26-29:
Error: This expression has type Node.elem_t list but is here used with type
         'a Node.t list
       Type Node.elem_t = [ `Bold of Node.elem_t list | `Text of string ]
       is not compatible with type
         'a Node.t = [< `Bold of Node.elem_t list | `Text of string ]
       Types for tag `Text are incompatible

[That point to the seq in List.map sprintf2 seq].  Here is where the 
potential bug is: how is string incompatible with string?
[If this is a bug, I'll add it to the database]

Jacques

Re: [Caml-list] Private types in 3.11, again

[Dario Teixeira]

Hi,

> Hmmm, a variant of your code may be exhibiting a bug in ocaml 3.11.0.

Thanks for the reply.  I'm kind of hoping it is indeed a bug, because
those are fixable and it would mean what I intend to do is feasible...

Best regards,
Dario Teixeira

Re: [Caml-list] Private types in 3.11, again

[Jacques Garrigue]

From: Dario Teixeira <darioteixeira@yahoo.com>
> I ditched the regular variants in favour of polymorphic variants, hoping
> the coercion trick described by Jacques Garrigue would help [1].  I've also
> simplified the formulation as much as possible.  Anyway, I'm still stuck
> with the same problem: while function 'sprint' works alright inside the
> Node module, its clone 'sprint2' fails to compile when placed outside.
> Is this a case where no amount of explicit annotations and coercions will
> work or am I missing something obvious?
> 
> Thanks in advance!
> Regards,
> Dario Teixeira
> 
> [1] http://groups.google.com/group/fa.caml/msg/855011402f1ca1b5
> 
> 
> module Node:
> sig
> 	type elem_t = [ `Text of string | `Bold of elem_t list ]
> 	type +'a t = private elem_t
> 
> 	val text: string -> [> `Basic ] t
> 	val bold: 'a t list -> [> `Complex ] t
> 	val sprint: 'a t -> string
> end =
> struct
> 	type elem_t = [ `Text of string | `Bold of elem_t list ]
> 	type +'a t = elem_t
> 
> 	let text str = `Text str
> 	let bold seq = `Bold seq
> 	let rec sprint = function
> 		| `Text str	-> Printf.sprintf "(Text %s)" str
> 		| `Bold seq	-> Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint seq))
> end
> 
> 
> module Foobar:
> sig
> 	val sprint2: 'a Node.t -> string
> end =
> struct
> 	let rec sprint2 node = match (node : _ Node.t :> [> ]) with
> 		| `Text str	-> Printf.sprintf "(Text %s)" str
> 		| `Bold seq	-> Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint2 (seq : _ Node.t list :> [>] list)))
> end

The problem is clear enough: the annotation in your recursive call to
sprint2 is inverted. It assumes that seq has type Node.t, while it is
Node.elem_t, and tries to convert it to a list of variants, which is
incompatible to the input to sprint2, which is Node.t (due to the
annotation on node.)
But you cannot just revert the annotation, since the subtyping only
goes in one direction.
The solution here is to split the definition in two steps:

module Foobar:
sig
  val sprint2: 'a Node.t -> string
end = struct
  let rec sprint2 = function
    | `Text str	-> Printf.sprintf "(Text %s)" str
    | `Bold seq	-> Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint2 seq))
  let sprint2 node = sprint2 (node : 'a Node.t :> [> ])
end

However, I agree with my eponym that there is little point in using a
private abbreviation where you could use a private row, and avoid
coercions. When doing this, you have to be careful that your type is
recursive, so that the row should be recursive too.

You should change the signature to be:
  type 'a elem_t = [ `Text of string | `Bold of 'a list ]
  type +'a t = private [< 'b elem_t] as 'b
and the implementation
  type 'a elem_t = [ `Text of string | `Bold of 'a list ]
  type +'a t = 'b elem_t as 'b

Then the module Foobar types without any coercion.

I have also looked at your previous code, using normal variants.
It looks like you are trying to do something like GADTs, and I don't
see how you could possibly do that without adding some support inside
the first module (where the phantom type is defined.) For instance,
you could define a generic mapping function there, and use instances
of it outside of the module.

Hope this helps,

Jacques Garrigue 

Re: [Caml-list] Private types in 3.11, again

[Jacques Garrigue]

Hi Jacques,

From: Jacques Carette <carette@mcmaster.ca>
> Hmmm, a variant of your code may be exhibiting a bug in ocaml 3.11.0.
> 
> In your signature, change the +'a t signature to
>     type +'a t = private [< elem_t ]
> and remove all annotations from the definition of sprint2.  Then, as 
> defined, one gets the error message
> 
> File "bug2.ml", line 26, characters 0-223:
> Error: Signature mismatch:
>        Modules do not match:
>          sig
>            val sprint2 :
>              ([< `Bold of 'a list | `Text of string ] as 'a) -> string
>          end
>        is not included in
>          sig val sprint2 : 'a Node.t -> string end
>        Values do not match:
>          val sprint2 :
>            ([< `Bold of 'a list | `Text of string ] as 'a) -> string
>        is not included in
>          val sprint2 : 'a Node.t -> string
> 
> which is not very informative, especially since expanding 'a Node.t 
> gives exactly what the compiler reports as the first argument of sprint2.

Unfortunately, type errors for private row types can be hard to
understand when the types themselves are complex.
As I pointed in my answer to Dario, the private row type Node.t has to
be recursive for it to be an instance of a recursive type.
[< elem_t] does not define a recursive type, but just adds a row
variable on its outermost variant.

> To coax the compiler to be more helpful, on places the definition of 
> sprint2 outside a module (but still in the same file as Node), and 
> instead the result is:
> 
> File "bug2.ml", line 30, characters 26-29:
> Error: This expression has type Node.elem_t list but is here used with type
>          'a Node.t list
>        Type Node.elem_t = [ `Bold of Node.elem_t list | `Text of string ]
>        is not compatible with type
>          'a Node.t = [< `Bold of Node.elem_t list | `Text of string ]
>        Types for tag `Text are incompatible
> 
> [That point to the seq in List.map sprintf2 seq].  Here is where the 
> potential bug is: how is string incompatible with string?
> [If this is a bug, I'll add it to the database]

The bug is in only in the error message; which seems another instance
of the problem you reported in your previous mail.
There is however a real type error, because Node.t, as it has a
private row, cannot be an instance of the fixed type elem_t.

Cheers,

Jacques Garrigue

Re: [Caml-list] Private types in 3.11, again

[Jacques Garrigue]

From: Dario Teixeira <darioteixeira@yahoo.com>
> > So my question is how can I make the Foobar code behave as if it were
> > defined inside Node.  Based on a previous thread [1], I'm guessing there
> > is a solution, but I've been unable to hit on its exact formulation.
> 
> There have been no replies yet to my question, but I'm still stuck with
> this little problem.  The offending code is below; though it doesn't
> compile, I reckon that all it needs is a suitable type annotation.  I'm
> guessing this because the function capitalise_node function will compile
> fine if placed inside the Node module.  Any ideas on how to solve this?

The problem is much deeper than a simple annotation.
If you want capitalize_node to have a polymorphic type, while it is
based on operations that produce values with specific (non-polymorphic)
types, ideally you need something like GADTs. Unfortunately they are
not available in ocaml, so you have to provide the basic building
blocks in Node; i.e. you need a polymorphic function collecting
non-polymorphic values.

Here is some sample code. Note that I use an object here, but this is
only to be able to pass a polymorphic function for "bold" (a record
would have worked too). Also, the same code would probably work with
polymorphic variants, except for the "[`Nonlink] t" inside the
definition of "t" (polymorphic variants may only have regular types).

More practically, the "map" function in Node is not the map of lists:
it doesn't recurse on the structure of t. The recursion is rather done
inside "capitalize_node", by redefining bold and mref. You might want
to define such a generic recursive maker somewhere, but the point is
that you don't have to do it inside Node, and you keep full generality
(i.e. your make may choose to only recurse on Bold for instance...)

I hope this gives you some ideas on how to proceed.

Cheers,

Jacques Garrigue

module Node: sig
  type +'a t = private
    | Text of string
    | Bold of 'a t list
    | Href of string
    | Mref of string * [`Nonlink] t list

  val text: string -> [> `Nonlink ] t
  val bold: 'a t list -> 'a t
  val href: string -> [> `Link ] t
  val mref: string -> [ `Nonlink ] t list -> [> `Link ] t
  class maker : object
    method text: string -> [ `Nonlink ] t
    method bold: 'a t list -> 'a t
    method href: string -> [ `Link ] t
    method mref: string -> [ `Nonlink ] t list -> [ `Link ] t
  end
  val map: maker -> 'a t -> 'a t
end = struct
  type +'a t =
    | Text of string
    | Bold of 'a t list
    | Href of string
    | Mref of string * [`Nonlink] t list

  let text txt = Text txt
  let bold seq = Bold seq
  let href lnk = Href lnk
  let mref lnk seq = Mref (lnk, seq)
  class maker = object
    method text: string -> [ `Nonlink ] t = text
    method bold: 'a. 'a t list -> 'a t = bold
    method href: string -> [ `Link ] t = href
    method mref: string -> [ `Nonlink ] t list -> [ `Link ] t = mref
  end
  let rec map (m : maker) = function
      Text s -> (m#text s :> 'a t)
    | Bold l -> (m#bold l :> 'a t)
    | Href s -> (m#href s :> 'a t)
    | Mref (s, l) -> (m#mref s l :> 'a t)
  let map = (map : _ -> 'a t -> 'a t :> _ -> 'b t -> 'b t)
end

module Foobar: sig
  open Node
  val capitalise_node: 'a t -> 'a t
end = struct
  open Node
  let capitalise_node node =
    map
      (object (self) inherit maker
        method text txt = text (String.capitalize txt)
        method bold l = bold (List.map (map self) l)
        method mref s l = mref s (List.map (map self) l)
       end)
      node
end


# open Node;;
# Foobar.capitalise_node (mref "a" [bold [text "b"]; text "c"]);;
- : [> `Link ] Node.t = Mref ("a", [Bold [Text "B"]; Text "C"])

Re: [Caml-list] Private types in 3.11, again

[Dario Teixeira]

Hi,

Thank you very much for your help, Jacques!  It's always enlightening to
see an Ocaml ninja in action, though I'm still digesting the finer points
of your message.  Anyway, I have implemented all three solutions you suggested:

a) Using a private row and PV
b) Using a private abbreviation and PV
c) Using the mapper + object system with regular variants

Solution a) is by far the most convenient, though I'm still having some trouble
with it (more below).  Which brings me to a crucial point where I'm still
fuzzy.  My initial model for the link-nodes-shall-not-be-ancestors-of-their-kin
problem did indeed rely on what I now realise are GADTs.  I ran into a
limitation of the type system and so I recast the model using phantom types
because I hoped they could provide a workaround.  So my question is whether it
is at all possible to emulate GADTs using only PV + phantom types, or if on the
contrary one needs to use the object system in these cases, as exemplified by
solution c).  In other words, is solution a) futile, or did you use the object
system in solution c) simply because you were also using regular variants?

As for the problem with solution a), it shows up when I implement outside
of module Node any non-trivial function operating on 'a Node.t.  Function
capitalise_node, for example:


module Node:
sig
	type 'a node_t =
		[ `Text of string
		| `Bold of 'a list
		| `Href of string
		| `Mref of string * 'a list
		]

	type +'a t = private [< 'b node_t ] as 'b

	val text: string -> [> `Nonlink ] t
	val bold: 'a t list -> 'a t
	val href: string -> [> `Link ] t
	val mref: string -> [< `Nonlink ] t list -> [> `Link ] t
end =
struct
	type 'a node_t =
		[ `Text of string
		| `Bold of 'a list
		| `Href of string
		| `Mref of string * 'a list
		]

	type +'a t = 'b node_t as 'b

	let text txt = `Text txt
	let bold seq = `Bold seq
	let href lnk = `Href lnk
	let mref lnk seq = `Mref (lnk, seq)
end


module Foobar:
sig
	val capitalise_node: 'a Node.t -> 'a Node.t
end =
struct
	let capitalise_node node =
		let rec capitalise_node_aux forbid_link node = match (forbid_link, node) with
			| (_, `Text txt)		-> Node.text (String.capitalize txt)
			| (x, `Bold seq)		-> Node.bold (List.map (capitalise_node_aux x) seq)
			| (false, `Href lnk)		-> Node.href lnk
			| (false, `Mref (lnk, seq))	-> Node.mref lnk (List.map (capitalise_node_aux true) seq)
			| _				-> failwith "this shouldn't happen"
		in capitalise_node_aux false node
end


The code above produces the compiler error below (though remember that this
same function works fine inside the Node module):

Error: This expression has type ([> `Link | `Nonlink ] as 'a) Node.t list
       but is here used with type ([< `Nonlink ] as 'b) Node.t list
       Type
         'a Node.t =
           [< `Bold of 'a Node.t list
            | `Href of string
            | `Mref of string * 'a Node.t list
            | `Text of string ]
       is not compatible with type
         'b Node.t =
           [< `Bold of 'b Node.t list
            | `Href of string
            | `Mref of string * 'b Node.t list
            | `Text of string ]
       The first variant type does not allow tag(s) `Link


Thanks again for all your time!
Best regards,
Dario Teixeira

Re: [Caml-list] Private types in 3.11, again

[Gabriel Kerneis]

Hi,

On Wed, Jan 21, 2009 at 11:11:14AM -0800, Dario Teixeira wrote:
> So my question is whether it
> is at all possible to emulate GADTs using only PV + phantom types, or if on the
> contrary one needs to use the object system in these cases, as exemplified by
> solution c).  In other words, is solution a) futile, or did you use the object
> system in solution c) simply because you were also using regular variants?

I didn't followed the thread closely, but did you have a look at Ocsigen's way
to implement params_type?

http://ocsigen.org/trac/browser/server/ocsigen.ml?rev=183
(from line 146)

I don't know what it's worth, but anyway it uses only PV (and Obj.magic).

Regards,
-- 
Gabriel Kerneis

GADTs in Ocaml (was: Private types in 3.11, again)

[Dario Teixeira]

Hi,

> I didn't followed the thread closely, but did you have a look
> at Ocsigen's way to implement params_type?

Thanks for the suggestion.  Actually, there's an Ocsigen connection with
what I'm doing.  The Node module we've been discussing is a simplification;
the real problem is for a data type that can be converted into the XHTML.M
data used in Ocsigen.  (As was discussed some time ago in the Ocsigen mailing
list, the XHTML.M module does not strictly enforce the nested link nodes
rule of the W3C.  Nevertheless I have been looking for a solution that does
enforce this rule).

Anyway, I took a brief look at the code you mentioned, and re-read the
relevant section in the "Rapport Ocsigen" you wrote a while ago (when
I first read that report I had no idea what GADTs were!).  It does seem
that we're all just cooking up workarounds to the lack of GADTs in
Ocaml.  Now, I recall Xavier Leroy mentioning this topic at the user
meeting last year.  It seems the theory is ready, but the compiler
needs some work done before it can accommodate this new feature.  Are
there news on that front?

Best regards,
Dario Teixeira

Re: [Caml-list] Private types in 3.11, again

[Jacques Garrigue]

From: Dario Teixeira <darioteixeira@yahoo.com>

> Thank you very much for your help, Jacques!  It's always enlightening to
> see an Ocaml ninja in action, though I'm still digesting the finer points
> of your message.  Anyway, I have implemented all three solutions you suggested:
> 
> a) Using a private row and PV
> b) Using a private abbreviation and PV
> c) Using the mapper + object system with regular variants
> 
> Solution a) is by far the most convenient, though I'm still having some trouble
> with it (more below).  Which brings me to a crucial point where I'm still
> fuzzy.  My initial model for the link-nodes-shall-not-be-ancestors-of-their-kin
> problem did indeed rely on what I now realise are GADTs.  I ran into a
> limitation of the type system and so I recast the model using phantom types
> because I hoped they could provide a workaround.  So my question is whether it
> is at all possible to emulate GADTs using only PV + phantom types, or if on the
> contrary one needs to use the object system in these cases, as exemplified by
> solution c).  In other words, is solution a) futile, or did you use the object
> system in solution c) simply because you were also using regular variants?

I should have been clearer that, for what you are trying to do, the
different between regular variants and polymorphic variants is mostly
irrelevant. This is because you are using a phantom type to refine
your types, rather than subtyping the polymorphic variants themselves,
so you can perfectly do a) with regular variant (i.e. a private
variant type), or c) with polymorphic variants. For a), you would just
have to write

	type 'a t = private Text of string | Bold of 'a t list

and everything should work fine.

As I mentionned in my previous mail, I only use objects here for
polymorphic methods (i.e. the ability to pass a polymorphic function
as parameter to a function), so that records with polymorphic fields
would have worked too. One might even try with functors.

> As for the problem with solution a), it shows up when I implement outside
> of module Node any non-trivial function operating on 'a Node.t.  Function
> capitalise_node, for example:

This is not surprising at all.
The reason everything was simpler in your second example is that you
were just decomposing a private type, not building a new value. Private
types were specifically designed to do that, so they are the ideal
tool in that case.

In your first example, you want to simultaneously deconstruct a value,
a reconstruct a new value with the same polymorphic type. For this,
you need the expressive power of GADTs, i.e. the ability to
instanciate type variables differently inside different branches of a
pattern-matching. Since they are not available in ocaml, what I have
done in c) is to define a skeleton of pattern-matching, such that you
can simultaneously decompose a value and create a new value with the
same type, polymorphically. Of course this is not as generic as GADTs,
since only one specific form of pattern-matching is handled, where the
return type should be exactly the same as the matched type, but this
is generic enough that you can write many kinds of transformations.

There are other known encodings of GADTs, relying on existential
types. They are more generic, but since ocaml has only universal
types, existentials have to be encoded in a kind of
continuation-passing style, which makes using them rather heavy.

Personally I would suggest you try to see how far you can go with (c).
I'm repeating myself, but if you're just decomposing your input
without creating a new polymorphic value, (c) lets you write functions
with plain pattern matching. It is only when you need the extra
expressive power that you have to use the mapper.
For instance, here is your sprint function.

let rec sprint = function
  | Text str -> Printf.sprintf "(Text %s)" str
  | Bold seq ->
      Printf.sprintf "(Bold %s)" (List.fold_left (^) "" (List.map sprint seq))
  | Href str -> Printf.sprintf "(Href %s)" str
  | Mref (str, seq) ->
      Printf.sprintf "(Mref %s %s)" str
        (List.fold_left (^) ""
           (List.map sprint (seq :> [`Link|`Nonlink] Node.t list)));;

Here a coercion is needed to allow both `Link and `Nonlink in
input. This would not be necessary if I had written
"Mref of string * 'a t list" in the definition, rather than
"Mref of string * [`Nonlink] t list" like I did. But being more
specific also means that you have more information when you unwrap an
Mref node.

Cheers,

Jacques Garrigue