
20 Dec
2011
20 Dec
'11
7:15 p.m.
MigMit wrote:
Dec 20, 2011, в 14:40, Jesse Schalken
написал(а): If you think a value might not reduce, return an error in an error monad. Then the caller is forced to handle the case of an error, or propagate the error upwards. The error can also be handled in pure code this way, whereas bottom can only be handled within the IO monad.
So... this imaginary language of yours would be able to solve the halting problem?
Depends on what you mean "solve" the halting problem. Agda and Coq are two languages that will only compile programs that can be proven to terminate. Non terminating programs are rejected. Erik -- ---------------------------------------------------------------------- Erik de Castro Lopo http://www.mega-nerd.com/