Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Troublesome nodes
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-07-14 (19:37)
From: Jeremy Yallop <jeremy.yallop@e...>
Subject: Re: [Caml-list] Troublesome nodes
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

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


     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

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

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 ]

in the implementation.