[Haskell-cafe] Clearly, Haskell is ill-founded

[Conor McBride]

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.

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