GOPHERSPACE.DE - P H O X Y
gophering on hngopher.com
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/