unique abstract types functional?
Dr. Mark E. Hall
mehall@mut.ac.th
Sat, 7 Aug 1999 12:56:46 +0700 (GMT+0700)
On Mon, 2 Aug 1999, Fergus Henderson wrote:
> 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.
Thank you. This was my feeling, too, but I am not an expert on abstract
data types, so I did not argue with Gert.
> > > 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.
Yes and no. I should not have tried to be too concise. The precise
undecidability result I was refering to was the following: If A and B
are infinite types (such as [char]), then there is no algorithm to
determine whether or not two functions of type A -> B are equal. Thus,
if fun is of type T -> A -> B for some type T, and x1 and x2 are of
type T, then there is no algorithm for determining whether or not
(fun x1) = (fun x2). So yes, the function fun that is being tested
for pure functionality is a higher-order function, but the functions
which cannot be tested algorithmically for equality need not be
higher-order.
>
> > 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.
I would go even further and say that pure functionality is a semantic
property of the language, and thus we can determine whether or not a
language (or even just a single given function) is purely functional
as long as we have a complete description of the language's formal
semantics, although it may be necessary to use a particular type of
formal semantics, such as denotational semantics. I will say more about
this in a moment, but first I need to address another issue in this
discussion.
On Thu, 29 Jul 1999, Gert Veldhuijzen van Zanten wrote:
[snip]
> 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.
[snip]
> 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.
I would say that the need be able to check the equality (or inequality)
of function arguments is an illusion, as the following example shows.
Consider the following fragment of C code:
int external_influence = 0;
int f(void *x)
{
external_influence++;
return external_influence;
}
Clearly the function f above is not purely functional, since successive
calls to f return the values 1, 2, 3,..., regardless of what arguments
are passed to f. And yet, by using C's typecasting mechanism, f's argu-
ment can be a pointer to an object of any type whatsoever, including
one for which we cannot determine equality. (We could always use
pointer equality, but in most cases we really want to be able to
check the equality of the objects pointed to.)
The problem arises from the attempt to give a simple, concise statement
of the property of being purely functional. In the discussion so far,
all of us (including myself) have been saying that a function f is
purely functional if for all x and y (of the appropriate type) we have
x = y ==> f x = f y,
and then that a language is purely functional if every function that
can possibly be written in that language is purely functional (I am
changing things a bit, so that I can talk about the pure functionality
of individual functions, but I think everyone would agree that what I
just wrote is equivalent to what we have been using so far). However,
pure functionality is really about whether or not putting in the same
argument always yields the same function value. Written precisely in
words, it would go something like this:
The function f is purely functional if for all x (of the
appropriate type), f x always returns the same value in
all situations.
In particular, when we check whether or not f x always returns the
same value, for a fixed value of x, we can use that same x repeatedly,
so it is not necessary to check whether or not it is equal to some
other value. However, we must be able to check whether or not the
various computations of f x return the same value, so it is necessary
that equality be defined for values in the return type of f.
Perhaps the confusion arises because if we tried to write my definition
above as a short, symbolic statement, it would come out like this:
for all x, f x = f x,
and our intuition from elementary mathematics tells us that this should
always be true, because an expression should always equal itself. Of
course, as computer scientists we know that this is not correct (for
example, f x = f x would be false for the C example I gave above), but
by writing it as
for all x and y, x = y ==> f x = f y,
the use of f x and f y on the right-hand side makes it easier to see
that they might be different.
As I wrote above, I think the property of being purely functional
should really be expressed using the formal semantics of the language
in question. I have a way of expressing it using denotational semantics,
but this posting is getting rather long, and this topic is no longer
very closely related to Clean, so perhaps I should not talk about it
on this discussion list. However, anyone who is interested is welcome
to contact my privately.
Finally...
On Mon, 2 Aug 1999, Gert Veldhuijzen van Zanten wrote:
> However, as soon as we add interfaces to the non-functional world
> (see discussion on "World als Value") pure functionality is easily
> compromised.
I certainly agree with you on this point. Even though I apparently do
not worry about abstract data types as much as some other people, I
do not feel comfortable with the "world as value" approach to I/O.
The model described by Peter Achten in his thesis is very complicated,
and as soon as you get such a complex model you run the risk of over-
looking something important, especially when your model tries to mate
the nonfunctional world with the functional world.
Mark
________________________________________________________________________________
Mark E. Hall
Mahanakorn University of Technology
Vanit Building 2, 8th Floor
1126/1 New Petchburi Road
Bangkok 10400, Thailand
66-2-6553181--7
mehall@mut.ac.th
http://www.mut.ac.th/~mehall