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

Alexis King lexi.lambda at gmail.com
Fri Aug 31 20:13:21 UTC 2018

Detecting termination of an arbitrary program written in a
Turing-complete language is (about as literally as can be) the halting


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).


> 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?

More information about the Haskell-Cafe mailing list