4 ms·

My comment isn't specifically about Dhall, but about the note on Turing completeness. I often read comments about how YAML/JSON is not turning complete. These c

My comment isn't specifically about Dhall, but about the note on Turing completeness. I often read comments about how YAML/JSON is not turning complete. These comments normally frame the lack of Turing completeness as being a short coming of the format(s). I find this interesting because one the reasons that the industry moved away from XML was to have cleaner separation between data and logic. I generally tend to think that it is cleaner to separate logic and data, instead of creating a tight coupling. I don't read many people making comments from this perspective though. I am not trying to say we can't do better then YAML/JSON, I am just trying to offer some food for thought. I tend to view JSON/YAML as a data exchange format, and not a programming language, so I am not bothered by the lack of Turing completeness.

nine_k 7y ago
Not being Turing-complete is a feature. A Turing-complete language allows to write programs that never terminate. This is not what a config file should be capable of.
- dharmab 7y ago
  Previously in my career I've abused Jinja templating to build "scripts" out of Ansible and SaltStack YAML. It solved business problems effectively but I'm sure when I left that role I passed on a big plate of spaghetti to my successor with minimal automated tests. If it depends on conditional logic or iteration, it probably belongs in a proper programming language with a linter, type checkers, debugger and unit test framework.
  - eropple 7y ago
    This is one of the reasons why, coming from a background of writing Chef and writing exhaustive testing around my configuration management, I've never been able to deal with Ansible without grinding my teeth. Or, for that matter, Terraform; HCL is godawful and trying to write it in JSON is a sucker's bet, too. With the move towards more containerized systems I don't write Chef much anymore (thankfully), but Terraform has become ever more of a boil on my rear end. Fortunately there's also Pulumi now and writing this stuff in TypeScript is a lot faster and feels really good.
    - markandrewj 7y ago
      The thing is, although Ansible is not perfect, it is python. When you are writing playbooks you should be defining the state of the world, if you are writing custom logic it is probably best to write a custom module, which are commonly unit tested. I haven't tried Pulumi yet, thanks for pointing it out.
      - _frkl 7y ago
        I'm not quite ready yet (esp. documentation is lacking), but I'm working on something to get the best of both worlds: https://freckles.io https://freckles.io Basically, you write your state-defining code in Ansible, using either modules, tasklists, roles, or a combination thereof. 'freckles' lets you wrap those up in re-usable, distinct, atomic units which you can combine for more complex tasks. Then you can use those directly via the command-line, or you can auto-generate (wrapper) Python (will do other languages later) classes from them (e.g. https://freckles.io/doc/interfaces/python#code https://freckles.io/doc/interfaces/python#code ), for when there is more 'logic' to be implemented. I reckon it's a bit like Pulumi, but it is less opinionated. Actually, it's probably more like it lets you create your own little domain-specific Pulumi, if that makes any sense. It also works really well as a wrapper for Packer and Terraform. As I said, documentation is not quite there yet, but most of the important stuff works. Starting to look for people to try it out, if anybody on here is interested.
        eropple 7y ago
        First off: congratulations on shipping something! Shipping is hard. But this misses the mark. With respect, and I'm trying to not not dunking on your project, to me Ansible is the worst of every world and is emblematic of configuration management retreating from the realm of "infrastructure as code" to "infrastructure as magic notepad files because incurious sysadmins won't write code.". I don't really care that Ansible is being wrapped so long as, inevitably, I'm going to have to go deal with that when it breaks. Eventually Pulumi/Terraform will break too, and there is no programming language I have more eyerolls for than Golang, but at least it's a programming language, you know? (And I really don't relish the thought of ping-ponging from the Python wrapper to YAML hell to a Python module, tbh.) The biggest thing that a project like Freckles fails to capture, and where Pulumi shines, is that it's all code and you just treat it as code. They're compiler wonks, or at least the guy I know there is one, and they leverage that--when dealing with stuff like Lambdas/GCP Cloud Functions, you just write them inline and they're hoisted into deployable packages without comment or incident. There's no zipping of files, there's no messing around--you wrote a function to do a thing and it gets run. Done-and-done. It's got a lot of other nice features, but that it is transparently code, and that they're investing most of their effort (it seems) into hiding the unfortunate fact that eventually some Terraform providers get run, makes Pulumi a really hard one to top.
