unique abstract types functional?

[Gert Veldhuijzen van Zanten]

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

What I meant was that the programming language itself does not require
the existence of a mathematical model. Of course, that does not exclude
the possibility of its existence. And I fully agree that good
programming practice calls for such models.

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

I would say that the inference is correct, as is the inference
"if all men can fly, then (since I am a man) I can fly" is a correct
inference, drawing the conclusion that I can fly may however not be
entirely valid.

The conclusion to draw here is that in order to define equality, we 
need a mathematical model of our abstract types. This can be
read as an invitation to programmers to write comments. 

{ snap ]

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

I never denied that there were consequences. The point is that by
definition of pure functionality, we require that for ALL functions f
we have that "x = y ==> f x = f y", not just for some. So indeed, if
a language is purely functional, then we have a nice property that
we have such consequences that you describe. However, proving rigorously
that the language is indeed purely functional requires the implication
to hold for ALL functions f.

Now, you DO have a good point. One I never intended to obscure.
Given mathematical models for abstract data types, that satisfy the
pure functionality constraint (all functions defined for the data type
are indeed pure), we can show that no inpure functions can be
constructed.
And as long as the implementation of abstract data types is done in 
Clean as well, the know that this constraint holds (whether it can be
computationaly tested or not).
However, as soon as we add interfaces to the non-functional world
(see discussion on "World als Value") pure functionality is easily
compromised.

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