From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA24233; Wed, 12 Mar 2003 17:58:00 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA24077 for caml-list@pauillac.inria.fr; Wed, 12 Mar 2003 17:57:59 +0100 (MET) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id RAA22482 for ; Tue, 11 Mar 2003 17:47:10 +0100 (MET) Received: from post.bourget.univ-savoie.fr (post.bourget.univ-savoie.fr [193.48.120.73]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h2BGlAX14853 for ; Tue, 11 Mar 2003 17:47:10 +0100 (MET) Received: from univ-savoie.fr (d85.lama.univ-savoie.fr [193.48.123.85]) by post.bourget.univ-savoie.fr (8.12.3/jtpda-5.4) with ESMTP id h2BGl0wJ003137 ; Tue, 11 Mar 2003 17:47:00 +0100 Message-ID: <3E6E131C.2040804@univ-savoie.fr> Date: Tue, 11 Mar 2003 17:47:24 +0100 From: Christophe Raffalli User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.1) Gecko/20020826 X-Accept-Language: en-us, en MIME-Version: 1.0 To: Guillaume Marceau CC: caml-list@inria.fr Subject: Re: [Caml-list] about -rectypes References: <200303111023.LAA09578@pauillac.inria.fr> <1047392843.16158.2192.camel@anquetil> X-Enigmail-Version: 0.65.2.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enigD55B7D0E39CE406F2107809F" X-Spam: no; 0.00; raffalli:01 univ-savoie:01 caml-list:01 -rectypes:01 openpgp:01 2440:01 3156:01 implemented:01 fixpoint:01 ord:01 savoie:01 chablais:01 73376:01 lama:01 enigmail:01 X-Attachments: type="application/pgp-signature" X-Spam: no; 0.00; raffalli:01 univ-savoie:01 caml-list:01 -rectypes:01 openpgp:01 2440:01 3156:01 implemented:01 fixpoint:01 ord:01 savoie:01 chablais:01 73376:01 lama:01 enigmail:01 X-Attachments: type="application/pgp-signature" Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enigD55B7D0E39CE406F2107809F Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit 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 --------------------------------------------- --------------enigD55B7D0E39CE406F2107809F Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.0.7 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQE+bhMcSQDyWB/+xBwRAu9OAKDg5tFCBU91SwVTeqsLHdmZi1E+jQCg0Puv XOL3E4pt7TOw5u2tggEci7I= =Yilo -----END PGP SIGNATURE----- --------------enigD55B7D0E39CE406F2107809F-- ------------------- 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