Re: Polymorphic recursion in modules - impossible?

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

From: Markus Mottl <mottl@miss.wu-wien.ac.at>

> Code example:
> ---------------------------------------------------------------------------
> module RA_List =
> struct
>   type 'a ra_list = Nil
>                   | Zero of ('a * 'a) ra_list
>                   | One of 'a * ('a * 'a) ra_list
> 
>   let rec cons x = function
>       Nil -> One (x, Nil)
>     | Zero ps -> One (x, ps)
>     | One (y,b) -> Zero (cons (x, y) ps)
> end
> ---------------------------------------------------------------------------
> 
> It is clear that this piece of code cannot compile because of the
> polymorphic recursion found in the last match of "cons".

There is a way to circumvent this using polymorphic methods in olabl.
This amounts more or less to what Pierre Weis calls "polymorphic
recursion by constraints".

(* Using olabl-2.01 *)

type 'a ra_list = Nil
  | Zero of ('a * 'a) ra_list
  | One of 'a * ('a * 'a) ra_list

class conser = object (self)
  method cons : 'a. 'a ->  'a ra_list -> 'a ra_list =
    fun x l ->
      match l with
	Nil -> One (x, Nil)
      | Zero ps -> One (x, ps)
      | One (y,b) -> Zero (self#cons (x, y) b)
end

You notice that the only reason to use an object here is to use
explicit polymorphism: this object has no value fields.
Then you can use it by defining your function cons as

	let conser = new conser
	let cons x l = conser#cons

Which gives you the expected:

	val cons : 'a -> 'a ra_list -> 'a ra_list = <fun>

OK, using a method call is a little bit inefficient, but the
type-checker is in fact ready to do it for any function, I just lack a
nice syntax to provide it...

Remark that you can also create a real object using this

class ['a] ra_obj = object (self)
  val l : 'a ra_list = Nil
  method get = l
  method private do_cons : 'b. 'b ->  'b ra_list -> 'b ra_list =
    fun x l ->
      match l with
	Nil -> One (x, Nil)
      | Zero ps -> One (x, ps)
      | One (y,b) -> Zero (self#do_cons (x, y) b)
  method cons x = {< l = self#do_cons x l >}
end

class ['a] ra_obj :
  object ('b)
    val l : 'a ra_list
    method cons : 'a -> 'b
    method get : 'a ra_list
  end

Cheers,
Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>