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 E3EA0BB81 for ; Mon, 13 Dec 2004 10:56:41 +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 iBD9ufll011617 for ; Mon, 13 Dec 2004 10:56:41 +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 KAA23946 for ; Mon, 13 Dec 2004 10:56:41 +0100 (MET) Received: from rproxy.gmail.com (rproxy.gmail.com [64.233.170.194]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBD9ue3b011612 for ; Mon, 13 Dec 2004 10:56:40 +0100 Received: by rproxy.gmail.com with SMTP id c16so1379538rne for ; Mon, 13 Dec 2004 01:56:39 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:references; b=j7S1SukgPvIc8ZPGUET6xyB2aoEHBsBuToVViApuffZvk7aVVCS4Q+HqbVY9xx8TtPMH8UgTELqOYZkJW4JCDQvcV7fd0eSMx7w0uqvQ/NTWHsALGagOeQWdfOmEcsXSMS95hDzK9BIAeEsy0aQmwJNtayc7PJ8VmEo1xntZOe4= Received: by 10.38.90.74 with SMTP id n74mr605536rnb; Mon, 13 Dec 2004 01:56:39 -0800 (PST) Received: by 10.38.86.10 with HTTP; Mon, 13 Dec 2004 01:56:39 -0800 (PST) Message-ID: <877e9a17041213015616bff817@mail.gmail.com> Date: Mon, 13 Dec 2004 04:56:39 -0500 From: Michael Walter Reply-To: Michael Walter To: skaller@users.sourceforge.net Subject: Re: [Caml-list] environment idiom Cc: caml-list In-Reply-To: <1102918715.2768.240.camel@pelican.wigram> Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit References: <9410EC84C0872141B27A2726613EF45D02A52E08@psmrdcex01.psm.pin.safeco.com> <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> <1102918715.2768.240.camel@pelican.wigram> X-Miltered: at nez-perce with ID 41BD6759.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41BD6758.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 wrote:01 monadic:01 monadic:01 computations:01 monads:01 invocations:01 main':01 monads:01 haskell:01 computations: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=RCVD_BY_IP autolearn=disabled version=3.0.0 X-Spam-Level: On 13 Dec 2004 17:18:36 +1100, skaller wrote: > 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? > [..] > 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" Right. But very often (such as in "mine is bigger" <0.5 wink>), the comparison argument ("the context") is obvious and/or has a typical meaning: If you say that "monadic programming allows side effect free transparent purely functional encoding of state", most people will understand what you are talking about (the State monad allows apparent stateful computations, but can be purely functionally encoded). You are stressing a different but no less obvious point of monads, in this example that a State monad models state (i.e. you have apparent statefulness *inside* the monad). > 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 ..] Can I read about the reasoning behind this on felix.sf.net? > [...] 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. Indeed (and Monads give you an attractive way to partly do this the other way around). > 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. Are there specific statements, for instance on the Haskell home page, which you dislike? Or do you dislike that fact that for instance in the statement "Monads allow for sideeffect free encoding of stateful computations" everyone is assuming that "encoding" refers to the encoding in the target language? > 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. Okay, I was thinking (along the lines of the paragraph above) that you were unhappy about the way that people are talking about monads. > 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. Okay. So far I have never been confused by such statements about monads -- it was usually pretty clear what "pure" was referring to (Of course stateful computations deal with state, that is the very point of them. But OTOH it is very obvious that calling the State monad "pure" does not talk about computations *inside* the State monad, but about the *outside* view -- if you run a computation in the State monad, the result _purely_ depends on the arguments of runState). > ... 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. Sure. > 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. I'm not an O'Caml programmer but I think I know what you mean. > 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? Yep. This also seems very natural -- the more localized the (potential and actual) effects, the easier to reason about (you can reason about smaller chunks of code, so to say). 4;56 AM-ly yours, Michael