10 ms·
Dhall: a programmable configuration language that is not Turing-complete
- Karrot_Kream 9y agoI see you allude to Terraform, but will you ever write a dhall specific compiler for Terraform configs?
- Gabriel439 9y agoYes, however standardizing the language is higher priority at the moment
- qznc 9y agoInteresting. I’m pondering non-turing-complete languages myself. I believe they are under-estimated and should be used more often for anything that looks like configuration. Configurations usually start simple, like we only need “x = y” statements. Oh wait, sections would be nice, so use the ini-format. Oh wait, nesting stuff would be nice, so use JSON/XML/Lisp. Oh wait, we want to reduce duplicated stuff, so use a preprocessor. Oh wait, more abstractions would be nice, so use some scripting language already. Stop, we just skipped one level before scripting languages, the non-turing-complete languages! Concerning Dhall, I never met the “Oh wait, we want to annotate types” idea. Is that really desireable for configurations?
- man-and-laptop 9y agoSubtraction: let pred = λ(n : Natural) → (Natural/fold n { prev : Natural, next : Natural } (λ(p : { prev : Natural, next : Natural }) → { prev : p.next, next : p.next + +1}) { prev : 0, next : 0 }).prev in λ(x : Natural) → λ(y : Natural) → Natural/fold y Natural pred x The Ackermann function: let iter = λ(f : Natural → Natural) → λ(n : Natural) → Natural/fold n Natural f (f (1)) in λ(m : Natural) → Natural/fold m (Natural → Natural) iter (+ +1) Save the above to 'ack' and run the following: $ dhall <<< './ack 10 10' It's going to take a while before it finishes. This language is close to Turing complete.
- lomnakkus 9y agoYes? 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.)
- man-and-laptop 9y agoPerhaps I should've added a :P to the end of that. See Gabriel's response here: https://news.ycombinator.com/item?id=15187733 https://news.ycombinator.com/item?id=15187733
- imtringued 9y agoIt's only guaranteed to terminate. That doesn't mean it's guaranteed to terminate before the heat death of the universe.
- networked 9y agoCan you limit evaluation to N reductions?
- Gabriel439 9y agoAuthor here: you could in principle, but in practice neither the library nor the executable compiler provide out-of-the-box support for limiting the number of reductions Dhall's basic approach to safety is: * make it impossible to intentionally do something malicious (such as destroying something important) * make it hard to unintentionally do something incorrect or inconvenient (such as running for a long time) For example, you can intentionally write a program that takes a very long time to run if you want to, but you will almost certainly know you are doing so; it's hard to write such a program by accident. In general, programming in a non-Turing-complete language forces you to structure code in such a way that potentially long-running code is more "obvious" than in Turing-complete languages.
- 9y ago
- kronos29296 9y agoTotally off topic but Liked the name and the reference to Planescape Torment. (My favourite RPG)
- icen 9y agoThe author has a bunch of similarly named projects (Morte, Annah).
- JackC 9y agoMaybe I'm just not the target audience, but I found this intriguing yet confusing. It might benefit from an explanation of typical use cases -- what do people do now that Dhall would be a better tool for? I read the tagline: "Dhall is a programmable configuration language that is not Turing-complete," so I figured "programmable configuration language" was a term I just wasn't familiar with, and it might bring up some typical use cases if I searched for it -- but it seems like that term was invented for Dhall. So maybe the kind of example I'm looking for is: if you're now using a non-programmable configuration language, here's what that would look like, and here's the improvement if you switch to Dhall. Or if you're now using a programmable configuration language that is Turing complete, here's what that would look like, and here's the improvement if you switch to Dhall. (A more specific question: in what kind of scenarios is JSON+arbitrary terminating functions useful?)
- TeMPOraL 9y agoIt'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 https://news.ycombinator.com/item?id=15190110. TL;DR: langsec.
- nathancahill 9y agoMore 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 https://varnish-cache.org/docs/3.0/tutorial/vcl.html
- kreetx 9y agoI 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.
- 9y ago
- azeirah 9y agoI understand that Turing completeness is not always a desirable quality for your programming language of choice, but since it is a rather obscure thing for those of us who haven't studied CS, when is a non-turing-complete language a favorable choice compared to a more traditional turing complete one?
- TeMPOraL 9y agoSecurity. 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/ http://langsec.org/ - Papers and public talks of Meredith L. Patterson - https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete for some examples of unexpected Turing-completeness
- chriswarbo 9y ago> Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it. Can I ask why Turing-completeness is "especially dangerous"? Let's say we have a pure language for e.g. generating a JSON value (nested lists/maps of strings, floats, nulls and booleans). It has no primitives other than null, true/false, string, float, list, map and function literals, and corresponding "arithmetic" functions for each type. What would the safety and security differences be between such a language being Turing-complete and not being Turing-complete? Programs in these languages can't "do" anything, other than calculate. The only problem I can think of is making denial-of-service easier, by e.g. generating an infinitely large list and running out of memory: (\x -> [ null ] ++ (x x)) (\x -> [ null ] ++ (x x)) This will generate `[ null, null, null, ... ]` until it runs out of memory. However, we could still blow the memory without Turing-completeness, e.g. by growing an exponentially large datastructure for a large number of steps (basically like a zip bomb): (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) [ null, null, null, null, null, ...and so on 1000 times ] This recursion is well-founded, and structurally-decreasing since we only call `f` with a strictly-decreasing value of `xs`, until we hit the base-case for `xs = nil` where we return `[ null ]`. In the non-base-case we recurse twice to generate two identical lists, then append them together. This results in a list with 2^1000 elements, easily consuming all available memory. Hence for security, we need to kill programs which go over some predefined time/memory bounds regardless of whether or not they're Turing-complete. Hence my question about whether or not Turing-completeness is "especially dangerous", in comparison to e.g. I/O primitives.
- thesmallestcat 9y agoWhat they're attempting here is interesting, but for configuration, I like a well-known real language, or a well-known, simple configuration language (ini, shell/env vars, JSON...). This to me is an awkward middle ground.
- _ibu9 9y agoThe whole point is if this (or something similar) was well known then you wouldn't have to use shitty typeless stuff like JSON...
- skybrian 9y agoIt's not typeless if you validate it using a schema. (For example, there are JSON encodings of protobufs, where validation will be done when the file is read.)
- jopsen 9y agoWe recently did a similar thing, phrased as json-expressions, ie. a json structure that evals to another... https://taskcluster.github.io/json-e/ https://taskcluster.github.io/json-e/
- sly010 9y agoEvery configuration documentation is full of wagely defined or undefined combination of options and "this-flag-cannot-be-used-together-with-that-flag" clauses. Often these things are not even documented but are implicit. e.g. in systemd service definitions depending on your service "Type" the meaning and the validity of the other properties change. (e.g. Type=oneshot cannot have ExecStart) Statically typed languages allow you to create very elegant configuration DSLs so the user cannot create invalid programs (where invalid can mean whatever the DSL creator wants). But most software is written to read shitty (untyped) configuration languages. I always wished config files were not a soup of magic keywords but typed datastructures (talking to you, every yaml configuration file ever). It looks like Dhall is just a statically typed and functional language that allows you to create a nice typed DSLs to generate always valid config files. It's at least worth a closer look.
- touisteur 9y agoTalking 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.pdf 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.md 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.