- comex 7y ago
  Of all the bugs you've ever dealt with in programs in general, what fraction of them of them were infinite loops? For me I'd guess maybe... 0.1%? It's definitely under 1%. Given that, it makes no sense to me that I'd want to make myself jump through hoops to express some basic coding patterns [1], just to rule out that single class of bugs. It seems like a solution in search of a problem. [1] https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall https://github.com/dhall-lang/dhall-lang/wiki/How-to-transla...
  - jose_zap 7y ago
    I think the Non-Turing completeness is misunderstood as "no infinite loops!". Of course, that's the obvious effect of not having it, but it has more important effects: 1. Any expression can be normalised at compile time. This means that you can remove all abstractions in your code and audit the result before running it. This is great of debugging and understanding a codebase you may not be familiar with. 2. You can be sure that the language cannot do a jailbreak and potentially read files or make network calls it was not supposed to. Not because the Dhall developers are security geniuses but because it is literally impossible without Turing completeness. An example of a NT complete language that you would hate if it could read a file in your system and send it to attackers is Regular Expressions, for example. 3. It helps the language stay focused. This limitation is the biggest motivator to keep the language being focused on a single domain, and not try to be everything. This also helps execution performance of the language.
    - jholman 7y ago
      I feel like you've made in "inverse error" here repeatedly. If a language L1 is Turing complete then you have some potential liabilities: there's no general normalization plan, you cannot in general ensure security guarantees, etc. But another language, L2, might be not-Turing-complete and still have all the same problems. It may especially be the case that L2 has no known normalization algorithm, or no known general security audit. For example, many interesting properties are undecidable for the general case of context-free languages (a class that I'm sure you know is much more restricted than the class for Turing-complete languages). For example universality is undecidable in this class, as is language equivalence. As for being sure that the language cannot do a jailbreak, you can't be sure until you write a proof. It's nice that Godel isn't telling you that no such proof can possibly be written, but that's still a long way from having a proof. I agree with you that this sort of thinking seems to be why people say that they do not want certain languages to be Turing-complete, but I'm not at all convinced that those people have correctly named the property that they want.
tannhaeuser 7y ago
> one [of] the reasons that the industry moved away from XML was to have cleaner separation between data and logic How is XML coupling data and logic? The only kind of "processing" it does by itself I can think of is composing documents from pieces and "processing instructions" as a generic extension mechanism. That is, features to support its original use case of authoring and capturing structured text. Now SGML has more processing features (tag inference, stylesheets/link processes, notations), but is still far away from Turing-completeness.
- markandrewj 7y ago
  I am not sure if this completely answers your question, but I am talking about XML in a SOAP based architecture.
javier2 7y ago
I 100% agree. It should be considered an important feature that my configuration files (and transfer data) don't suffer from the halting problem.
dragonwriter 7y ago
> I find this interesting because one the reasons that the industry moved away from XML was to have cleaner separation between data and logic. That's not really true or even sensible, since XML doesn't combine data and logic. Sure, there were XML-based logic languages (most notably XSLT) as well as XML-based data languages, but while all were applications of XML they were separate languages. XML lost ground to JSON, etc., as the fashion pendulum swung away from heavyweight tooling and detailed specs for most things (though it's swinging back again), and to some closer-to-memory-layout binary formats as efficiency became a concern in some of the places where rigid specs remained important.
- markandrewj 7y ago
  Hello, just to clarify I am specifically talking about how XML was used in the 90's for web development, i.e. SOAP.

nine_k 7y ago

Not being Turing-complete is a feature. A Turing-complete language allows to write programs that never terminate. This is not what a config file should be capable of.

dharmab 7y ago
Previously in my career I've abused Jinja templating to build "scripts" out of Ansible and SaltStack YAML. It solved business problems effectively but I'm sure when I left that role I passed on a big plate of spaghetti to my successor with minimal automated tests. If it depends on conditional logic or iteration, it probably belongs in a proper programming language with a linter, type checkers, debugger and unit test framework.
- eropple 7y ago
  This is one of the reasons why, coming from a background of writing Chef and writing exhaustive testing around my configuration management, I've never been able to deal with Ansible without grinding my teeth. Or, for that matter, Terraform; HCL is godawful and trying to write it in JSON is a sucker's bet, too. With the move towards more containerized systems I don't write Chef much anymore (thankfully), but Terraform has become ever more of a boil on my rear end. Fortunately there's also Pulumi now and writing this stuff in TypeScript is a lot faster and feels really good.
  - markandrewj 7y ago
    The thing is, although Ansible is not perfect, it is python. When you are writing playbooks you should be defining the state of the world, if you are writing custom logic it is probably best to write a custom module, which are commonly unit tested. I haven't tried Pulumi yet, thanks for pointing it out.
    - _frkl 7y ago
      I'm not quite ready yet (esp. documentation is lacking), but I'm working on something to get the best of both worlds: https://freckles.io https://freckles.io Basically, you write your state-defining code in Ansible, using either modules, tasklists, roles, or a combination thereof. 'freckles' lets you wrap those up in re-usable, distinct, atomic units which you can combine for more complex tasks. Then you can use those directly via the command-line, or you can auto-generate (wrapper) Python (will do other languages later) classes from them (e.g. https://freckles.io/doc/interfaces/python#code https://freckles.io/doc/interfaces/python#code ), for when there is more 'logic' to be implemented. I reckon it's a bit like Pulumi, but it is less opinionated. Actually, it's probably more like it lets you create your own little domain-specific Pulumi, if that makes any sense. It also works really well as a wrapper for Packer and Terraform. As I said, documentation is not quite there yet, but most of the important stuff works. Starting to look for people to try it out, if anybody on here is interested.
      - eropple 7y ago
        First off: congratulations on shipping something! Shipping is hard. But this misses the mark. With respect, and I'm trying to not not dunking on your project, to me Ansible is the worst of every world and is emblematic of configuration management retreating from the realm of "infrastructure as code" to "infrastructure as magic notepad files because incurious sysadmins won't write code.". I don't really care that Ansible is being wrapped so long as, inevitably, I'm going to have to go deal with that when it breaks. Eventually Pulumi/Terraform will break too, and there is no programming language I have more eyerolls for than Golang, but at least it's a programming language, you know? (And I really don't relish the thought of ping-ponging from the Python wrapper to YAML hell to a Python module, tbh.) The biggest thing that a project like Freckles fails to capture, and where Pulumi shines, is that it's all code and you just treat it as code. They're compiler wonks, or at least the guy I know there is one, and they leverage that--when dealing with stuff like Lambdas/GCP Cloud Functions, you just write them inline and they're hoisted into deployable packages without comment or incident. There's no zipping of files, there's no messing around--you wrote a function to do a thing and it gets run. Done-and-done. It's got a lot of other nice features, but that it is transparently code, and that they're investing most of their effort (it seems) into hiding the unfortunate fact that eventually some Terraform providers get run, makes Pulumi a really hard one to top.
comex 7y ago
Of all the bugs you've ever dealt with in programs in general, what fraction of them of them were infinite loops? For me I'd guess maybe... 0.1%? It's definitely under 1%. Given that, it makes no sense to me that I'd want to make myself jump through hoops to express some basic coding patterns [1], just to rule out that single class of bugs. It seems like a solution in search of a problem. [1] https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall https://github.com/dhall-lang/dhall-lang/wiki/How-to-transla...
- jose_zap 7y ago
  I think the Non-Turing completeness is misunderstood as "no infinite loops!". Of course, that's the obvious effect of not having it, but it has more important effects: 1. Any expression can be normalised at compile time. This means that you can remove all abstractions in your code and audit the result before running it. This is great of debugging and understanding a codebase you may not be familiar with. 2. You can be sure that the language cannot do a jailbreak and potentially read files or make network calls it was not supposed to. Not because the Dhall developers are security geniuses but because it is literally impossible without Turing completeness. An example of a NT complete language that you would hate if it could read a file in your system and send it to attackers is Regular Expressions, for example. 3. It helps the language stay focused. This limitation is the biggest motivator to keep the language being focused on a single domain, and not try to be everything. This also helps execution performance of the language.
  - jholman 7y ago
    I feel like you've made in "inverse error" here repeatedly. If a language L1 is Turing complete then you have some potential liabilities: there's no general normalization plan, you cannot in general ensure security guarantees, etc. But another language, L2, might be not-Turing-complete and still have all the same problems. It may especially be the case that L2 has no known normalization algorithm, or no known general security audit. For example, many interesting properties are undecidable for the general case of context-free languages (a class that I'm sure you know is much more restricted than the class for Turing-complete languages). For example universality is undecidable in this class, as is language equivalence. As for being sure that the language cannot do a jailbreak, you can't be sure until you write a proof. It's nice that Godel isn't telling you that no such proof can possibly be written, but that's still a long way from having a proof. I agree with you that this sort of thinking seems to be why people say that they do not want certain languages to be Turing-complete, but I'm not at all convinced that those people have correctly named the property that they want.

tannhaeuser 7y ago

> one [of] the reasons that the industry moved away from XML was to have cleaner separation between data and logic How is XML coupling data and logic? The only kind of "processing" it does by itself I can think of is composing documents from pieces and "processing instructions" as a generic extension mechanism. That is, features to support its original use case of authoring and capturing structured text. Now SGML has more processing features (tag inference, stylesheets/link processes, notations), but is still far away from Turing-completeness.

markandrewj 7y ago
I am not sure if this completely answers your question, but I am talking about XML in a SOAP based architecture.

javier2 7y ago

I 100% agree. It should be considered an important feature that my configuration files (and transfer data) don't suffer from the halting problem.

dragonwriter 7y ago

> I find this interesting because one the reasons that the industry moved away from XML was to have cleaner separation between data and logic. That's not really true or even sensible, since XML doesn't combine data and logic. Sure, there were XML-based logic languages (most notably XSLT) as well as XML-based data languages, but while all were applications of XML they were separate languages. XML lost ground to JSON, etc., as the fashion pendulum swung away from heavyweight tooling and detailed specs for most things (though it's swinging back again), and to some closer-to-memory-layout binary formats as efficiency became a concern in some of the places where rigid specs remained important.

markandrewj 7y ago
Hello, just to clarify I am specifically talking about how XML was used in the 90's for web development, i.e. SOAP.