Browse thread
[Caml-list] OCaml popularity
-
Graham Guttocks
- Gerd Stolpmann
-
Nicolas Cannasse
-
Pierre Weis
-
Guillaume Marceau
- David Brown
- Nicolas Cannasse
- Christophe Raffalli
- Graham Guttocks
- Tushar Samant
-
Guillaume Marceau
- Fred Yankowski
-
Pierre Weis
- Martin Weber
[
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 <Christophe.Raffalli@u...> |
| 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
---------------------------------------------