Item — HN Reader

As soon as you add some kind of macro system or any other content-rewriting, template-with-parameters or functional-abstraction mechanism, you may as well go full Turing. Otherwise people will try to simulate it using the available mechanisms, as they have for example with the C preprocessor, resulting in higher complexity than if you’d just given them Turing completeness in the first place.

So the only real choices seem to be either a pure data format or else full Turing completeness. There doesn’t seem to be a useful middle ground, unfortunately.

2 comments

I think Dhall is an interesting point in this design space: powerful enough to write real functions, not Turing complete so all Dhall programs can be reduced to a normal form and compared for equivalence.

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.

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.

sendmail.cf was a warning, not an example!