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 072A6BB81 for ; Mon, 13 Dec 2004 10:29:30 +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 iBD9TTTJ006819 for ; Mon, 13 Dec 2004 10:29:29 +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 KAA23054 for ; Mon, 13 Dec 2004 10:29:29 +0100 (MET) Received: from rproxy.gmail.com (rproxy.gmail.com [64.233.170.197]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iBD9TSmj006805 for ; Mon, 13 Dec 2004 10:29:28 +0100 Received: by rproxy.gmail.com with SMTP id b11so846263rne for ; Mon, 13 Dec 2004 01:29:24 -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=IY3vVDPekAxKqeeL6tUPjIVi+LQNOqdyQ3/bIyApoCT1ElPEtH/CZSc6mGfKGbgqyoaZWk3WQEMsRiK4mLsEEFBq7Q4K+GVe1BlTl8dmXHdViZ2DmDuz74aoO8Ji2P593L7UjJK4LOjb5VZbfrrlNo4o5+GXmAuhLbtl7+hwiIs= Received: by 10.38.68.47 with SMTP id q47mr1916823rna; Mon, 13 Dec 2004 01:29:24 -0800 (PST) Received: by 10.38.86.10 with HTTP; Mon, 13 Dec 2004 01:29:24 -0800 (PST) Message-ID: <877e9a17041213012926f7e18a@mail.gmail.com> Date: Mon, 13 Dec 2004 04:29:24 -0500 From: Michael Walter Reply-To: Michael Walter To: skaller@users.sourceforge.net Subject: Re: [Caml-list] environment idiom Cc: William Lovas , caml-list In-Reply-To: <1102916483.2768.204.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> <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> <1102916483.2768.204.camel@pelican.wigram> X-Miltered: at nez-perce with ID 41BD60F9.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41BD60F8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 implements:01 abstraction:01 haskell:01 monads:01 haskell:01 programmer's:01 ocaml:01 monads:01 ...:98 desiring:98 contrast:01 idiom: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 16:41:23 +1100, skaller wrote: > [...] > 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. Agreed. > 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. What is "the detail level"? Like the "language level" in contrast to the level of the current abstraction (for instance, State monad)? Different note: I think you are missing out an important property of the functional encoding, which is its purity wrt composability. Suppose one of the few obvious types of the sieve, for instance: sieve :: Integer -> [Integer] You can clearly see that the sieve is a pure function, and actually the type system proves this for you (modulo cheating, err, unsafePerformIO et al). This makes it very easy and safe to use the function (and also to test it, btw!). In constrast, in a language such as C++ you cannot assume that.. vector sieve(unsigned); has no side effects. Also consider the "print" part of your algorithm, which I ignored so far. In C++ it would be very easy to add it to sieve() thus making the function virtually useless to use but in the special case where you want to print the number instantly. In Haskell, you *could* have a sieve :: Integer -> IO [Integer], but what you would really do is to decouple the sieve and I/O (and this is made kinda "attractive" by the expressiveness of the language and the type system). So what you would do is something like: printPrimes :: Integer -> IO () printPrimes :: mapM_ print . sieve (modulo obvious types made at 4 AM :-) There is also an interesting point about algorithms which I'm sure you are aware of. Often when analyzing algorithms for their correctness, you reason about the state before and after a certain step in the algorithm. That is, you make the state and its change explicit. Sounds like sieveStep :: State -> State, huh? :-) I think that is also what makes monads in Haskell attractive. They are very nice to use from a programmer's perspective (IMO), but they also allow good reasoning (as they are usually purely defined or at least definable). > 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. Yep! Monads actually allow nice embedding of many paradigms, not only the imperative. 4:29 AM-ly yours, Michael