[m-dev.] diff: det_report.m: report error for nondet functions

[Fergus Henderson]

Thomas Charles CONWAY, you wrote:
> Fergus Henderson, you write:
> > compiler/det_report.m:
> > 	Report an error if a "forward" mode of a function,
> > 	(a mode for which all the arguments are fully input)
> > 	has determinism nondet, multi, cc_nondet or cc_multi.
> > 	Such functions should be illegal because they break
> > 	referential transparency.
> 
> What do you mean by "referential transparency" in this context, and
> why is a nondet function not referentially transparent?

If you want the long answer, see Harald's paper on determinacy and
referential transparency.  If you want the short answer,
I mean being able to substitute equals for equals, e.g.
replacing a variable with its value.

For example, if I have

	q :-
		X = f(a),
		p(X, X)

then that should be equivalent to

	q :-
		p(f(a), f(a)).

but the two are not equivalent if f/1 is a nondeterministic function,
and p/2 is defined by e.g.

	p(X, Y) :- X \= Y.

> Are predicates "referentially transparent"? Why/Why not?

Yes.  This may be suprising, since predicates and functions are
just different syntax for the same thing, but the reason why this
is can be the case is that referential transparency _is_ a syntactic quality.
(Imperative languages and functional languages are just different syntax
for the same thing too, but only the latter can be referentially transparent.)

Roughly speaking, the problem with nondeterministic functions is
that it is not clear when the nondeterminism should happen; simple
transformations such as replacing a variable with its value change
the semantics, because values might be nondeterministic.  In
contrast, with predicates this problem doesn't arise.  You cannot turn

	q :-
		f(a, X),
		p(X, X).

into

	q :-
		f(a, X),
		f(a, Y),
		p(X, Y).

by replacing equals with equals.

[For more on this topic, try a dejanews search for
"Fergus Henderson comp.lang.functional referential transparency",
in DejaNews's OLD database.]

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.