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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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