It seems to me the equivalence comparison will always have its limits. The Dhall documentation gives the example of `even(n + n)`, which Dhall is unable to recognize as equivalent to `true`. The feature is of course still useful, but I‘m doubtful the non-Turing completeness is absolutely essential to it, given its limitations.
back
1 comments
In a total language, you can prove that `even(n+n) = true`. Dhall probably doesn’t bother with this because it’s focused on proving that your resulting data structures are equivalent: so, since functions are guaranteed to run in a bounded amount of time, it just runs all the functions it finds and then normalizes the resulting data structure. Equality between these data structures implies program equivalence.