[shakna]

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

[Gabriel439]

Author of Dhall here: while Dhall can't guarantee timely normalization Dhall can guarantee timely checking if a term is normalized and you can write a program using the Dhall library (or add a flag to the default Dhall compiler) that rejects imports that aren't in normal form. Checking for normal form is linear in the size of the source code.

As others have mentioned, Dhall is based on System F, which guarantees that all programs halt. You can't write the Y combinator or any other infinitely looping lambda calculus term in Dhall because it won't type check. The typical example of an infinitely looping lambda term is the following untyped lambda calculus term:

    (λx → x x) (λx → x x)

... which won't type-check in Dhall. It's actually not even legal Dhall code because you have to declare the type of all bound variables but there is no type you can assign to x that will make that type check. Even in a language with type inference it still won't type check as you will get a unification error

The theory behind Dhall's termination guarantees is sound. If a program loops indefinitely in Dhall it can only be because of an implementation bug causing Dhall not to match the underlying theoretical foundation. The theory itself is unbreakable.