Re: polymorphic recursion

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

> In some languages (most notably Haskell and Miranda) it is possible
> to define a function that enjoys polymorphic recursion, i.e., the
> types of its recursive calls may be instances of the type scheme at
> which the function is defined.
> 
> Can you do the same in OCaml? I am aware of the tricks mentioned in
> the FAQ, but I would like to know if there is a cleaner way to do it,
> for example by providing a type signature.

To my knowledge, there is no direct way to do this. Part of the reason
is that type signatures have a different role in Haskell and ML: in
Haskell the type signature appears before its function, and restricts
it explicitely, while in ML you write it in an independent signature
file, which is not known when typing the function itself (signature
matching takes place after the type checking).

This does not matter very much in ML, since you explicitely decide
which functions recurse with which (in Haskell all definitions in a
module are a priori recursive), and there are only few examples really
needing polymorphic recursion.

To be complete on this point, in Objective Label method calls can be
polymorphically recursive:

# class r = object (self)
    method virtual m : 'a. 'a -> 'a
    method m x =
      let q = self#m true in
      let r = self#m 0 in
      x
  end;;
class r : object method m : 'a. 'a -> 'a end

Thanks to the mechanisms use for this inference, it would be easy to
provide polymorphic recursion for functions also, but we go back to
the ML problem: where do we write the signature ?

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