Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

[Caml-list] OCaml popularity
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2003-03-12 (16:58) From: Christophe Raffalli Subject: Re: [Caml-list] about -rectypes
```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
---------------------------------------------

```