3 ms·

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

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/

Quekid5 7y ago
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.
- Boulth 7y ago
  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.
- cryptonector 7y ago
  I mean, jq is a powerful programming language. Did you look at the link I posted?
  - jessaustin 7y ago
    Well, you did format it so that it's not clickable...
  - Quekid5 7y ago
    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.
    - cryptonector 7y ago
      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).
      - Quekid5 7y ago
        > 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.
        cryptonector 7y ago
        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.
        Quekid5 7y ago
        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?
codebje 7y ago
Recursion is fine, as long as an argument gets smaller at every iteration, since that guarantees termination.
- ignaloidas 7y ago
  Oh, like Ackermann function[0]? Because I wouldn't want my server try to evaluate that. [0] https://en.wikipedia.org/wiki/Ackermann_function https://en.wikipedia.org/wiki/Ackermann_function
  - cryptonector 7y ago
    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.
  - Quekid5 7y ago
    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.)

Quekid5 7y ago

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.

Boulth 7y ago
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.
cryptonector 7y ago
I mean, jq is a powerful programming language. Did you look at the link I posted?
- jessaustin 7y ago
  Well, you did format it so that it's not clickable...
- Quekid5 7y ago
  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.
  - cryptonector 7y ago
    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).
    - Quekid5 7y ago
      > 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.
      - cryptonector 7y ago
        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.
        Quekid5 7y ago
        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?

codebje 7y ago

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

ignaloidas 7y ago
Oh, like Ackermann function[0]? Because I wouldn't want my server try to evaluate that. [0] https://en.wikipedia.org/wiki/Ackermann_function https://en.wikipedia.org/wiki/Ackermann_function
- cryptonector 7y ago
  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.
- Quekid5 7y ago
  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.)