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