SHshakna·Dec 7, 2016
> This is a property of System F, the core itself, which is quite well established.
So when I repeatedly asked for the aspect of the language design that guaranteed this safety, and you responded with "the design guarantees it", you meant polymorphic lambda calculus, that, as it lacks infinite terms, preventing the creation of recursion through unfolding.
Clearly stating the reliance of System F would go some way towards generating trust in the definition of the language.
> There is no scientific debate to be had about this, anymore than there is a scientific "debate" about what temperature water boils at.
A language is considered to be Turing complete if it can calculate any computable value that a Turing machine can.
Brainfuck was proven to be Turing complete by Muller, and languages such as Piet have proven their own completeness by em
Read the rest
ulating or translating arbitrary Brainfuck programs.
So, I'm afraid the question in regards to the CPP, is only is limited recursion acceptable for Turing completeness?
The Turing-Church thesis specifically states that it should ignore resource limitations, which leads to the question of whether the limited recursion is a result of available resource or the language at hand.
There are active debates on this topic, and it cannot be so readily dismissed.
However, the point I raised with this, is the claimed safety of Dhall, in that it doesn't guarantee timely normalisation of its terms.
Which I believe you may have also noticed. [0]
> much like you're unlikely to write a Dhall configuration which takes 10 years to reduce when evaluated.
True, however the guarantee of evaluation safety is false.
There is no safety there when you can run out the available resource, such as time.
And people do insane, unlikely things with a language, such as breaching the type safety of Scala, and in response, they developed DOT calculus, so that they might give those guarantees.
Trusting a programmer not to do something stupid, is often the wrong thing to do. [1]
There is a line which must be drawn, but you can't make guarantees that mislead the programmer to feel safe.
[0] https://github.com/Gabriel439/Haskell-Dhall-Library/issues/6
[1] https://github.com/kanaka/mal/tree/master/awk