Re: [Caml-list] environment idiom

[skaller <skaller@users.sourceforge.net>]

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?

I think I am saying something like this: if you claim

	"Mine is bigger"

what would you say? Bigger than what? A comparative needs two
arguments or it is meaningless.

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"

Of course I'm not implying a strict stratification by the
use of the word "level", merely ignorance of the proper
way to structure the statement.

> main :: [Response] -> [Request]
> 
> In a pure language, main is obviously pure as well. And still, _given
> the proper "invocation" from an impure language_, it allows for I/O.

I have seen theoretical models of functional languages where
an imperative machine calculates functions -- an interactive
interpreter that is entirely lazy isn't much use :)

So at the top level, the system isn't functional,
but for each individual calculation it is.

However this is a fairly primitive and boring situation.
Monadic Haskell, and Ocaml, are far more interesting
because the interactions are more complex.

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 ..]

In addition, you can say that the procedural code is actually
functional, since it works by resumptions, a style of continuation
passing where code executes for a while then returns a new
continuation. In some places, it is the same object, modified,
and in others a clone is made first, so that it really is
purely functional -- with respect to that continuation at least.


> To paraphrase: Does the mere existance of a "magic main invocation"
> (whether a streaming-main or an IO monadic-main) make a language
> impure, in your concept?

If the 'magic main' is part of the semantic specification yes,
otherwise no.. and clearly here the division is quite plain
and well defined. 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.

> Again I believe we are talking about different kinds of "purity".
> Thomas is obviously right in that the StateTransformer monad (modulo
> unsafe conversions) is pure, you are obviously right in the
> (different) point that _running_ an IO fragment has side effects.

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.

> Generally, I'm not sure whether it's sensible to qualify other
> people's statements as "unquestionably bogus". Everything is relative
> <wink> :)

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.

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 -- 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.

So given the utility of transparency for reasoning,
one might find some styles of monad preserved transparency,
even in their higher levels of interpretation, whilst
other did not. And that would be valuable, since it would
be a way to guide the choice of techniques, whereas
a bland 'it is all transparent and pure' fails to
provide sufficient distinctions.

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.

Obvious example -- references are 'safer' if you keep their
scope local -- for example I do this a lot, and whilst it
isn't pure it is not too bad:

	let f x = 
		let a = ref 0 in
		for i = 1 to x do incr a done;
		!a

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?

-- 
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