Conor McBride wrote:
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.
I like that distinction.. how is "shutting down" or "executing (switching to) another arbitrary OS's kernel" modeled (in response to input, in a total way, of course)?
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.
I find that one of Haskell's faults is it's too hard to avoid the "everything is lazy " even when I want to - partly because I don't understand inductive vs. coinductive very well (particularly, not in practice). If "data List a = Nil | Cons a (List a)" is finite and "codata Stream a = Cons a (Stream a)" is infinite, what is "codata CoList a = Nil | Cons a (CoList a)"? I need a tutorial on "more-total" programming in Haskell =) (leading to a keener awareness of just where the untamed laziness of Haskell can occasionally make code much more concise and understandable, and where the laziness actually has a formal structure that one can stay within) Non-inductive, finite structures - cyclic directed graphs, usually - are quite annoying to implement and use in Haskell. (Especially if you want garbage collection and sharing to work well with them... or if different nodes should be different types, only allowed in particular arrangements - I'm pretty sure that dependent types would alleviate that last one, not sure about the other irritations ) Isaac