<story><title>Dhall: a programmable configuration language that is not Turing-complete</title><url>https://github.com/dhall-lang/dhall-lang/blob/master/README.md</url></story><parent_chain></parent_chain><comment><author>sly010</author><text>Every configuration documentation is full of wagely defined or undefined combination of options and &amp;quot;this-flag-cannot-be-used-together-with-that-flag&amp;quot; clauses. Often these things are not even documented but are implicit.&lt;p&gt;e.g. in systemd service definitions depending on your service &amp;quot;Type&amp;quot; the meaning and the validity of the other properties change. (e.g. Type=oneshot cannot have ExecStart)&lt;p&gt;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.&lt;p&gt;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&amp;#x27;s at least worth a closer look.</text></comment>
<story><title>Dhall: a programmable configuration language that is not Turing-complete</title><url>https://github.com/dhall-lang/dhall-lang/blob/master/README.md</url></story><parent_chain></parent_chain><comment><author>man-and-laptop</author><text>Subtraction:&lt;p&gt;&lt;pre&gt;&lt;code&gt;   let pred = λ(n : Natural) → (Natural&amp;#x2F;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&amp;#x2F;fold y Natural pred x
&lt;/code&gt;&lt;/pre&gt;
The Ackermann function:&lt;p&gt;&lt;pre&gt;&lt;code&gt;   let iter = λ(f : Natural → Natural) → λ(n : Natural) → Natural&amp;#x2F;fold n Natural f (f (1)) 
   in λ(m : Natural) → Natural&amp;#x2F;fold m (Natural → Natural) iter (+ +1)
&lt;/code&gt;&lt;/pre&gt;
Save the above to &amp;#x27;ack&amp;#x27; and run the following:
    $ dhall &amp;lt;&amp;lt;&amp;lt; &amp;#x27;.&amp;#x2F;ack 10 10&amp;#x27;
It&amp;#x27;s going to take a while before it finishes.&lt;p&gt;This language is close to Turing complete.</text></comment>