Re: [Caml-list] Troublesome nodes

[Dario Teixeira <darioteixeira@yahoo.com>]

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