Dhall: a programmable configuration language that is not Turing-complete

Talking about statically-typed languages and configuration paramètres, something coming from the Ada/SparkAda world is the use of type predicates and invariants, in addition to expressive static typing.

Here's an interesting paper on the subject : http://acg-solutions.fr/acg/wp-content/uploads/2017/04/PDI-5...

And here's some demo code : https://github.com/AdaCore/SPARK_PDI_Demo/blob/master/README...

The other interesting part is that you can then prove (or use static analysis to get à high level of confidence) your application will never be run with incoherent parameters. Another nice thing is that with the help of the prover you can let the internal constraints of your implementation surface up to the application parameters. Sa y you didn't handle some corner case, you can either implement it, or use a predicate to ensure this case is never run. Your pre-conditions and the type invariants/predicates of your parameters are part of your interface.

It's only guaranteed to terminate. That doesn't mean it's guaranteed to terminate before the heat death of the universe.

Wait, so you can write programs in this thing that aren't primitive recursive? That's quite interesting; requiring primitive recursiveness is the usual way to guarantee termination. What class of programs does this language allow you to write? (It of course can't allow all programs that terminate, unless it also allows some that don't, which it claims not to.)

For what is worth, Dhall lets you check if an expression is already in normal form: http://hackage.haskell.org/package/dhall-1.6.0/docs/Dhall-Co... so one could use Dhall as a "data-only" language without bothering with evaluation.

Yes? Do you foresee this being a typical thing to write in configuration files?

If we're being pedantic, as you were in your comment, "close to Turing complete" is not really a very precise term, is it?

