Hacker News Reader

Comment by cryptonector | Hacker News Reader

If you have functions that can call functions, you'd better not have recursion if you want to not be Turing-complete.

Non-Turing-completeness is certainly very important in many cases (e.g., in DTrace and eBPF), but I'm not sure that it's so important for configuration. Assuming for a moment that I don't need non-Turing-completeness for configuration, my choice of DSL would be jq[0]! Using jq for configuration means that I can use JSON, TOML-style, and other ways of expressing complex data, including combinations of them, all with "interpolation" (not quite) and complex computation being available.

  [0] https://stedolan.github.io/jq/

View on HN

One valuable point of Dhall is that it is programmable (yet not TC) in such a way to that you can e.g. describe a whole system entirely in Dhall and then (in Dhall!) derive whatever further configurations (plural!) you need from that. This is much more feasible than in e.g. YAML because Dhall is strongly typed.

So you could describe e.g. a cluster of machines entirely in Dhall and derive Ansible YAML scripts (with all their boilerplate), derive DNS config files, etc. etc. all from a single strongly typed description.

It goes even further: because Dhall supports functions one can write a function that will migrate old configs to new format. Migration function can also be type checked (it must accept old config format and emit new one). Of course all of this without TC.

I mean, jq is a powerful programming language. Did you look at the link I posted?

Well, you did format it so that it's not clickable...

Sure, I'm familiar with it. It's nothing compared to what Dhall can do.

... unless of course it's grown to a similar point. As of about a year ago, for some complex transformations I had to stitch together multiple invocations of jq using pipes, etc. etc. That may have been my inexperience with using it, though.

Regardless, the point about typing stands. Dhall uses structural typing/subtyping which turns out to be hugely useful for config transformation.

I never have to "stitch together multiple invocations of jq using pipes". There was a time when I did have to, but that was years ago, and it now has the features needed to avoid that. Not sure what the point about typing was -- you can do the same derivation of data from a master entity with or without strong typing (though my preference is always for strong typing, which jq lacks).

> you can do the same derivation of data from a master entity with or without strong typing (though my preference is always for strong typing, which jq lacks).

Yes, of course you can. The point is that the strong typing helps prevent inadvertent and hard-to-spot mistakes. In jq even simple typos of a field name can lead to "empty result set" silent failures instead of "what do you mean!" loud failures. That's a big thing.

Strong typing generally doesn't speak to "how many values this expression should produce", only their types. Not saying it couldn't, but that even in Haskell you don't quite get that.

I was talking about a mismatched field name. What case are you talking about?

EDIT: Actually, responding to

> Strong typing generally doesn't speak to "how many values this expression should produce"

Have you heard of affine/linear types?

Recursion is fine, as long as an argument gets smaller at every iteration, since that guarantees termination.

Oh, like Ackermann function[0]? Because I wouldn't want my server try to evaluate that.

[0] https://en.wikipedia.org/wiki/Ackermann_function

Exactly.

And heck, even with loops that are guaranteed to terminate, you can loop long enough to have that be a problem.

You really want to have no loops at all, like DTrace and eBPF, or else you want to give up on this idea of not being Turing-complete. You have to decide how critical it is to be able to put a reasonable bound on the run-time of a function.

Since there are no side effects in Dhall you can always just impose an arbitrary timeout if you really want to.

IME, it's really rare to stumble upon pathological complexity like the Ackermann function. You basically have to go out of your way to do 'absurd' things.

(The point is of course taken, but personally I don't really care much about the TC-ness or otherwise of Dhall, though it is kind a nice-to-have to ensure that you don't accidentally introduce infinite loops.)

Reply on news.ycombinator.com