[Haskell-cafe] if-then without -else?

[Rodrigo Stevaux]

Oh I see. Type checking a possibly infinite computation might itself take
possibly infinite steps?

Em sex, 31 de ago de 2018 às 17:13, Alexis King <lexi.lambda at gmail.com>
escreveu:

> Detecting termination of an arbitrary program written in a
> Turing-complete language is (about as literally as can be) the halting
> problem:
>
>     https://en.wikipedia.org/wiki/Halting_problem
>
> This problem has been known to be unsolvable in general (assuming we
> don’t discover some form of computation more powerful than a Turing
> machine; that is, the Church-Turing thesis holds) since 1936, and is one
> of the most fundamental results in computer science.
>
> It’s possible to determine if programs halt if you restrict the language
> sufficiently, but then it won’t be Turing-complete. However, this does
> not make totality checking completely fruitless, as it turns out you can
> do a great deal of useful things even in a language that is not
> Turing-complete (which I find is often surprising to people).
>
> Alexis
>
> > On Aug 31, 2018, at 15:02, Rodrigo Stevaux <roehst at gmail.com> wrote:
> >
> > which cannot be prohibited statically if we want both the language to
> > be Turing complete, and type inference to be decidable.
> >
> >
> > Could you be so kind as to give a hint on literature that could help
> > me understand this statement?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180831/795e55b5/attachment.html>