This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] Cyclic ?!
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2002-09-25 (07:09) From: Christophe Raffalli Subject: [Caml-list] 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
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

```