
Hi all On 9 Jul 2007, at 06:42, Thomas Conway wrote:
I don't know if you saw the following linked off /.
[..]
The basic claim appears to be that discrete mathematics is a bad foundation for computer science. I suspect the subscribers to this list would beg to disagree.
It's true that some systems are better characterised as corecursive "coprograms", rather than as recursive "programs". This is not a popular or well-understood distinction. In my career as an advocate for total programming (in some carefully delineated fragment of a language) I have many times been gotcha'ed thus: "but an operating system is a program which isn't supposed to terminate". No, an operating system is supposed to remain responsive. And that's what total coprograms do. By the looks of this article, the program versus coprogram distinction seems to have occasioned an unprecedented degree of existential angst for this individual. Even so, I'd say that it's worth raising awareness of it. Haskell's identification of inductive data with coinductive data, however well motivated, has allowed people to be lazy. People aren't so likely to be thinking "do I mean inductive or coinductive here?", "is this function productive?" etc. The usual style is to write as if everything is inductive, and if it still works on infinite data, to pat ourselves on the back for using Haskell rather than ML. I'm certainly guilty of that. I'd go as far as to suggest that "codata" be made a keyword, at present doubling for "data", but with the documentary purpose of indicating that a different mode of (co)programming is in order. It might also be the basis of better warnings, optimisations, etc. Moreover, it becomes a necessary distinction if we ever need to identify a total fragment of Haskell. Overkill, perhaps, but I often find it's something I want to express. Just a thought Conor