From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 2545BBB81 for ; Mon, 13 Dec 2004 13:01:31 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBDC1Ulh032064 for ; Mon, 13 Dec 2004 13:01:30 +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 NAA28154 for ; Mon, 13 Dec 2004 13:01:30 +0100 (MET) Received: from mail.physik.uni-muenchen.de (mail.physik.uni-muenchen.de [192.54.42.129]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBDC1TXD032059 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Mon, 13 Dec 2004 13:01:29 +0100 Received: from localhost (unknown [127.0.0.1]) by mail.physik.uni-muenchen.de (Postfix) with ESMTP id 58B3E20039; Mon, 13 Dec 2004 13:01:29 +0100 (CET) Received: from mail.physik.uni-muenchen.de ([127.0.0.1]) by localhost (mail.physik.uni-muenchen.de [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 28092-01-71; Mon, 13 Dec 2004 13:01:27 +0100 (CET) Received: from mailhost.cip.physik.uni-muenchen.de (kaiser.cip.physik.uni-muenchen.de [141.84.136.1]) by mail.physik.uni-muenchen.de (Postfix) with ESMTP id 2C21820036; Mon, 13 Dec 2004 13:01:27 +0100 (CET) Received: from eiger.cip.physik.uni-muenchen.de (eiger.cip.physik.uni-muenchen.de [141.84.136.54]) by mailhost.cip.physik.uni-muenchen.de (Postfix) with ESMTP id 19FAD26E87; Mon, 13 Dec 2004 13:01:27 +0100 (CET) Received: by eiger.cip.physik.uni-muenchen.de (Postfix, from userid 3092) id 139943CBC; Mon, 13 Dec 2004 13:01:27 +0100 (CET) Received: from localhost (localhost [127.0.0.1]) by eiger.cip.physik.uni-muenchen.de (Postfix) with ESMTP id 1134C2D686; Mon, 13 Dec 2004 13:01:27 +0100 (CET) Date: Mon, 13 Dec 2004 13:01:27 +0100 (CET) From: Thomas Fischbacher To: skaller Cc: Markus Mottl , Andrej Bauer , caml-list Subject: Re: [Caml-list] environment idiom In-Reply-To: <1102935187.2578.85.camel@pelican.wigram> Message-ID: References: <9410EC84C0872141B27A2726613EF45D02A52E08@psmrdcex01.psm.pin.safeco.com> <41B97FD7.50309@andrej.com> <1102732237.2611.580.camel@pelican.wigram> <41BB04D8.60405@andrej.com> <20041211181313.GA9656@fichte.ai.univie.ac.at> <1102809398.2611.637.camel@pelican.wigram> <1102901206.2768.127.camel@pelican.wigram> <1102935187.2578.85.camel@pelican.wigram> X-BOFH: Daemons did it MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: amavisd-new at physik.uni-muenchen.de X-Miltered: at nez-perce with ID 41BD849A.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41BD8499.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 wrote:01 monadic:01 beginners:01 monadic:01 grammar:01 distinctions:01 distinctions:01 sequences:01 haskell:01 sequences:01 foo:01 foo:01 subsumed:01 mutation:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Mon, 13 Dec 2004, skaller wrote: > I.e. a simplified Assembler. > > Is assmebler code functional? > > No of course not! > > Yes of course it is! Is is nothing more > than a function from registers to registers where ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > the instructions guarrantee you can't access the prior state. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > That's just the state monad .. :) That's not quite how I would describe the state monad to work. However solid the mental picture which you have of a brick may be, you will not be able to hit real people with it as with a real brick. You can, of course, have a solid mental picture of solidly hitting real people with a solid real brick. This transformation of "mental picture of a solid brick" to "real brick in a mental picture of something that involves a brick" is just monadic binding. I know all this may sound a bit hairsplitting, but it is precisely the necessity of this hairsplitting that makes it so difficult for beginners that have been poisoned by the imperative side of the force(TM) to get the idea behind the monadic approach. Back to the question: > Is assmebler code functional? After all, "code" can mean very different things here: a string that can be parsed in a given grammar, a sequence of instructions that are to be fed into a processor, an actually running programm, etc. Some people work hard to get the fine distinctions one has to make here into other people's heads. My impression is that your statements just work against these distinctions other people try to establish. > The point really is: what do you mean by purely functional? > I think the answer depends on context. I think the answer depends on properly wording the question! Can one express transformations on sequences of machine instructions in a functional language? ("Language" in the much broader sense than just "functional programming language, especially haskell"; rather: "using proper mathematical reasoning".) Sure, and this is in many aspects perhaps the best way to talk about such transformations. Do sequences of machine instructions of the type Ra = foo Rb Rc respect some "naive" substitution properties like e.g. Ra = foo Rb Rc Ra = foo Rb Rc --> Ra = foo Rb Rc The answer is, of course, that no one would expect this. These questions could not be any more different! What irks me is when such very different things are subsumed under a statement of the form "depends whether you ask this question in the outer or inner context". As it is a very different question you are asking! It does not depend on "context", but actually on the meaning you connect with the words which you use. So, can one do array mutation in haskell? Certainly not. Can one use haskell to talk about doing array mutations? For sure. But nothing more. Well, systems like hugs will actually behave in funny ways if especially plans to do IO appear in certain magical places, but this is an entirely different story. My point is that with statements like > Yes, that indeed is my intention. Basically, any non-transparent ^^^^^^^^^^^^^^^^^^^ > non-function code can be made purely functional and transparent ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > with a simple transformation, yet it doesn't by this transformation ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > get any easier to reason about the code. you are trying to "hit real people with mental bricks". > I'm sure you can implement this machine using the ST monad... I'm sure you can even do without. :-) -- regards, tf@cip.physik.uni-muenchen.de (o_ Thomas Fischbacher - http://www.cip.physik.uni-muenchen.de/~tf //\ (lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y) V_/_ (if (= x 0) y (g g (- x 1) (* x y)))) n 1)) (Debian GNU)