Re: [Caml-list] About polymorphic methods and recursive classes

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Sebastien Briais <sebastien.briais@epfl.ch>

> >Actually no. Polymorphic methods are not inferred, but declared.
> >And polymorphic type variables should not be used as parameters to
> >simultaneously defined types.
> >Actually, your mutually recursive definition should not be accepted to
> >begin with. It clearly results in a wrong internal type.
> >
> So, if I understand you well, it is not possible to write something like 
> that in ocaml:
> 
> class virtual ['a,'b] list_visitor =
> object
>   method virtual caseNil : 'a
>   method virtual caseCons : 'b -> 'b list -> 'a
> end
> and virtual ['b] list =
> object
>   method virtual visit : 'a.(('a,'b) list_visitor -> 'a)
> end

Right.
The only workaround I see is to unroll the recursion:

class type ['a,'b,'c] list_visitor_t = object
  method caseNil : 'a
  method caseCons : 'b -> 'c -> 'a
end
class type ['b] alist = object
  method visit : 'a. ('a,'b,'b alist) list_visitor_t -> 'a
end
class type ['a,'b] list_lisitor = ['a,'b,'b alist] list_visitor_t

class ['b] nil = object (_ : 'b #alist)
  method visit x = x#caseNil
end

class ['b] cons h t = object (_ : 'b #alist)
  method visit x = x#caseCons h t
end

I agree this is not a very intuitive solution.

> But what is the reason of this limitation ?
> I do not see the reasons since for example, in Generic Java, such a 
> definition is correct.

Generic Java is another language, and it does not have ML-style type
inference. It is very hard to compare. There are lots of tricks you
can do with type inference that you cannot do with a fully declared
language.

For those who remember old discussions about loss of polymorphism in
mutually recursive type definitions in earlier versions of caml, this
is related: in order to propagate type constraints, type variables in
class definitions are only generalized after then end of the whole
definition, which in this case is too late.

You can also see this as bug, and not so easy to fix.

> Can you explain in more details your answer ?
> Does it lead to type insafety or indecidability of typing to authorize 
> polymorphic type variables to be used as parameters to
> simulteanously defined types ?

According to the target you choose, this can probably lead to
indecidabilty. There should be some reasonnable solution,
avoiding going too far, but the interaction with constraints is going
to be really hard to avoid.
I was unaware of this problem until it was posted on this list.

Jacques Garrigue

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners