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 11EB9BB81 for ; Mon, 13 Dec 2004 06:41:34 +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 iBD5fXAg008214 for ; Mon, 13 Dec 2004 06:41:33 +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 GAA16817 for ; Mon, 13 Dec 2004 06:41:32 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBD5fUug008209 for ; Mon, 13 Dec 2004 06:41:31 +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 iBD5fN7D004720; Mon, 13 Dec 2004 16:11:24 +1030 (CST) Subject: Re: [Caml-list] environment idiom From: skaller Reply-To: skaller@users.sourceforge.net To: Michael Walter Cc: William Lovas , caml-list In-Reply-To: <877e9a17041212180365f76e4a@mail.gmail.com> 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> <1102829608.2768.77.camel@pelican.wigram> <877e9a170412121109ec02d44@mail.gmail.com> <1102898935.2768.88.camel@pelican.wigram> <877e9a17041212180365f76e4a@mail.gmail.com> Content-Type: text/plain Message-Id: <1102916483.2768.204.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 13 Dec 2004 16:41:23 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41BD2B8D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41BD2B8A.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 bool:01 implements:01 haskell:01 haskell:01 monads:01 monadic:01 abstractions:01 abstraction:01 monads:01 inference:01 monadic:01 inference: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:03, Michael Walter wrote: > It is probably better to say "from the outside it is pure, and inside > it appears impure, relative to its boundary" (thus stressing the point > that your apparent impurity is only a "view" ). Perhaps so. > I think the problem is that we are using "pure" twofold here: Yes. But this is not all .. > a) As an (absolute) property of the language > b) As the property of code (which is relative to its environment) > > As you can obviously emulate impurity in a pure language (see State > monad), and code pure in a impure language, it is not much of a > surprise that b) can differ from a). Consider this example. We have an algorithm, such as: Take an array of bool length n initially all false. for i = 1 to n do if element i is false print i set every i'th element true Of course this is the Sieve. Now consider a procedural and functional implementation. We can ask: is the implementation *correct*? In this case, probably it is easier to reason about the correctness of the procedural implementation than the functional one (although I wouldn't bet on it :) We can also ask: is the algorithm correct? (At finding primes). That's a different question about a different level of the encoding. Finally we can ask: are the functional and procedural programs correct (at finding primes)? I am desiring to show here that 'the ability to reason about correctness' depends on what encoding of what you're asking the question about. Clearly even a functional encoding of the Sieve is still a procedural program at the level of calculating primes. However it is pure at the detail level. This only helps, and only perhaps helps, at reasoning if the code faithfully implements the algorithm -- if you try to reason about it's ability to calculate primes you inevitably have to account for the fact the algorithm isn't functional. So we're agreeing on the ideas, but we need some way to *distinguish* in a less informal way, that a Haskell program may not be as 'pure' at all levels as the detailed encoding is. Whilst this isn't restricted to Haskell, given monads it seems we can focus on the monadic parts to see what higher level abstractions they represent, and how pure they are, in the abstract, and thus make -- or find it harder to make -- judgements, depending on how 'transparent' that abstraction is. In other words, I guess Haskell monads are good, because not only do monads localise the code that needs this special consideration, but the typeclasses systematically present the structure, so you can extend your normal inference rules to cover the monadic code. It would seem than that for some monads, the extension inference rules would be harder to use since they don't include rules that require transparency. The advantage is that you can still reason about the code, and you can even say which inference rules can be applied where. This is probably harder to do in Ocaml, where the places that transparency is lost aren't so easy to find, and the effects on the whole program not quite so easy to isolate. -- 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