🚀 go-pugleaf

tom@nw.stl.stc.co.uk (Tom Thomson) writes:

->This is pretty straightforward.
->If I have a set of numbers, I can talk about their sum and their product;
->these two things are described by a "reduction" function: one reduces 
->binary addition (or binary nultiplication) over the set with respect to
->an unit value of zero (or one).  It's not possible to talk about the
->difference or quotient of a set, because subtraction and division do not
->have the right properties.
->Think of it as starting from a function on lists:

->reduce :: ((alpha * beta) -> beta) * beta * list alpha -> beta;
->   reduce f u (cons a l) = reduce f (f a u) l;
->   reduce f u nil        = u;
->Then impose the requirement that it's meaningful for sets, rather than just
->for lists: ie you have to get the same result for the same set of list
->elements, regardless of the order they occur in.

->You can see how this requirement to be relevant to sets imposes restrictions
->on the function "f" in the above definition; and today's type systems do
->not allow me to specify these restrictions.

Presumably, the requirement on f is that (f,u,T) form an abelian group.
This certainly cannot be established either at compile or run-time. It
must be established during the specification and refinement phase, since
it will be undecidable for non-finite sets T, and essentially be
somewhat unwieldy for largish sets, say of size 10 and above. I think,
in part, you are pointing out a problem with the exclusive use of
executable notations.

The typing problem occuring here lies in the fact that "reduce" will
happily go about its business regardless of the nature of the "f" and
"u" passed to it. The user may never realise that the answers being
produced are complete garbage. This example shows that the original
problem put forward goes far beyond the idiosyncracies of lazy
evaluation.

In fact it helps make it clear that the original problem was
due to a failure of type security not to the method of evaluation used.
The function in question was being used incorrectly. It is the job of
the programmer to ensure that an overall product cannot be used
incorrectly (i.e. it must at least make it clear that it is producing
garbage), and hence that all internal functions are always used correctly.
The primary tool available for ensuring this is the programmers
intellect. Compile time and run-time checks can help in discovering some
incorrect uses of functions, but as we have seen the general problem is
theoretically beyond their capacity. The only way of having reasonable
confidence that all functions will always be used correctly is to
produce rigorous logical proofs that this is the case. Lambda calculus
is not an appropriate vehicle for producing such proofs, though its
cousin natural deduction is a good candidate for such a vehicle.

Far too little effort is being made by the fp community to deal with
this problem.
--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       
Department of Computer Science   | heretic: someone who disgrees with you
University of Queensland         | about something neither of you knows
Australia                        | anything about.