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

[Isaac Dupree]

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