It would be nice to be able to use recursive types without -rectypes. Not in general (accept too much bad programs with very strange type) but at least in one of the two case: - the recursive types are introduced by a recursive definition - the "loopin types" respects a positivity condition (I have no example of bad programs accepted with strange types in the case ... but this is probably because this is not implemented). Here is a nice program (that needs -rectypes) and this is a pitty :-) ---------- (* a very short representation of ordinals up to epsilon_0 as a fixpoint of list (remark: the are more than one representation for each ordinals: [[];[[]]] = [[[]]] != [[[]];[]] ) *) *) type ord = ord list let rec compare (o1:ord) (o2:ord) = match o1, o2 with | [], [] -> 0 | [], _ -> -1 | _, [] -> 1 | x::o1', y::o2' -> match compare x y with -1 -> compare o1' o2 | 1 -> compare o1 o2' | 0 -> compare o1' o2' let lesseq o1 o2 = compare o1 o2 <= 0 (* compute the simplest form of an ordinal*) let rec normalize (o1:ord) = let rec add l x = let x = normalize x in match l with [] -> [x] | y::l' -> if lesseq x y then x::l else add l' x in List.rev (List.fold_left add [] o1) let zero = ([] : ord) let un = ([[]] : ord) let deux = ([[];[]] : ord) let omega = ([[[]]] : ord) let deux_omega = ([[[]];[[]]] : ord) let omega_carré = ([[[];[]]] : ord) let omega_to_the_omega = ([[[[]]]] : ord) (* exercise: implements addition, multiplication and exponentiation of ordinals, as epsilon_0 is the smallest ordinals closed for these operation after omega *) --------- -- 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 --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature ---------------------------------------------