When you have an issue, at least be explicit about it rather than just snarky. (See also Gabriel's other comments in this thread; not that I know or have any affiliation with him.)

Perhaps I should've added a :P to the end of that. See Gabriel's response here: https://news.ycombinator.com/item?id=15187733

More commonly called a DSL. See: Varnish's configuration language, which is also not Turing-complete: https://varnish-cache.org/docs/3.0/tutorial/vcl.html

I agree with you there, but those of you already reading this, here's what it means (what I think it means anyway ;-):

Dhall is like a templating language, but statically typed and will always terminate. Typing is good because your configuration will always have correct structure -- the language itself allows you to verify this; and non-determination is good because you don't have to worry about your program accidentally not terminating.

JSON, YAML, .ini, etc etc are non-programmable configuration languages, and, I guess, m4 would be an example of a Touring complete one.

I use Dhall extensively now. In fact, all my typescript programs for my current employer use JSON configuration that Dhall generates (and I've tried so many times to get this to frontpage on YC, I guess I'm just not good at timing).

Dhall's draw as a configuration language is that it allows you to express logic in your configuration and even call out to remote services and file handles safely. People have a gut negative reaction to this phrase even as they essentially encode non-trivial logic directly into their Chef, CircleCI, Docker-Compose and Kubernetes configs, so it's hardly a new idea.

Dhall lets you write logic into your configs that otherwise would be implicit. As an example, you might define a new configuration environment with Dhall and use the types to make sure you NEVER provide production credentials, or even shared credentials.

Dhall also allows you to safely call out to web services (with authentication and SSL, of course) to fill in holes or even provide non-trivial logic (it's perfectly valid to move functions around in dhall over the wire). I use this feature to map a tiny microservice that resolves Hashicorp Vault calls to AWS credentials just-in-time as I ship, and I feel very confident that it's safe because I can encode the sorts of permissions and their resolution directly into the types I'm handling.

You could start using Dhall instead of JSON today for configs, and the main advantage is that you can assert values have specific types (and also provide sane loops over list fields).

Dhall is actually a pretty amazing invention and I keep trying to work up the guts and time to write a typescript interpreter for it.

For starters, consider any kind of configuration that might get really repetitive. Say you're running a web server that's serving several subdomains, but almost all of them are serving static files from a pretty standard directory hierarchy. You could write out each server configuration individually, like

  { "servers":
    [ { "domain": "foo.example.com", "root": "/srv/example/foo", "port": 80, "gzip": true, ...},
      { "domain": "bar.example.com", "root": "/srv/example/bar", "port": 80, "gzip": true, ...},
      { "domain": "baz.mydomain.com", "root": "/srv/mydomain/baz", "port": 80, "gzip": true, ...},
    ]
  }

but in a proper programming language, that'd be kind of a code smell: it's repetitive, a bunch of fields are shared between each entry, &c &c. Well, a configuration language that adds functions would let you abstract over that repetition. (This isn't Dhall syntax, because I don't know Dhall, but rather a kind of strawman syntax.)

  let typical_server(domain, subdomain) =
    { "domain": concat(subdomain, ".", domain, ".com"),
      "root": concat("/srv/", domain, "/", subdomain),
      "port" 80,
      "gzip": true,
      ...
    }
  in { "servers": [ typical_server("example", "foo"),
                    typical_server("example", "bar"),
                    typical_server("mydomain", "baz"),
                    ...
                  ] }

More than that, though, it would also let you include values in your configuration fields that are themselves functions. For example, say I'm writing an email client, and I want users to be able to define labels that allow automatic sorting of emails based on various criteria: does it contain this substring, is it from this address, does it have an attachment, &c.

  { "labels": [ { "name": "from_joe",
                  "criteria": { "email_address": "joe@example.com" }
              ] }

But this only works with simple tests. Let's say a user wants to apply a label if an email is from this address or from that address or contains certain text in the body as well as a particular attachment: I would have to add all kinds of complicated edge cases to this JSON configuration, or just throw my hands up and say that the user can't do that.

But with JSON + arbitrary terminating functions, I can have my cake and eat it too, because now I can include functions as values in my configuration. A user could write something like (although again, pseudocode and not Dhall):

  { "labels": [ { "name": "from_joe",
                  "criteria": fun(email) => email.addr == "joe@example.com"
                                || email.addr == "joseph@example.com"
                                || (email.body.contains("joseph") && is_key(email.attachments[0]) }
               ] }

That doesn't mean you'd necessarily want this for every kind of configuration, of course! But features like this—the ability to use program-like abstraction in your configuration files as well as the ability to express arbitrary terminating functions are both interesting features that make a language like this worth considering.

Author here: there is a reason why "programmable configuration language" is a fairly new term. Most of the time, when people want a programmable configuration they use whatever language they are already programming in. So, for example, if you are writing a program in Scala you might write the program's configuration in Scala, too. For example, this is how Scala's SBT works: the SBT configuration is written in Scala

However, there are some down-sides with writing your configuration within a language like Scala (or any other mainstream language). For example, your program "configuration" can hang, crash, throw exceptions, or destroy your system if it is running with sufficiently elevated privileges. Dhall has none of those problems.

Similarly, you can go overboard and use excessive abstraction in other languages, which is inappropriate for a configuration file (which needs to be easy to read and understand). Dhall also avoids this issue by supporting automatic simplification of configuration files to remove abstraction, imports, and indirection (which is made possible by the fact that Dhall is not Turing complete)

I'll try to rework the documentation to answer this sort of question better and also incorporate some of the other excellent replies to your question

It's less about "programmable", it's more about "Turing-complete". Why this is important - see my other comment here for details: https://news.ycombinator.com/item?id=15190110. TL;DR: langsec.

For configuration you very much do not want Turing-complete language -- or any programming language, for that matter. Configuration quite often is processed by more than just the original program it was intended for, so plain data dump is the easiest form from this angle. Also, it's much easier for human operator to just read the values than to interpret a de facto script that produces values.

There were several attempts at using a programming language the tool was written in for storing its configuration. None worked well enough to catch up as a general trend, and not because the languages used were Turing-complete.

My opinion is that a programmer has seen for a short moment what sysadmins do and decided to make something to help in the task, without really understanding what's needed and what works, what doesn't work, and why.

If your language is not Turing Complete, then it might be possible to always prove certain properties of programs. Canonically, you might be able to prove that the program will always complete and exit in finite time on any input. Other properties include guaranteeing that an error will not be thrown (or will be thrown), or bounding the amount of time or memory consumed, or guaranteeing that the output of a function will be within a certain numeric range.

For instance, if you want to make guarantees about program termination (as the author does here). This is not possible for Turing complete languages.

You would always prefer to not have Turing completeness in your language, all other things being equal. Turing completeness isn't ever necessary to write the logic you want to write.

But all other things are not equal. There is a cost to giving up Turing completeness. The language must now ensure additional properties about the code, mostly related to termination and productivity. The two strategies for this are reducing functionality offered by the language until you can prove all programs are good and introducing tools into the language to write compiler-verified proofs about your code.

Dhall is an example of the former approach. It removes enough pieces that it can only express computations that terminate.

Language like Idris, Agda, and Coq are examples of the latter. They provide rich systems that allow you to express proofs of various properties as needed to avoid Turing completeness.

Both categories of language are currently difficult to use for general purposes software. Turing completeness is a sacrifice made to ease writing software at the cost of making certain bugs possible.

At the moment, the best times to use a non-Turing complete language are when you have a problem domain where you can be satisfied with a reduced power language, or when you want to go all the way in the opposite direction and write machine-checked proofs about your software.

As we study these things more, we find ways of easing the burden of using languages that aren't Turing complete. Maybe in the far future, systems will be good enough that most software can comfortably be written in languages that aren't Turing complete. It's a worthy aspiration.

It's not now, though.

In layman's terms, it is impossible to determine certain properties of an arbitrary program written in a Turing-complete language. Properties like "will this program finish within a reasonable amount of time?" or "does program X do the same thing as program Y?"

For a non-turing-complete language, it may be possible to test such properties.

It's crucial to understand that this distinction is not one of how practical it is to determine properties; once you open the door to Turing-completeness, all ability to reason about a program effectively flies out the window. You might be able to come up with rules-of-thumb that determine an interesting property of a program in a Turing-complete language some of the time, but there will always exist programs for which your rules-of-thumb are insufficient.

Here's a practical example of why it's beneficial to not be Turing complete. In Dhall, you can normalize programs, even if they are functions. For example, the interpreter can automatically simplify this Dhall function:

        let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate

    in  let exclaim = λ(t : Text) → t ++ "!"

    in  λ(x : Text) → replicate +3 Text (exclaim x)

... to this one:

    λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"]

... even though we haven't applied the function to any arguments yet. You can't perform this sort of simplification (in general) if the language is Turing-complete

This sort of automatic simplification comes in handy a lot when authoring configuration files. For example, if somebody objects to the import of the remote `replicate` function, you can just simplify the file and (voila!) all the imports are gone because they've all been inlined and reduced. Similarly, if somebody objects to excessive use of abstraction and functions you can similarly simplify them to remove all indirection

Security.

A lot of security vulnerabilities in programs essentially boil down to your code being an ad-hoc parser for an (often implicit) language that's more powerful than you wanted. Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it.

This is a very insightful way of looking at things, and is a research area called langsec.

See:

- http://langsec.org/

- Papers and public talks of Meredith L. Patterson

- https://www.gwern.net/Turing-complete for some examples of unexpected Turing-completeness

Other popular non-Turing-complete languages are TeX and SQL.

In practice, the fact that the program cannot hang is probably the biggest point. Every programmer has experienced bugs where the program runs into an infinite loop or deadlocks. Those are the nastier bugs. Removing Turing-completeness removes that whole class of bugs, similar to how Rust removes the whole class of data race bugs.

Yes, however standardizing the language is higher priority at the moment

The whole point is if this (or something similar) was well known then you wouldn't have to use shitty typeless stuff like JSON...

The author has a bunch of similarly named projects (Morte, Annah).