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 /.
http://www.itwire.com.au/content/view/13339/53/
[..]
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
