On 20/12/2011, at 21:52 , Gregory Crosswhite wrote:

Some would say that non-termination is a computational effect, and I can argue either way depending on the day of the week.

*shrug* I figure that whether you call _|_ a value is like whether you accept the Axiom of Choice: it is a situational decision that depends on what you are trying to learn more about.

I agree, but I'd like to have more control over my situation. Right now we have boxed and lifted Int, and unboxed and unlifted Int#, but not the boxed and unlifted version, which IMO is usually what you want.

Of course, the history books show that monads were invented *after* it was decided that Haskell would be a lazy language. Talk about selection bias.

True, but I am not quite sure how that is relevant to _|_...

I meant to address the implicit question "why doesn't Haskell use monads to describe non-termination already". The answer isn't necessarily "because it's not a good idea", it's because "that wasn't an option at the time".

Including all possible manifestations of infinite loops?

So... this imaginary language of yours would be able to solve the halting problem?

All type systems are incomplete. The idea is to do a termination analysis, and if the program can not be proved to terminate, then it is marked as "possibly non-terminating". This isn't the same as deciding something is "*definitely* non-terminating", which is what the halting problem is about. This "possibly non-terminating" approach is already used by Coq, Agda and other languages.

Ben.