unique abstract types functional?

[Fergus Henderson]

On 29-Jul-1999, Gert Veldhuijzen van Zanten <veldhvz@ipo.tue.nl> wrote:
> 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.

The specification for an abstract data type should state the intended
semantics for that ADT precisely, though not necessarily completely;
that is, it is OK if some aspects are unspecified, so long as it is clear
which aspects are specified and which are deliberately left unspecified.
If the semantics of the abstract type are stated precisely, then it
should be straight-forward to construct an appropriate mathematical model.

So for ADTs either you do have a mathematical model, or if not then it
should be easy to construct one.

> Thus, in the presence of abstract types, we cannot define equality even 
> in the mathematical sense. 

This inference (we don't have mathematical models, therefore we can't
define equality in the mathematical sense) is incorrect;
it is based on a false premise.

> > 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").

Yes, I think that's what he meant.

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

No, this is incorrect.  The claim of pure functionality holds, and is
meaningful, even if it is not _directly_ testable, because you can test
it indirectly.

For example, if I have an ADT

	data Foo
	bar :: Int -> Foo
	baz :: Foo -> Int

then you may not be able to directly test the condition "x = y ==> f x = f y"
for the case where "f" is "bar".  But you *can* test this condition for the
case where "f" is "\ x -> baz (bar x)".  So the claim that this ADT is
purely functional is not a vacuous claim -- it does have testable consequences.

The same applies for function types -- you can't test equality of function
types directly, but equality of functions does have testable consequences
in general.

-- 
Fergus Henderson <fjh@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@128.250.37.3        |     -- the last words of T. S. Garp.