From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 87CD6BC8C for ; Tue, 1 Feb 2005 10:27:36 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j119RaNr019911 for ; Tue, 1 Feb 2005 10:27:36 +0100 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 KAA21984 for ; Tue, 1 Feb 2005 10:27:35 +0100 (MET) Received: from post.bourget.univ-savoie.fr (post.bourget.univ-savoie.fr [193.48.120.73]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j119RYNE024941 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO); Tue, 1 Feb 2005 10:27:35 +0100 Received: from [193.48.123.85] (d85.lama.univ-savoie.fr [193.48.123.85]) by post.bourget.univ-savoie.fr (8.12.3/jtpda-5.4) with ESMTP id j119RTnH026480 ; Tue, 1 Feb 2005 10:27:29 +0100 Message-ID: <41FF4B84.5030501@univ-savoie.fr> Date: Tue, 01 Feb 2005 10:27:32 +0100 From: Christophe Raffalli User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.2) Gecko/20040804 X-Accept-Language: en-us, en MIME-Version: 1.0 To: Xavier Leroy , caml-list@inria.fr Subject: Re: [Caml-list] cyclic types References: <7f8e92aa0501290415321a8e46@mail.gmail.com> <6b8a914205012905427c79cd85@mail.gmail.com> <7f8e92aa05012909335800c97@mail.gmail.com> <20050130103309.GD4213@yquem.inria.fr> In-Reply-To: <20050130103309.GD4213@yquem.inria.fr> X-Enigmail-Version: 0.85.0.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enig0FBC1CFAE8137249F7E0AD89" Content-Transfer-Encoding: 8bit X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang) X-Miltered: at concorde with ID 41FF4B88.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41FF4B86.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 caml-list:01 -rectypes:01 val:01 arises:01 recursive:01 recursive:01 cyclicity:01 unification:01 ocaml:01 annotation:01 X-Attachments: type="application/pgp-signature" name="signature.asc" name="signature.asc" X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enig0FBC1CFAE8137249F7E0AD89 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit > > let f x = x :: x > > where the author of that code really intended > > let f x = x @ x > > With -rectypes, the wrong definition (with ::) is accepted with type > > val f : ('a list as 'a) -> 'a list = > > and it's only when you try to apply f to a "normal" list that the > problem arises, with a hard-to-understand error message: > > f [1;2;3];; > ^ > This expression has type int but is here used with type 'a list as 'a > Why do you think 'a list as 'a is an <<"impossible" recursive types>> ? It is a very nice representation of ordinals up to epsilon_0 (curious, see the code below) Why not this restriction: accept a recursive type 't as 'a only if access to 'a in t needs to expand a definition. I mean, the cyclicity check at the end of unification could check that one traverses definition. I am not sure how OCaml treat type annotation, this will work only if the compiler does its best to use all type annotation. 'a list as 'a is illegal and let f x = x @ x is illegal type ord = ord list is legal (all type definition should be legal) let f (x:ord) = x @ x is legal code for curious: --------------------------8<---------------- (* need -rectypes *) (* a very short representation of ordinals up to epsilon_0 as a fixpoint of list *) type ord = ord list (* comparison: you must normalize ordinal before comparison *) 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 normal form of an ordinal*) let rec normalize (o1:ord) = List.sort (fun x y -> compare y x) (List.map normalize o1) let zero = ([] : ord) let un = ([[]] : ord) let deux = ([[];[]] : ord) let omega = ([[[]]] : ord) let deux_omega = ([[[]];[[]]] : ord) let omega_square = ([[[];[]]] : ord) let omega_to_the_omega = ([[[[]]]] : ord) let addition (o1:ord) (o2:ord) = o1 @ o2 let rec multiplication (o1:ord) (o2:ord) = match o1, o2 with [], _ -> [] (* zero * o2 = zero *) | _, [] -> [] (* o1 * zero = zero *) | ([]::o1'), _ -> (* (1 + o1') * o2 = o2 + o1' * o2 *) addition o2 (multiplication o1' o2) | _, ([]::o2') -> (* o1 * (1 + o2') = o1 + o1 * o2' *) addition o1 (multiplication o1 o2') | (o1''::o1'),(o2''::o2') -> (* (w^o1'' + o1')*(w^o2'' + o2') = w^(o1''+o2'') + o2'*w^o1'' + o1'*w^o2'' + o1'*o2' *) (addition o1'' o2'')::(multiplication [o1''] o2')@ (multiplication o1' [o2''])@(multiplication o1' o2') (* test *) let _ = compare [[]] [[];[]] let _ = compare [[[]];[]] [[];[[]]] let _ = compare [[[]]] [[];[[]]] let _ = compare omega_to_the_omega omega_square let _ = normalize [[];[[]]] let _ = normalize [[[];[]];[];[[]]] let quatre = multiplication deux deux let quatre_omega = multiplication omega quatre let big = normalize (multiplication omega_to_the_omega quatre_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. The public key is stored on www.keyserver.net --------------------------------------------- --------------enig0FBC1CFAE8137249F7E0AD89 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.2.4 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFB/0uFSQDyWB/+xBwRAhVKAKCo+HzU41RaMHi6oAFhi4QfgnjMhACg1cIh 9MBNpqjyH4zN25XUE1F/qJY= =nHN+ -----END PGP SIGNATURE----- --------------enig0FBC1CFAE8137249F7E0AD89--