unique abstract types functional?

[Gert Veldhuijzen van Zanten]

Mark E. Hall wrote:
>
> ...                                       
> all methods for describing semantics that I know of are based on
> mathematics, with the data values operated on by the language being
> elements of some set (usually a domain). In particular, all of the
> data values are modelled as mathematical objects, and therefore the
> standard mathematical equality relation is used to determine whether
> or not two data values are equal. In short, since we have to give
> mathematical models for all data values the language uses---including
> all values in all abstract types---when we describe the semantics of
> the language, there is no problem about equality, because the equality
> relation is defined for all mathematical objects.

The point is that for abstract types we do NOT have mathematical models.
This is so, even if we define the abstract type as an instance of 
the equality class, so that == is defined for it.
Thus, in the presence of abstract types, we cannot define equality even 
in the mathematical sense. 

> Having said that, I should point out that I am a mathematician by
> training, and, although I have now shifted my research interests
> to computer science, I still tend to view things from a mathematical
> perspective. However, I think that in this case at least, the mathe-
> matical perspective is quite appropriate. Also, if one rejects the
> mathematical perspective, then the situation is even worse than Erik
> originally suspected, because equality of functions is undecidable.
> Thus, if one insists on an equality that (in principle, at least) can
> be checked computationally, there will be certainly be problems if
> the values of fun are functions, because there will be no way to
> check whether or not (fun x1) = (fun x2).

This one I can't follow. Unless you mean that equality of higher order
functions cannot be checked. (i.e. by "the values of fun are functions"
you mean "the result type of fun is a function").

Now what does this give us. We are dealing with a language in which
the equality of functions can only be approximated. For the basic
types and structured types (types with constructors, records, lists and 
arrays) the relations is defined, and for functions and abstract types
we rely on token identity as an approximation. This language can be said
to be purely functional if for all expressions x, y and f, we have that

	x = y  ==>  f x  =  f y

So, the requirement is that for those x and y for which we can decide
that
x = y we should be able to decide whether f x is equal to f y.
Otherwise,
the claim of pure functionality is void. The problem that Mark pointed
out,
of the undecidability of function equality in general, is btw not a
proof
that the claim does not hold, because we clearly have a special case
here.
If f has no way to distinghuish x from y, it cannot return a different 
function for x than for y. Pure functionality thus heavily depends on
the
absense of mechanisms to distinghuish two situations that do not depend
on the inequality in the function arguments.
For abstract types this argument turns into a trivial one in which no 
cases can be found in which the pure functionality could be disproved.
That is in my view indeed unfortunate. It would be nice to have a means
to define axioms that hold for abstract types, and some way to prove the 
correctness of the implementation of the abstract types wrt these
axioms.
Equality of abstract types could also be defined through these axioms.

-- 
Gert Veldhuijzen van Zanten      P.O. Box 513, NL-5600 MB  Eindhoven
 ____________________________    +31 40 2475260, fax: +31 40 2431930
| IPO, Center for Research   |                    veldhvz@ipo.tue.nl
|_on User-System Interaction_|  http://www.tue.nl/ipo/people/veldhvz