New topic, new thread :-)
Paul Rubin schrieb:
> Joachim Durchholz <jo@[EMAIL PROTECTED]
> writes:
>> What's a coalgebraic datatype?
>> In simple terms that a humble trench programmer can understand, please
;-)
>
> If you haven't read Turner's paper on total functional programming,
> you should. It is great.
>
> http://www.jucs.org/jucs_10_7/total_functional_programming
OK, I just read the paper and am now ready to discuss it.
I have several issues with it.
Issue 1.
I'm not sure I even follow his premise. The starting point of his
argumentation is that nontermination makes equational reasoning invalid.
To sup****t that stance, he gives us this little function definition:
> loop n = 1 + loop n
and goes on to instantiate it with n = 0, giving
> loop 0 = 1 + loop 0
subtracts loop 0 from both sides and gets
> 0 = 1
which is obviously not what equational reasoning should give us as a
result.
He attributes the problem to the fact that loop n diverges for any n,
i.e. it has a "result" of bottom, and uses that to argue that we should
avoid nontermination.
I think different. He simply forgot to check whether subtracting loop 0
on both sides was a valid, equality-preserving operation - just as
diving both sides of an equation is valid iff the divisor is nonzero. I
think finding out whether a formula terminates is just as easy or
complicated as finding out whether its result is zero, so this
nontermination "s****" isn't anything new in the garden of mathematics;
there are simply some formulae that are syntactically valid but
semantically void, such as the definition of loop above.
(Mathematically, loop n = 1 + loop n is an overspecified linear
equation, and such equations are well known to not have a solution
unless you're lucky.)
Issue 2.
To make all operations total, he proposes to establish
> 0 / 0 = 0
Mathematically, this is just ****fting problems: all division operations
now have a result, but you lose the property that a / b * b = a (for b
!= 0). In other words, he *still* has to check that the divisor isn't
zero to avoid funny effects during equational reasoning, though the
exact nature of the funny effects is now different.
Face it: there's no way of making division both total and an inverse of
multiplication; multiplication *must* make a*0=0 for any a, so there is
no way to fill in an X for X*0 = 1 (which is just an other way of
writing 1/0 = X).
So even natural-number arithmetic isn't total, and making it total means
giving up at least one of commutativity, associativity, the role of
zero, or the role of the inverse for multiplication - seems like
throwing out one s**** just to invite back all its distant relatives.
Issue 3.
It seems that his codata is just what I meant with "separate types for
potentially nonterminating expressions" (unbounded data in the
terminology I have been using).
I may be wrong with that. I may have overlooked what's so fine about
naming unbounded data as codata. Or maybe the really interesting part
about his paper is that he draws a relatively straightforward type-based
(actually even syntax-based) boundary between bounded and unbounded
data. I'm not far enough into the relevant theories to really know the
ramifications.
Personal Conclusion
On the other hand, there's a very simple way to deal with the issue.
First, given the observation that equational reasoning isn't always
simple, deal with nontermination as a bug. Infinite data structures can
always be represented using higher-order data. I suspect that Turner's
approach of distingui****ng between data (finite) and codata (unbounded)
is effectively the same as OCaml's approach of distingui****ng between
lists (finite) and generators (unbounded).
We lose laziness that way, but I think of it as a very mixed blessing
anyway.
Why deal with it as a bug? Because the language needs to deal with bugs
anyway. Regardless of how little error-prone a programming paradigm is,
programs will grow to exactly the complexity that's barely manageable -
and it becomes unmanageable exactly at the point where the bug density
becomes intolerable.
So use strict evaluation, throw an exception if a subroutine fails to
return within the allowed time (for every piece of code, there *is* a
maximum time it's allowed to run, if only the user who's not willing to
wait anymore), and use metalinguistic facilities (assertions with
primitives that go slightly beyond what's in the language) to establish
complexity limits.
The section "Personal Conclusion" is, of course, just the conclusions
that I personally draw from my observations.
The observations may be off the mark, and other people may draw other
conclusions - I'd be interested to read them!
Regards,
Jo
|
