Polymorphic recursion 9Was Re: [Caml-list] Doubly-linked list)

[Brian Rogoff <bpr@artisan.com>]

Diego Olivier Fernandez Pons writes:
> Brian Rogoff a écrit :
> > With OCaml 3.05 and above, you'll be able to use polymorphic methods to 
> > get non-uniform recursion. This issue has come up a lot on the list 
> > (see the archives) over the years and several proposals were made for 
> > adding this capability to the language. I don't know if adding this 
> > feature is a priority for the developers; it isn't clear that the data
> > structures in Okasaki's book constitute a strong enough argument for 
> > adding it. 
> 
> Non-uniform recursion allows you to capture structure invariants in
> your type, which means that the correction of the algorithms will not
> be proved by the programmer but by the type-checker. 

Oh I'm not arguing that point, I totally agree that it's omission is a 
bad thing. However, not everyone agrees, since you it becomes a lot tougher
to build a monomorphizing compiler if you allow it, though it has been 
suggested that the same tricks you use to manually remove polymorphic
recursion could be used in an SSC (sufficiently smart compiler). 

Anyways, since OCaml 3.05 allows first class polymorphism on records, you
don't even need to use "polymorphic recots" to get non-uniform recursion; 
simply mapping the OOP to records does the trick. Here's the first example
from OKasaki which uses polymorphic recursion, done in OCaml with this 
direct approach 

module type RANDOM_ACCESS_LIST =
  sig
    type 'a ra_list

    val empty   : 'a ra_list
    val is_empty : 'a ra_list -> bool

    val cons    : 'a -> 'a ra_list -> 'a ra_list
    val head    : 'a ra_list -> 'a
    val tail    : 'a ra_list -> 'a ra_list
    val lookup  : int -> 'a ra_list -> 'a
    val update  : int -> 'a -> 'a ra_list -> 'a ra_list
  end

module AltBinaryRandomAccessList : RANDOM_ACCESS_LIST =
  (* assumes polymorphic recursion! *)
  struct 
    type 'a ra_list = Nil
    | Zero of ('a * 'a) ra_list
    | One of 'a * ('a * 'a) ra_list

    let empty = Nil
    let is_empty = function Nil -> true | _ -> false

    (* Use first class polymorphism to get the effect of explicitly typing 
       the polymorphic recursion 
    *)
    type dictionary = 
      { cons : 'a. dictionary -> 'a -> 'a ra_list -> 'a ra_list;
	uncons : 'a. dictionary -> 'a ra_list -> 'a * 'a ra_list;
	lookup : 'a. dictionary -> int -> 'a ra_list -> 'a;
	fupdate : 'a. dictionary -> ('a -> 'a) -> int -> 'a ra_list -> 'a 
ra_list
      }

    (* Define the methods, taking care that the recursive calls go through
       the dictionary
    *)

    let cons' dict x l =
      match l with
	Nil -> One (x, Nil)
      | Zero ps -> One (x, ps)
      | One (y,b) -> Zero (dict.cons dict (x, y) b)

    let uncons' dict l =
      match l with
	Nil -> raise Not_found
      | One (x,Nil) -> (x,Nil)
      | One (x,ps) -> (x, Zero ps)
      | Zero ps -> 
	  let ((x,y),ps') = dict.uncons dict ps in 
	  (x, One (y, ps'))

    let lookup' dict i l = 
      match i,l with 
	(i, Nil) -> raise Not_found
      | (0, One (x, ps)) -> x
      | (i, One (x, ps)) -> dict.lookup dict (pred i) (Zero ps)
      | (i, Zero ps) -> 
	  let (x, y) = dict.lookup dict (i / 2) ps
	  in if i mod 2 = 0 then x else y

    let rec fupdate' dict f i l =
      match i,l with 
	(i, Nil) -> raise Not_found
      | (0, One (x, ps)) -> One (f x, ps)
      | (i, One (x, ps)) -> dict.cons dict x (dict.fupdate dict f (i-1) (Zero 
ps))
      | (i, Zero ps) ->
	  let f' (x, y) = if i mod 2 = 0 then (f x, y) else (x, f y) in 
	  Zero (dict.fupdate dict f' (i / 2) ps)


    (* Make the sole dictionary which will be called *)

    let methods = 
      { cons = cons'; uncons = uncons'; lookup = lookup'; fupdate = fupdate' }

    (* Make the actual functions *)
    let cons x l = cons' methods x l 
    let uncons l = uncons' methods l 
    let head xs = let (x, _) = uncons xs in x
    let tail xs = let (_, xs') = uncons xs in xs'
    let lookup i xs = lookup' methods i xs
    let update i y xs = fupdate' methods (fun x -> y) i xs
  end

> I think it is a big improvment. Chris Okasaki's data structure may not
> be a strong enough argument, but more complicated data structures are
> being studied.

I agree, and I hope that in the future we won't have to use hacks like the 
above to get polymorphic recursion, but that it will be supported more
directly. The style above, besides being indirect, is also a little uglier
still when you're using the tail recursive accumulator passing style
because your recursive functions have funny names and signatures. In any
case, this kind of hack will allow you to translate these structures and
won't require much rework when polymorphic recursion is finally added 
"for real"

-- Brian
-------------------
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