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