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 A615CBB81 for ; Sun, 12 Dec 2004 06:33:36 +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 iBC5Xae7009222 for ; Sun, 12 Dec 2004 06:33: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 GAA11743 for ; Sun, 12 Dec 2004 06:33:35 +0100 (MET) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBC5XXH0009212 for ; Sun, 12 Dec 2004 06:33:34 +0100 Received: from [192.168.1.200] (ppp203-65.lns1.syd3.internode.on.net [203.122.203.65]) by smtp1.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id iBC5XT0r012771; Sun, 12 Dec 2004 16:03:30 +1030 (CST) Subject: Re: [Caml-list] environment idiom From: skaller Reply-To: skaller@users.sourceforge.net To: William Lovas Cc: caml-list In-Reply-To: <20041212023636.GA12724@force.stwing.upenn.edu> 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> <20041212023636.GA12724@force.stwing.upenn.edu> Content-Type: text/plain Message-Id: <1102829608.2768.77.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 12 Dec 2004 16:33:29 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41BBD830.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41BBD82D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 lovas:01 wrote:01 wrote:01 semantically:01 reused:01 ocaml:01 haskell:01 o'caml:01 haskell:01 monadic:01 ocaml:01 o'caml:01 semantics: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 Sun, 2004-12-12 at 13:36, William Lovas wrote: > On Sun, Dec 12, 2004 at 10:56:38AM +1100, skaller wrote: > > The bottom line is that given an environment E > > > > f: A -> B > > > > is not functional if f fiddles with environment E. > > It is absurd then to think that > > > > f: E * A -> E * B > > > > is suddenly purely functional, just because the environment > > is now made explicit. [...] > > I'm not sure i buy this: if f returns the same result every time it's > called with the same argument, and calling f cannot affect the behavior of > any other part of your progrem, then in what way is f not purely > functional? It is, my point is simply that the mere recharactisation of an function modifying its environment, to one accepting and returning its environment, clearly isn't very useful in determining how 'nice' the function f is. Clearly, the encoding of f is unchanged .. the fact is, in the first typing E is every bit an argument, it just happens to be implicit. I mean in general, the input E might be persistent, in which case the two constructions are semantically distinct. However if the input E is never reused -- which is guaranteed in the first formulation, they're the same. > > A final example. Ocaml *is* purely functional. As long > > as you consider references as values -- rather than what > > they refer to. In reality, it's just a state transformer > > monad like Haskell, only the encoding is built in to > > the language. > > But there exist "functions" in O'Caml whose behavior is not always the same > for a given argument, namely (!). Does Haskell have such "functions"? Yes it does, inside the state transformer monad for example. The question is whether monadic code is actually Haskell code, and of course that's an absurd question .. :) I have a Scheme interpreter written in Ocaml .. if I use to execute Scheme code, is the code Scheme or Ocaml? I don't want an answer .. the question is rhetorical, it's obviously BOTH. The real question is about encoding structure: clearly the meaning of code depends on context in a subtle way. > You're blurring some definitions fairly substantially when you say things > like "Haskell is not purely functional, but O'Caml is" :) 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. So taken on its own, 'purely functional' is of no real importance. Anything is purely functional if you want to consider it that way. In order to *actually* make an argument that referential transparency makes it easier to reason about program semantics, it seems to me we need some more context. As another example, there is no difference in the ability to reason about a purely functional tail recursive exposition of a loop, and an actual loop construction -- there cannot possibly be, since they're equivalent -- the best one can say is the the tail-rec method is *harder* to reason about, since you need to first establish if a call is tail-rec, which is manifest in a procedural loop. A paper on SSA (single assignment form) I read recently shows that it isn't suprising SSA is easy to work with, since it can be shown to be equivalent to a purely functional construction using continuation passing. So, the many equivalences between stateful and functional programming suggest functional programming simply does NOT have a necessary advantage purely from being purely functional, particularly if you're just emulating procedural code, as is possible in a Haskell monad. Its clear the monadic code has no advantage over the emulated procedural code since they're semantically equivalent. I'm not saying purely function/referentially transparent is useless in respect of reasoning ability, I'm saying it just isn't enough to say 'the code is better because it is purely functional'. That isn't enough to gain the advantages .. something more is needed to make this claim carry through. I don't know exactly what.. :) Crude example: OCS scheme interpreter (OCaml code) + Scheme program (Data) --> functional code. Yet: Scheme interpreter (Ocaml code) + Scheme program (Scheme code) => NOT functional. Ie. it depends trivially on whether you label the Scheme inputs to the interpreter as data or code. But all data is just an encoding .. So perhaps the question is more like: given a low level purely functional code, how far up the abstraction heirarchy can you push the dividing line between data and code until the result loses purity/transparency? This should give a better indication how easy it will be to reason about semantics: if you lose purity early, it will be hard, if the whole system is pure all the way, perhaps it will be easier. The point is there is no longer any issue of code being 'purely functional' qualitatively, instead the question is quantitative. As an example you might apply this analysis to MetaOcaml programs. Is MetaOcaml code easier/harder to reason about if the outermost metalevels of the code are functional, and any procedural code is reserved for the innermost (last generated) levels? Actually, MetaOcaml is a pretty good example of what I'm talking about since you can say it is functional for the first several expansions and then becomes procedural, and actually *count* the number of metalevels. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net