Dirk Thierbach a écrit :
> On Mon, Feb 25, 2008 at 10:23:09AM +0100, Tiphaine.Turpin wrote:
>   
>> I will try to state at an abstract level what I would like to do :
>>
>> - define parametric virtual classes A and B so that every A has a Bs 
>> (one or many...) and vice-versa.
>> - possibly extend A and B to A' and B' respectively, so that every A' 
>> has B's (and not just Bs), etc.
>> - subtyping: possibly extend B to B1 and B2 so that their objects have 
>> As, but those As still have Bs, so that I can associate the same A to 
>> objects of class B, B1 or B2.
>>
>> - and the ultimate goal combining all that: define A and B as above, 
>> other virtual classes C and D in a similar way and E and F too, and 
>> define concrete classes X Y Z1 Z2 just by saying that X extends A, Y 
>> will play the role of B in the first two classes and the role of C in 
>> the last two ones, and Z1 Z2 extends D (both) and E and F 
>> (respectively). It happens that some of the types that were left 
>> parametric (respectively methods defined as virtual) in B are made 
>> concrete in C, (and so on), so I obtain my final concrete classes.
>>     
>
> If you manage to find a simple type system for that, preferably with
> type inference and principal typings, I'd like to see it :-)
>   

I made more extensive tests with my class extension problem, using only 
classes, and with a quite acceptable overhead for the programmer (no 
modules, no need to write row types by hand). So I'm giving the state of 
my understanding in this very long mail. I hope this will be of interest 
to the many of you who answered my questions and therefore contributed 
to it. The following is about achieving the programming schemes 
described above ; don't expect any concrete examples here, as I still 
have to try that and see wether it is any usefull for programming. 
Actually there are even almost no methods (especially virtual) in what 
follows, but I think this doesn't change the rules too much.

First, here is a way to define two classes a and b as above (the kind of 
link here is one to one association, but this is not important since the 
concern is about typing).

