Note: there is a nice exercise at the end of the mail ...

There is a better solution then -rectypes that the developper could 
implement :

Let the us write recursive type annotation in programs, but
when doing the loop detection in the unification used by the 
type-checker, each loop should go
through a type variable that has been created by one of these type 
anotation.

So the only thing you have to add to the type-checker is a marker on 
type variables introduced by the user: if the user write (e : ... as 'a) 
then 'a is marked.

This mark is propagated by unification and the loop detection is 
modified as I suggested.

Therefore, the type-checker will not introduce recursive types by itself 
and the cost is not to much (I have in mind a unification algorithm 
using graph unification followed by loop detection, I do not know if 
this is what OCaml uses, but I guess it is).

--

By the way, here is a nice program using recursive types:
run l n where l is a list of functions from positive int to positive int 
and n is a nat will produce a list of int of size n such that all the 
functions in l are increasing on that list ...

The program prints the lists it tries before finding the good one.

Exercise: try to remove the need for -rectypes ... keeping the same 
algorithm.

--
(* an algorithm extracted (by hand) from the proof of Dickson's lemma *)
(* by C. Raffalli *)
(* compile with ocamlc -rectypes *)

let lem1 f e k =
   let rec k' x q = k (x : int) ((f,k')::q) in
   e k'

let lem2 f u x = lem1 f (u (x : int))

let rec dickson lf =
   match lf with
     [] -> (fun x k -> k x [])
   | f::lf -> lem2 f (dickson lf)

let rec extract n u k =
   match n with
     0 -> k []
   | x ->
     let k' l =
       match l with
	[] -> u 0 (fun x lx -> k [x,lx])
       |	(y, ly)::_ -> u (y+1) (fun z lz -> k ((z,lz)::l))
     in
     extract (x - 1) u k'

let weak_dickson lf n = extract n (dickson lf)

let rec decidable' acc = function
     (y, (ly : (((int -> int) * (int -> 'a -> 'c)) list as 'a)))::l ->
       match l with
	[] -> y::acc
       |	(x,(lx : 'a))::_ ->
	  let rec test lx' ly' =
	    match lx', ly' with
               [], [] -> decidable' (y::acc) l
	    | (((fx : int -> int),( kx : int -> 'a -> 'c))::lx'), (((fy : int -> 
int), (ky : int -> 'a -> 'c))::ly') ->
		if not (fx == fy) then failwith "bug: the function should be the same !";
		if fx x < fx y then
		  ky x lx' else test lx' ly'
	  in test lx ly

let print_list f l =
   List.iter (fun x -> print_int (f x); print_string ", ") l;
   print_newline ()

let count = ref 0

let reset () =
   print_string "Number of tries:"; print_int !count; print_newline ();
   count := 0

let decidable l =
   print_list fst l;
   incr count;
   decidable' [] l;


let run l n =
   let r = weak_dickson l n decidable in
   reset ();
   r
--



-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
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