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

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