[Caml-list] implicit subtyping fails with recursive classes

[Caml-list] implicit subtyping fails with recursive classes

[Goswin von Brederlow]

Hi,

I'm trying to add implicit subtyping to a pair of recurisve classes:

Without subtyping:
------------------
class type foo = object method foo : t -> unit end
and t = object method push : foo -> unit end

With that I can call t#push (x :> foo) for any x that implements the
foo interface.


What I want:
------------
# class type foo = object method foo : t -> unit end
and t = object method push : 'a . (#foo as 'a) -> unit end;;
                             ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The universal type variable 'a cannot be generalized:
       it escapes its scope.



The problem seems to be the recursive definition with "and". Here is
an example with and without "and":

(* works *)
class type foo = object method foo : string end;;
class type bar = object inherit foo method bar : string end;;
class type t = object method push : 'a . (#foo as 'a) -> unit end;;

(* fails *)
class type foo = object method foo : string end
and bar = object inherit foo method bar : string end
and t = object method push : 'a . (#foo as 'a) -> unit end;;


So what am I doing wrong?

MfG
	Goswin

Re: [Caml-list] implicit subtyping fails with recursive classes

[Leo White]

I am not sure, but I think the problem is that you are using #foo before
it is fully defined, so it is becoming unified with the universal 'a and
then when #foo is generalised the universal is escaping its scope.

One way to avoid the problem is to expand out the type of #foo:

  # class type t = object method push : 'b. (< foo : t -> unit; ..> as 'b) -> unit end;;
  class type t = object method push : < foo : t -> unit; .. > -> unit end
  # class type foo = object method foo : t -> unit end;;
  class type foo = object method foo : t -> unit end

if foo has a lot of methods, and you want to avoid typing them out
multiple times, you could try:

  # class type ['a] foo' = object method foo : 'a -> unit end;;
  class type ['a] foo' = object method foo : 'a -> unit end
  # class type t = object method push : 'b. (t #foo' as 'b) -> unit end;;
  class type t = object method push : t #foo' -> unit end
  # class type foo = [t] foo';;
  class type foo = [t] foo'

Regards,

Leo

Goswin von Brederlow <goswin-v-b@web.de> writes:

> Hi,
>
> I'm trying to add implicit subtyping to a pair of recurisve classes:
>
> Without subtyping:
> ------------------
> class type foo = object method foo : t -> unit end
> and t = object method push : foo -> unit end
>
> With that I can call t#push (x :> foo) for any x that implements the
> foo interface.
>
>
> What I want:
> ------------
> # class type foo = object method foo : t -> unit end
> and t = object method push : 'a . (#foo as 'a) -> unit end;;
>                              ^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: The universal type variable 'a cannot be generalized:
>        it escapes its scope.
>
>
>
> The problem seems to be the recursive definition with "and". Here is
> an example with and without "and":
>
> (* works *)
> class type foo = object method foo : string end;;
> class type bar = object inherit foo method bar : string end;;
> class type t = object method push : 'a . (#foo as 'a) -> unit end;;
>
> (* fails *)
> class type foo = object method foo : string end
> and bar = object inherit foo method bar : string end
> and t = object method push : 'a . (#foo as 'a) -> unit end;;
>
>
> So what am I doing wrong?
>
> MfG
> 	Goswin

Re: [Caml-list] implicit subtyping fails with recursive classes

[Goswin von Brederlow]

On Sat, Jul 20, 2013 at 08:06:43PM +0100, Leo White wrote:
> 
> I am not sure, but I think the problem is that you are using #foo before
> it is fully defined, so it is becoming unified with the universal 'a and
> then when #foo is generalised the universal is escaping its scope.
> 
> One way to avoid the problem is to expand out the type of #foo:
> 
>   # class type t = object method push : 'b. (< foo : t -> unit; ..> as 'b) -> unit end;;
>   class type t = object method push : < foo : t -> unit; .. > -> unit end
>   # class type foo = object method foo : t -> unit end;;
>   class type foo = object method foo : t -> unit end
> 
> if foo has a lot of methods, and you want to avoid typing them out

Yeah, the real code has rather a few more methods (9 occurances of t
in foo) so expanding out expands a lot. And since I'm still developing
the classes still change and then the change has to be copied to each
expanded type again. That is realy painfull.

> multiple times, you could try:
> 
>   # class type ['a] foo' = object method foo : 'a -> unit end;;
>   class type ['a] foo' = object method foo : 'a -> unit end
>   # class type t = object method push : 'b. (t #foo' as 'b) -> unit end;;
>   class type t = object method push : t #foo' -> unit end
>   # class type foo = [t] foo';;
>   class type foo = [t] foo'
> 
> Regards,
> 
> Leo

I came up with that idea independently, too. But I parameterized t
instead of foo. This causes and Assert_failure in the toplevel:

http://caml.inria.fr/mantis/view.php?id=6083

But the way you suggest with ['a] foo', t and foo works. Luckily so far I
only need subtyping in t.

The other idea to circumvent his I had was using recursive modules but
I haven't tried that.

MfG
	Goswin