HN Gopher Feed (2017-09-06) - page 1 of 10 ___________________________________________________________________
Dhall: a programmable configuration language that is not Turing-
complete
95 points by happy-go-lucky
https://github.com/dhall-lang/dhall-lang/blob/master/README.md___________________________________________________________________
azeirah - 2 hours ago
I 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?
chowells - 1 hours ago
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.
RodgerTheGreat - 57 minutes ago
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.
tincholio - 1 hours ago
For instance, if you want to make guarantees about program
termination (as the author does here). This is not possible for
Turing complete languages.
dozzie - 2 hours ago
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.
Gabriel439 - 36 minutes ago
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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc
6Ccx/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-completeThis 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
lmkg - 1 hours ago
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.
jkabrg - 2 hours ago
Subtraction: 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.
danidiaz - 54 minutes ago
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.
[deleted]
imtringued - 1 hours ago
It's only guaranteed to terminate. That doesn't mean it's
guaranteed to terminate before the heat death of the universe.
networked - 1 hours ago
Can you limit evaluation to N reductions/function calls?
Gabriel439 - 17 minutes ago
Author 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 reductionsDhall'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.
ameliaquining - 1 hours ago
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.)
sly010 - 1 hours ago
Every 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.
kronos29296 - 2 hours ago
Totally off topic but Liked the name and the reference to
Planescape Torment. (My favourite RPG)
JackC - 2 hours ago
Maybe 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?)
kreetx - 2 hours ago
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.
andolanra - 1 hours ago
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.
Gabriel439 - 28 minutes ago
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 ScalaHowever, 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
nathancahill - 2 hours ago
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
KirinDave - 1 hours ago
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.
nathancahill - 1 hours ago
Interesting, can you share the link you were submitting? I
looked through your submissions but didn't see it.
thesmallestcat - 1 hours ago
What 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.
kmicklas - 8 minutes ago
The whole point is if this (or something similar) was well known
then you wouldn't have to use shitty typeless stuff like JSON...
jopsen - 1 hours ago
We recently did a similar thing, phrased as json-expressions, ie. a
json structure that evals to
another...https://taskcluster.github.io/json-e/