unique abstract types functional?

[Mark E. Hall]

On Fri, 2 Jul 1999, Maarten de Mol wrote:

> -----Original Message-----
> From: Zuurbier, E. - AMSXE <Erik.Zuurbier@KLM.NL>
> To: 'clean-list@cs.kun.nl' <clean-list@cs.kun.nl>
> Date: Friday, July 02, 1999 3:28 PM
> Subject: unique abstract types functional?
>
> >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.
> 
> You could consider an abstract type only functional *if* it has a 
> (hidden) implementation somewhere. You could then easily define equality 
> on a theoretical level, by exposing this implementation. This of course 
> doesn't work for the *World, but it will work for any user defined 
> abstract type. 

I've been thinking about this for a long time, and I'm still not sure I
have the answer, but I think I can say something useful and at least
halfway intelligent.

It seems to me that the property of being purely functional depends on
the semantics of the language; surely it should not depend on the
implementation, because that would leave open the possibility that one
implementation was purely functional while another one was not. Now,
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.

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 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?
> 
> I dunno. As far as programs manipulating the *World are concerned: 
> I am pessimistic. But if you leave out the *World, I think we can 
> completely understand functional programming (someday at least).

I have been following the 'world as value' discussion since the beginning,
too, and I have found it quite fascinating, but difficult to understand
at times as well. I downloaded a copy of Peter Achten's thesis a week or
two ago, and have started working my way through it. It's not exactly
east reading, but it has improved my understanding measurably already.
Perhaps if I can finish it I will understand everything clearly---or
perhaps I will just have new questions of a different kind!

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