Re: [Caml-list] about -rectypes

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

[-- Attachment #1: Type: text/plain, Size: 2103 bytes --]

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

[-- Attachment #2: Type: application/pgp-signature, Size: 252 bytes --]