Re: [Caml-list] Wikipedia

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

On Mon, 2005-11-07 at 11:14 +0100, Andreas Rossberg wrote:
> "skaller" <skaller@users.sourceforge.net>:
> >
> > In fact there is a lot of misleading or missing stuff in Wikipoedia,
> > and there are also some excellent articles. Try
> >
> > [...]
> > Referential Transparency (totally wrong)
> 
> That article could well be more accurate and complete, but I don't see at
> all how you arrive at judging it "totally wrong".

It confuses purity with transparency. Purity is a semantic property
of functions. Transparency is a property of expressions. 

Particularly, it is applications which are transparent NOT functions.

A function is pure if it depends only on its arguments.

A expression is transparent if its evaluation does not vary
with time or place (more or less).

As I pointed out in the commentary, 'functions' are necessarily
and trivially transparent, since ALL constant terms are transparent.

The article obscures an important theorem: given 'suitable conditions',
an expression is transparent if the function part of all applications
in the expressions are pure. 

In particular, if ALL functions are pure (Haskell or Clean), then
ALL expressions are transparent.

I might add -- I know about this because at the moment,
Felix has the rule that functions may not have side effects.
But still, not all expressions are transparent because functions
can depend on variables .. so it matters when you evaluate them.
This cannot happen in Haskell because it has no variables.

I don't know what to call this kind of 'function' other
than 'impure', nor what to call the resultant expressions, 
but I am calling them 'semi-transparent'. 

What is actually interesting is that applications
of impure functions  are "transparent within a 
particular space/time locus".

The Felix optimiser uses this. For example:

	var x = 1;
	fun f(y:int)=> x + y; // impure
	val a = f 1;          // a = 2 at this point
	val b = a + a;        // b = 4
	x = 2;                // modify x
	val c = b;            // should be 4 not 6!

In this code, the optimiser knows it can inline to obtain

	val b = f 1 + f 1;

however the substitution

	val c = f 1 + f 1;

will give the wrong answer, since x has been modified -- 
so the expression f 1 is "transparent" in a certain part
of the control flow graph. Felix can follow only linear
sequence of val bindings, it gives up on branches,
assignments, and procedure calls: it is using simple
pattern matching, not a proper data flow analysis.

Anyhow, I hope my objection is clear: it is a serious
category error. 'transparency' is a property of terms
of the language -- bits of syntax. Purity is a property
of functions, not the terms which denote the function.

The coupling is vital, in the sense that transparency
allows you to examine a call such as:

	f (g (y) )

and know for sure without looking at ANY other code that
IF the expressions and subexpressions are transparent,
THEN you can rewrite the expression like, for example:

	let a = g (y) in f (a)

(or conversely) and numerous other rewrite rules,
without changing the semantics. To establish this
transparency in Ocaml you know to examine the
functions f and g to see if they're pure,
and it remains only to examine 'a' to see if it is
transparent (assuming f,g are function constants).

And here .. f and g are *of course* transparent,
when considered as expressions themselves -- whether
or not they're pure: all constants are transparent.

Transparent and pure are distinct concepts applying
to distinct categories of entity. The article is
therefore *totally* wrong. Purity and transparency
are nominally independent, they have to be connected
by a (language dependent) theorem. If you mess up
the meaning of these important words, there would
be no way to state this theorem, let alone prove it.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net