
On 22 Dec 2011, at 17:49, Bardur Arantsson wrote:
Alexander Solla wrote:
I happen to only write Haskell programs that terminate. It is not that hard. We must merely restrict ourselves to the total fragment of the language, and there are straight-forward methods to do so.
Do (web/XML-RPC/whatever) server type programs terminate?
No, but "total" and "terminating" are not the same. Those *co*programs will, if they're any good, be total by virtue of their productivity rather than their termination. What's slightly controversial is the claim that we "must merely restrict ourselves to the total fragment of the language". It would be more controversial to claim that some new Haskell-like language should restrict us to total programs. I'd be glad if "pure" meant "total", but partiality were an effect supported by the run-time system. Then we could choose to restrict ourselves, but we wouldn't be restricted by the language. This is not the first time the issue has surfaced, nor will it be the last. It's customary at this point to object that one wouldn't want to program with the monadic notation, just for the effect of partiality. I'd counter that I don't want to program with the monadic notation, for any effects: I'd like to program with an applicative notion, but in monadic types. That's what I'd do different, and for me, the subject is not a hypothetical question. All the best Conor