On Thu, 13 Mar 2003 10:56:56 +0900
Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp> wrote:

> From: Damien <Damien.Pous@ens-lyon.fr>
> 
> > Does someone know why the following class type
> > is not accepted ?
> > 
> > # class type a = object method m: 'a. (#a as 'a) -> unit end;;
> > The abbreviation #a expands to type #a but is used with type < .. >
> [...]
> Now, the serious part: can such a type be defined?
> After working a bit on this riddle, I'm afraid the answer is no.
> The reason is that there is no way to recurse on a quantified
> polymorphic method rather than on the whole object.
> The closest I found is:
>   class type a =
>     object method m : < d : 'b. (< m : 'a; .. > as 'b) -> unit > as 'a
>     end
> The dummy wrapper <d : 'b. ... > is just there to allow one to recurse
> on the polymoprhic method itself. You can call the method m by doing
> [a#m#d a'] in place of [a#m a'].
I worked with this class type, but it is a bit tedious :-(

My goal is to define a tree, whose node's type is a class
type a_t, containing a method for adding children.
but the child type can be any subtype of a_t

* this method can safely be typed [a_t->unit], but this will require a
lot of coercions in the rest of the code...

* that's why I wanted to type it ['a. (#a_t as 'a)->unit] (i.e. the
coercion is written only once, in the method)

 using your trick, I obtained the attached code. It works fine,
but that's not really a beautiful piece of code !



I don't know what do you mean when saying 
"such a type cannot be defined", in fact, I could define this 
equivalent (I think it is...) :

>#class type a_t = object 
>   method m: 'a.(<m: 'a -> unit; ..> as 'a) -> unit 
>end 

this class type definition being accepted, why is the former 
rejected ? 
both should be either rejected if this make no sense, or accepted else


then I tried to implement it, 
but I couldn't  do it "meaningfully" :

># class a: a_t = object
>   val mutable l = []
>   method m: 'a.(<m: 'a -> unit; ..> as 'a) -> unit = 
>     fun o -> l <- (o:>a_t) :: l
> end;;
>        Characters 116-117:
>      fun o -> l <- (o:>a_t) :: l
>                     ^
>This expression cannot be coerced to type
>  a_t = < m : 'a. (< m : 'a -> unit; .. > as 'a) -> unit >;
>it has type < m : 'b -> unit; .. > as 'b but is here used with type
>  'b = < m : 'c. < m : 'c -> unit; .. > -> unit; .. >.
>This simple coercion was not fully general. Consider using a double
>coercion.
>
>
># class a: a_t = object
>   val mutable l = []
>   method m: 'a.(<m: 'a -> unit; ..> as 'a) -> unit = 
>     fun o -> l <- (o:(<m: 'a -> unit; ..> as 'a):>a_t) :: l
> end;;
>
>        Characters 115-151:
>      fun o -> l <- (o:(<m: 'a -> unit; ..> as 'a):>a_t) :: l
>                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>Type < m : 'a -> unit; .. > as 'a is not a subtype of type
>  a_t = < m : 'b. (< m : 'b -> unit; .. > as 'b) -> unit > 
>The universal variable 'b would escape its scope


any idea ?


damien