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". > Dec 20, 2011, в 14:40, Jesse Schalken <jesseschal...@gmail.com> написал(а): >> 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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
