From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 82F0EBDDB for ; Sat, 27 Aug 2005 19:39:38 +0200 (CEST) Received: from hedwig1.umh.ac.be (hedwig2.umh.ac.be [193.190.193.73]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j7RHdcAR031823 for ; Sat, 27 Aug 2005 19:39:38 +0200 Received: from poincare (Debian-exim@pri-011.umh.ac.be [10.101.0.11]) by hedwig1.umh.ac.be (8.13.1/8.13.1) with ESMTP id j7RHdN3X1859714; Sat, 27 Aug 2005 19:39:23 +0200 Received: from [127.0.0.1] (helo=localhost ident=trch) by poincare with esmtp (Exim 4.52) id 1E92gx-00038K-Vr; Sat, 27 Aug 2005 17:34:00 +0200 Date: Sat, 27 Aug 2005 17:33:57 +0200 (CEST) Message-Id: <20050827.173357.20560607.debian00@tiscali.fr> To: "O'Caml Mailing List" Subject: Re: [Caml-list] Re: Parameter evaluation order From: Christophe TROESTLER In-Reply-To: <430F4AA5.5000803@univ-savoie.fr> <20050826141744.GC7595@gaia.cc.gatech.edu> <430F47F1.5020302@univ-savoie.fr> References: <430F0669.6050103@univ-savoie.fr> <430F0CCF.3030103@exomi.com> <430F4AA5.5000803@univ-savoie.fr> <20050826141744.GC7595@gaia.cc.gatech.edu> Organization: Universite de Mons-Hainaut (http://math.umh.ac.be/an/) X-Spook: Europol computer terrorism Fortezza SRI warfare STARLAN nuclear investigation airframe genetic X-Blessing: Om Ah Hum Vajra Guru Pema Siddhi Hum X-Operating-System: GNU/Linux (http://www.linux.org/) X-Mailer-URL: http://www.mew.org/ X-Mailer: Mew version 4.2.51 on Emacs 21.4 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Scanned-By: MIMEDefang 2.1 (www dot roaringpenguin dot com slash mimedefang) X-j-chkmail-Score: MSGID : 4310A55A.000 on nez-perce : j-chkmail score : X : 0/20 1 X-Miltered: at nez-perce with ID 4310A55A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 christophe:01 troestler:01 christophe:01 raffalli:01 raffalli:01 univ-savoie:01 monadic:01 gatech:01 appending:01 char:01 recursive:01 constructors:01 emphasizes:01 2005,:98 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: ** X-Spam-Status: No, score=2.3 required=5.0 tests=DNS_FROM_RFC_ABUSE, DNS_FROM_RFC_POST,FROM_ENDS_IN_NUMS autolearn=disabled version=3.0.3 On Fri, 26 Aug 2005, Christophe Raffalli wrote: > > Remark: clearly, a good proof system should not show the monadic > translation and hide it behind the scene ... Shouldn't a good proof system show the code to be correct regardless of the evaluation order of function args, records,...? After all, different evaluation orders may be interesting on different platforms and I think programs that rely on the evaluation order (say) of functions arguments to be correct are fragile -- they have a great potential to be broken at the first maintenance. On Fri, 26 Aug 2005, Fernando Alegre wrote: > > Ignoring efficiency concerns, may I suggest that the correct way to > build lists is by appending elements, not prepending them: > > # append('d', append('c', append('b', append('a', []))));; > - : char list = ['a'; 'b'; 'c'; 'd'] It is not. You have to respect their recursive definition, from which it is clear that "append" is not a primitive operation. The data structure that you contruct with "append" and deconstruct with "head" is a FIFO queue. I've been skimming through the discussion and basically I do not understand you guys who want a given evaluation order for function application, constructors,... First there is a way of imposing evaluation order of expressions if you need it and moreover, you are using a functional language which emphasizes immutability for which evaluation order does not matter... My 2¢, ChriS