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 CD882BB81 for ; Mon, 13 Dec 2004 07:18:46 +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 iBD6IkV0002783 for ; Mon, 13 Dec 2004 07:18:46 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id HAA17485 for ; Mon, 13 Dec 2004 07:18:46 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iBD6IhfI002780 for ; Mon, 13 Dec 2004 07:18:45 +0100 Received: from [192.168.1.200] (ppp203-65.lns1.syd3.internode.on.net [203.122.203.65]) by smtp3.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id iBD6Ib7D028849; Mon, 13 Dec 2004 16:48:37 +1030 (CST) Subject: Re: [Caml-list] environment idiom From: skaller Reply-To: skaller@users.sourceforge.net To: Michael Walter Cc: caml-list In-Reply-To: <877e9a1704121218456af9df9@mail.gmail.com> References: <9410EC84C0872141B27A2726613EF45D02A52E08@psmrdcex01.psm.pin.safeco.com> <20041211181313.GA9656@fichte.ai.univie.ac.at> <1102809398.2611.637.camel@pelican.wigram> <20041212023636.GA12724@force.stwing.upenn.edu> <1102829608.2768.77.camel@pelican.wigram> <877e9a170412121109ec02d44@mail.gmail.com> <1102898935.2768.88.camel@pelican.wigram> <877e9a17041212180365f76e4a@mail.gmail.com> <877e9a170412121805295e4704@mail.gmail.com> <877e9a170412121844b633bb8@mail.gmail.com> <877e9a1704121218456af9df9@mail.gmail.com> Content-Type: text/plain Message-Id: <1102918715.2768.240.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 13 Dec 2004 17:18:36 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 41BD3446.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41BD3443.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 monadic:01 invocation:01 lazy:01 monadic:01 haskell:01 ocaml:01 invocations:01 invocation:01 main':01 main':01 haskell:01 abstraction: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, 2004-12-13 at 13:45, Michael Walter wrote: > > The claims that monadic programming allows side effect > > free transparent purely functional encoding is unquestionably > > bogus. > In your view, would claiming that the stream approach allowed that be > bogus as well? I think I am saying something like this: if you claim "Mine is bigger" what would you say? Bigger than what? A comparative needs two arguments or it is meaningless. With that idea in mind, any claim that X is transparent is automatically bogus without context, you really need to say instead "X is transparent at the Y level" Of course I'm not implying a strict stratification by the use of the word "level", merely ignorance of the proper way to structure the statement. > main :: [Response] -> [Request] > > In a pure language, main is obviously pure as well. And still, _given > the proper "invocation" from an impure language_, it allows for I/O. I have seen theoretical models of functional languages where an imperative machine calculates functions -- an interactive interpreter that is entirely lazy isn't much use :) So at the top level, the system isn't functional, but for each individual calculation it is. However this is a fairly primitive and boring situation. Monadic Haskell, and Ocaml, are far more interesting because the interactions are more complex. Another example is my Felix language. It has both functions and procedures. Functions aren't allowed to have side effects, yet they're not pure in the sense the result can depend on variables which change between (but not during) invocations. [This has an alarming effect on the optimiser ..] In addition, you can say that the procedural code is actually functional, since it works by resumptions, a style of continuation passing where code executes for a while then returns a new continuation. In some places, it is the same object, modified, and in others a clone is made first, so that it really is purely functional -- with respect to that continuation at least. > To paraphrase: Does the mere existance of a "magic main invocation" > (whether a streaming-main or an IO monadic-main) make a language > impure, in your concept? If the 'magic main' is part of the semantic specification yes, otherwise no.. and clearly here the division is quite plain and well defined. Clearly you can reason about the 'functional subsystem' using transparency, and then combine the result with reasoning about the top level 'magic main' where the program as a whole is not transparent ... and you still have 'ease of reasoning' in the combination. > Again I believe we are talking about different kinds of "purity". > Thomas is obviously right in that the StateTransformer monad (modulo > unsafe conversions) is pure, you are obviously right in the > (different) point that _running_ an IO fragment has side effects. Yes, but that is precisely the point. In wishing to avoid the kind of hype normally associated with OO and Java, I think it is necessary to reconsider exactly what crude statements like 'it is pure and transparent' actually mean. > Generally, I'm not sure whether it's sensible to qualify other > people's statements as "unquestionably bogus". Everything is relative > :) It was actually *my* statement that I labelled 'unquestionably bogus', namely that Haskell (including all monadic programming) is pure and transparent (and side effect free) when clearly any kind of I/O at the OS level is not. However the claim is not *wrong*, instead I'm claiming it isn't a well formed formula: 'pure' is a predicate that has to be applied to a particular level of encoding, and then you can reason about that level using that property -- but that isn't enough to reason about correctness, since it invariably means checking the program meets some specification given at a much higher level of abstraction. So given the utility of transparency for reasoning, one might find some styles of monad preserved transparency, even in their higher levels of interpretation, whilst other did not. And that would be valuable, since it would be a way to guide the choice of techniques, whereas a bland 'it is all transparent and pure' fails to provide sufficient distinctions. Since I'm not a Haskell programmer it is hard to give examples, but for Ocaml I'm sure we all know that some uses of imperative programming technique feel 'safer' than others. They threaten purity less. But this is just waffle. I'd like to have a better guideline. Obvious example -- references are 'safer' if you keep their scope local -- for example I do this a lot, and whilst it isn't pure it is not too bad: let f x = let a = ref 0 in for i = 1 to x do incr a done; !a Why are localised uses of mutation less of a threat to reasoning than less localised ones? Because it's encapsulated in the function .. but that is a waffle explanation .. how about more general theoretical account of this phenomena? -- 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