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