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