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 079A9BB81 for ; Mon, 13 Dec 2004 02:27:31 +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 iBD1RUva012728 for ; Mon, 13 Dec 2004 02:27:30 +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 CAA10627 for ; Mon, 13 Dec 2004 02:27:29 +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 iBD1RR9G030134 for ; Mon, 13 Dec 2004 02:27:28 +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 iBD1Ql7D032081; Mon, 13 Dec 2004 11:56:49 +1030 (CST) Subject: Re: [Caml-list] environment idiom From: skaller Reply-To: skaller@users.sourceforge.net To: Thomas Fischbacher Cc: Markus Mottl , Andrej Bauer , caml-list In-Reply-To: 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> Content-Type: text/plain Message-Id: <1102901206.2768.127.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 13 Dec 2004 12:26:47 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41BCF002.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41BCEFFF.002 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 transformers:01 pointless:01 reformulate:01 haskell:01 haskell:01 monadic:01 encodings:01 monads:01 combinators:01 combinator: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 10:03, Thomas Fischbacher wrote: > On Sun, 12 Dec 2004, skaller wrote: > > > So monadic programming with state transformers is NOT > > referentially transparent or purely functional at all. > > Actually, it is. :-) Actually it is pointless after I took the trouble to explain why this is not the case, to make such a bland statement. It seems you missed entirely my point. In some interpretation of the encoding it is self-evident -- which means it isn't open to question or contradiction -- that the code is NOT transparent. The issue is to reformulate the meaning of 'encoding' in such a way that the well-known advantages of transparency are preserved. There is no doubt WHAT SO EVER that Haskell programs doing I/O have side effects, for example. Yet Haskell per se, doesn't. How can this be? The point is to *rescue* the basic conception from the ridicule which, at the moment, it deserves. The claims that monadic programming allows side effect free transparent purely functional encoding is unquestionably bogus. It can only be reinstated by more carefully specifying exactly *which* encodings have those properties. In particular with monads the combinators themselves patently admit a higher level of encoding -- combinator encodings -- which are NOT transparent, even if the terms they manipulate and the combinator definitions are. This is a new result for me -- functional code, when abstracted to a higher level encoding, need not be functional. Perhaps this is already known, and if not it will take a real theoretician to state what I'm trying to say properly, but I have no doubt at all the intent, though stated vaguely, is correct. Hmm .. of COURSE it is already known. Indeed, languages like Ocaml have long been classed as ISWIM-like. Such a language is purely functional, when the handles of variables are treated as values, but is not, when the values of the variables themselves are admitted. The whole *point* of the technique is to preserve the functional code and provide a clean dividing line between the functional part and the mutable store. Indeed I would bet there is a monadic interpretation of this, which would give Haskell programmers Ocaml like references. The point here is that *even* in languages like Ocaml where references are used, lack of absolute transparency does not make reasoning suddenly impossible. Despite the lack of absolute transparency, it is still much easier to reason about Ocaml than C++. Why? Because the core really is functional, and somehow you can still reason about the code 'as if' it were functional, and obtain a result pertaining to correctness of the code, perhaps 'with some caveats'. In particular, I would gues it is possible to reason the code is *incorrect* assuming it is purely functional (ignoring the values of references) and have that result hold, even if references are used -- but I don't know for sure, it may be one has to restrict the rules of inference. Obviously one can show that: let f x = f (1::x) in let x = ref 0 in f !x will not terminate since we're invoking, in an eager language, a nonterminating purely functional function... so the presence of a reference is irrelevant. Of course this is a trivial example, perhaps COQ programmers know better how to separate the mutable fields out. -- 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