class ['b] a = object
  constraint 'b = _ #b

  val b : 'b option ref = ref None
  method set_b b' = b := Some b'
  method get_b = match ! b with
    | Some b -> b
    | None -> raise Not_found

end

and ['a] b = object
  constraint 'a = _ #a

  val a : 'a option ref = ref None
  method set_a a' = a := Some a'
  method get_a = match ! a with
    | Some a -> a
    | None -> raise Not_found

end

So the two classes are parameterized by the type of the objects they are 
associated with. Furthermore this type parameter is constrained to be an 
instance of the open type of the other class, as suggested by Remi 
Vanicat. This seemed very counter-intuitive to me to give an open type 
to the content of a reference (which I expect to be invariant). But it 
works with that, and not with the close type (the definition works, but 
extension doesn't).

More generally, when defining a set of related classes, each one should 
be parameterized by the classes it is direcly linked with.

A very strange thing happens when type-checking this: the constraint 'b 
= _ #b is replaced with the stronger constraint 'b = 'b #a #b (and 
symetrically in class b). I still don't understand why it happens, but 
it is close to what we would like to express. A simpler (stronger) 
constraint that one could think of is something like 'self = 'self b a 
(which is not allowed) or writing unparameterized recursive classes, but 
this is too strong for some usages, because then we cannot associate 
objects of type a with objects of a subtype of b. So I view the 
constraint 'a = 'a #a #b as meaning a similar thing except that "an 
object a may see itself with a stronger type than its associated object 
b sees a". So, this definition will allow subtyping of either of the two 
classes, or both.

Note that instead of the above choice of parameters, one can use the 
whole set of all related classes to parameterize each one. This works 
too. However, parameterizing each class just by itself (which should 
concentrate all parameters in a single one) leads to very different 
results: first, the above "magic" constraint does not appear, even if we 
declare (an adapted version of) it explicitely. Is it somewhat implied ? 
Anyway, this version produces a typing bug when using the resulting 
classes with coercions (bug #00004505). So, for me, the above version 
seems to be the best solution at this time.

The above classes work (i.e., type-checks) as expected:

let x = new a
and y = new b

let _ =
  x#set_b y;
  y#set_a x;
  x = x#get_b#get_a && y = y#get_a#get_b

The compatibility of the two classes is checked too at some level, but 
not completely. Precisely the methods used on one side and declared on 
the other side are checked to be compatible (so that we cannot forget 
argumets or things like that) but the actual existence of a used method 
is not checked. Conjecture: if any concrete classes declared as above 
type-check, then they may be extended in such a way that the connection 
of two new objects will type-check). However, there is a way to enforce 
the existence of used methods, for example with the following code:

let _check _ : 'b a * ('b a b as 'b) = new a, new b

This is similar to the ckecks suggested by Jacques Garrigue and Julien 
Signoles (except that no functors are involved). This works only for 
concrete classes, and this is not ideal since this only appears as a 
challenge and not in the types of the classes themselves, but this is a 
good start. Note that the onstraint 'a = 'self a would work if the two 
classes were not recursive. However, the obtained classes could not be 
extended. With mutually recursive classes, we get a "Self type cannot 
escape its class" error.

Things like the following may also work (but I'm not sure wether it is 
equivalent). Extension of a' and b' is not possible then.

class virtual ['b] a' = object (self : 'self)
  inherit ['b] a
  constraint 'b = 'self b
end

class virtual ['a] b' = object (self : 'self)
  inherit ['a] b
  constraint 'a = 'self a
end

The following code extends a and b "simultaneously", in the sense that 
a2 knows that the object it would get by calling self#get_b is of type 
b2, and thus has a compatible method bar.

class ['b] a2 = object
  constraint 'b = _ #b2

  inherit ['b] a
  method foo = ()

end

and ['a] b2 = object
  constraint 'a = _ #a2

  inherit ['a] b
  method bar = ()

end

The constraints are re-stated in terms of the new classes in order to 
check the compatibility of new methods. Here is an example of error that 
would have been detected:

    method bar = self#get_a#foo ()
                 ^^^^^^^^^^^^^^
This expression is not a function, it cannot be applied

We can also repeat the second check:

let _check _ : 'b a2 * ('b a2 b2 as 'b) = new a2, new b2


The two new classes may be used without trouble, as for the first two 
ones. Another extension we can do is to make several subclasses of one 
of our classes, say b:

class ['a] b' = object

  inherit ['a] b
  method foo = ()

end

and ['a] b'' = object

  inherit ['a] b
  method bar = ()

end

This time, we don't add any new constraint to class a, since it must 
still accept b objects of class b, as we want to be able to connect 
objects of classes both b' and b''. Here is an example:

let x = new a
and y1 = new b'
and y2 = new b''

let _ =
  x#set_b (y1 :> _ b);
  y1#set_a x;
  x#set_b (y2 :> _ b);
  y2#set_a x

let _ =
  x = x#get_b#get_a && (y2 :> _ b) = y2#get_a#get_b

Of course we don't even need to define classes for that. We could have 
used immediate objects. Back to extension, the following is an example 
where a and b are the same class:

class ['c] c = object
  inherit ['c] b
  inherit ['c] a
end

Here is an example of use with subtyping:

let x = object inherit [_] c method foo = () end
and y = object inherit [_] c method bar = () end

let _ =
  x#set_b (y :> _ c);
  x#set_a (y :> _ c);
  y#set_b (x :> _ c);
  y#set_a (x :> _ c)

let _ =
  (y :> _ c) = x#get_a
  && (y :> _ c) = x#get_b
  && (x :> _ c) = y#get_a
  && (x :> _ c) = y#get_b

let _ =
  (x :> _ c) <> (y :> _ c)

Rather that closing the association link  on itself we may also combine 
two instances of it (this would also work for two differents pairs of 
classes):

class ['j] i = object
  inherit ['j] a
  constraint 'j = (_, _) #j
end

and ['i, 'k] j = object
  inherit ['i] b
  inherit ['k] a
  constraint 'i = _ #i
  constraint 'k = _ #k
end

and ['j] k = object
  inherit ['j] b
  constraint 'j = (_, _) #j
end

let _check _ : 'j i * (('j i, 'j k) j as 'j) * 'j k = new i, new j, new k

This time, the check looks more complex. And finally, the complete 
example described at the top:

class ['b] a = object
  constraint 'b = 'b #a #b

  val b : 'b option ref = ref None
  method set_b b' = b := Some b'
  method get_b = match ! b with
    | Some b -> b
    | None -> raise Not_found

end

and virtual ['a] b = object
  constraint 'a = 'a #b #a

  val a : 'a option ref = ref None
  method set_a a' = a := Some a'
  method get_a = match ! a with
    | Some a -> a
    | None -> raise Not_found

  method virtual foo : _
end

(* The following cannot be checked, because b is virtual
let _check _ : 'b a * ('b a b as 'b) = new a, new b
*)

class ['d] c = object
  constraint 'd = _ #d

  val d : 'd option ref = ref None
  method set_d d' = d := Some d'
  method get_d = match ! d with
    | Some d -> d
    | None -> raise Not_found
  method foo = ()

end

and ['c] d = object
  constraint 'c = _ #c

  val c : 'c option ref = ref None
  method set_c c' = c := Some c'
  method get_c = match ! c with
    | Some c -> c
    | None -> raise Not_found

end

let _check _ : 'd c * ('d c d as 'd) = new c, new d

class ['f] e = object
  constraint 'f = _ #f

  val f : 'f option ref = ref None
  method set_f f' = f := Some f'
  method get_f = match ! f with
    | Some f -> f
    | None -> raise Not_found

end

and ['e] f = object
  constraint 'e = _ #e

  val e : 'e option ref = ref None
  method set_e e' = e := Some e'
  method get_e = match ! e with
    | Some e -> e
    | None -> raise Not_found

end

let _check _ : 'f e * ('f e f as 'f) = new e, new f

class ['y] x = object
  inherit ['y] a
  constraint 'y = (_, _) #y
end

and ['x, 'z] y = object
  inherit ['x] b
  inherit ['z] c
  constraint 'x = _ #x
  constraint 'z = _ #z
end

and ['y] z = object
  inherit ['y] d
  constraint 'y = (_, _) #y
end

and ['y, 'z2] z1 = object
  inherit ['y] z
  inherit ['z2] e
end

and ['y, 'z1] z2 = object
  inherit ['y] z
  inherit ['z1] f
end

let _check _ : 'y x * (('y x, 'y z) y as 'y) * ('y, 'z2) z1 * (('y, ('y, 
'z2) z1) z2 as 'z2) = new x, new y, new z1, new z2

let x = new x
and y = new y
and z1 = new z1
and z2 = new z2

let _ =
  x#set_b y;
  y#set_a x;
  y#set_d (z1 :> _ z);
  z1#set_c y;
  y#set_d (z2 :> _ z);
  z2#set_c y;
  z1#set_f z2;
  z2#set_e z1

Here, the checks are becomming hard to write however. Note that both the 
type and implementation of foo were unspecified in b, and this was later 
fixed by inheriting from c.

In a real use, each of the successive extensions would probably go in a 
dedicated file. I hope that this will allow me to modularize my code 
some day :-).

Tiphaine Turpin