[Camllist] Cyclic ?!

Oleg

Michael Hicks

Oleg
 Markus Mottl
 Christophe Raffalli

Oleg
 John Max Skaller

Michael Hicks
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Christophe Raffalli <raffalli@u...> 
Subject:  [Camllist] Recursive types (Was Cyclic ?!) 
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 typechecker, 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 typechecker 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 typechecker 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 BourgetduLac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univsavoie.fr www: http://www.lama.univsavoie.fr/~RAFFALLI  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners