unique abstract types functional?

[Zuurbier, E. - AMSXE]

A language is purely functional if the function's result depends only on its
explicit input and on nothing else.

I seem to recall that this is expressed along the following lines:

For all x1, x2 and fun: if x1 = x2, then (fun x1) = (fun x2)

Clearly, equality is not the same as the == operator in Clean, as I could
give that any definition, including for instance <, which would invalidate
the above expression. If x1 and x2 have an abstract type, what does x1 = x2
mean? I cannot determine equality by inspection, as abstract types don't
allow that.

So maybe we ought to use pointer equality (if this is not a hilarious case
of mixing up theory and implementation). Then, if I don't trust a given
function fun, I could test to see whether its output ever differs. Assume
that x has an abstract type and that Initialize is defined to produce a
value of the type:

Start
	# x = Initialize 1.234
	= (fun x,fun x,fun x,fun x,fun x,fun x,fun x,fun x)

Now of course, if the outputs are all the same, this does not prove
anything, but if some differ, fun has clearly been exposed as
non-functional.

Then assume that the abstract type is also unique. Then I cannot even write
this test program! I must conclude that since you cannot express a test
program to expose fun to be non-functional, fun must be functional. Is this
true?

This e-mail was triggered by the 'world as value' discussion, as *World is a
unique abstract type. I must be mixing up very many different levels of
theory and implementation. Is there any hope of completely understanding
functional programming?

Erik Zuurbier





Erik Zuurbier
Application Architect, 
KLM, Information Services - AMSXE
phone: (+ 31) 20 64 96 255 
e-mail: erik.zuurbier@klm.nl