Re: [Caml-list] environment idiom

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

On Sun, 2004-12-12 at 13:36, William Lovas wrote:
> On Sun, Dec 12, 2004 at 10:56:38AM +1100, skaller wrote:
> > The bottom line is that given an environment E
> > 
> > 	f: A -> B
> > 
> > is not functional if f fiddles with environment E.
> > It is absurd then to think that
> > 
> > 	f: E * A -> E * B
> > 
> > is suddenly purely functional, just because the environment
> > is now made explicit.  [...]
> 
> I'm not sure i buy this: if f returns the same result every time it's
> called with the same argument, and calling f cannot affect the behavior of
> any other part of your progrem, then in what way is f not purely
> functional?

It is, my point is simply that the mere recharactisation
of an function modifying its environment, to one accepting
and returning its environment, clearly isn't very useful
in determining how 'nice' the function f is.

Clearly, the encoding of f is unchanged .. the fact is,
in the first typing E is every bit an argument, it just
happens to be implicit.

I mean in general, the input E might be persistent,
in which case the two constructions are semantically
distinct. However if the input E is never reused --
which is guaranteed in the first formulation, they're
the same.

> > A final example. Ocaml *is* purely functional. As long
> > as you consider references as values -- rather than what
> > they refer to. In reality, it's just a state transformer
> > monad like Haskell, only the encoding is built in to
> > the language.
> 
> But there exist "functions" in O'Caml whose behavior is not always the same
> for a given argument, namely (!).  Does Haskell have such "functions"?

Yes it does, inside the state transformer monad for example.
The question is whether monadic code is actually Haskell code,
and of course that's an absurd question .. :)

I have a Scheme interpreter written in Ocaml .. if I 
use to execute Scheme code, is the code Scheme or Ocaml?

I don't want an answer .. the question is rhetorical,
it's obviously BOTH. The real question is about encoding
structure: clearly the meaning of code depends on context
in a subtle way.

> You're blurring some definitions fairly substantially when you say things
> like "Haskell is not purely functional, but O'Caml is" :)

Yes, that indeed is my intention. Basically, any non-transparent
non-function code can be made purely functional and transparent
with a simple transformation, yet it doesn't by this transformation
get any easier to reason about the code.

So taken on its own, 'purely functional' is of no real
importance. Anything is purely functional if you want
to consider it that way.

In order to *actually* make an argument that referential
transparency makes it easier to reason about program semantics,
it seems to me we need some more context.

As another example, there is no difference in the ability
to reason about a purely functional tail recursive exposition
of a loop, and an actual loop construction -- there cannot
possibly be, since they're equivalent -- the best one can
say is the the tail-rec method is *harder* to reason about,
since you need to first establish if a call is tail-rec,
which is manifest in a procedural loop.


A paper on SSA (single assignment form) I read recently
shows that it isn't suprising SSA is easy to work with,
since it can be shown to be equivalent to a purely functional
construction using continuation passing.

So, the many equivalences between stateful and functional
programming suggest functional programming simply does NOT
have a necessary advantage purely from being purely functional,
particularly if you're just emulating procedural code,
as is possible in a Haskell monad. Its clear the monadic code has
no advantage over the emulated procedural code since they're
semantically equivalent.

I'm not saying purely function/referentially transparent
is useless in respect of reasoning ability, I'm saying
it just isn't enough to say 'the code is better because
it is purely functional'. That isn't enough to gain the
advantages .. something more is needed to make this
claim carry through. I don't know exactly what.. :)

Crude example: OCS scheme interpreter (OCaml code) +
Scheme program (Data) --> functional code.
Yet: Scheme interpreter (Ocaml code) + Scheme program 
(Scheme code) => NOT functional. Ie. it depends trivially
on whether you label the Scheme inputs to the interpreter
as data or code. But all data is just an encoding ..

So perhaps the question is more like: given a low level
purely functional code, how far up the abstraction heirarchy
can you push the dividing line between data and code until
the result loses purity/transparency?

This should give a better indication how easy it will
be to reason about semantics: if you lose purity early,
it will be hard, if the whole system is pure all the way,
perhaps it will be easier. The point is there is no longer
any issue of code being 'purely functional' qualitatively, 
instead the question is quantitative.

As an example you might apply this analysis to MetaOcaml
programs. Is MetaOcaml code easier/harder to reason about
if the outermost metalevels of the code are functional,
and any procedural code is reserved for the innermost
(last generated) levels?

Actually, MetaOcaml is a pretty good example of what I'm
talking about since you can say it is functional
for the first several expansions and then becomes procedural,
and actually *count* the number of metalevels.

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