[Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
Erik de Castro Lopo
mle+hs at mega-nerd.com
Wed Dec 21 01:15:12 CET 2011
MigMit wrote:
> Dec 20, 2011, в 14:40, Jesse Schalken <jesseschalken at 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/
More information about the Haskell-Cafe
mailing list