Thursday, April 13, 2017

Use Dhall to configure Bash programs

Dhall is a non-Turing-complete programming language for configuration files, and if you are new to Dhall you might want to read the Dhall tutorial which explains how to use Dhall and several of the language features.

Dhall is currently adding support for new languages and file formats such as:

... and now Dhall supports Bash, too! I'm releasing the dhall-bash package which you can use to configure Bash programs using a strongly typed configuration language. This lets you carve out a typed subset of Bash in your scripts and share your configuration files with other languages that support Dhall.

This package provides a dhall-to-bash executable which can convert Dhall expressions to either Bash expressions or Bash variable declarations. For example, you can convert simple Dhall values like Text, Integers, Natural numbers, or Bools to Bash expressions, like this:

$ dhall-to-bash <<< '"ABC"'
ABC
$ dhall-to-bash <<< '2'
2
$ dhall-to-bash <<< '+2'
2
$ dhall-to-bash <<< 'True'
true

The output is a valid Bash expression which you can use directly or assign to a Bash variable, like this:

$ FOO=$(dhall-to-bash <<< '"ABC"')
$ echo "${FOO}"
ABC

You can convert more complex values like lists, records, and optional values into Bash statements by passing the --declare flag to dhall-to-bash:

$ dhall-to-bash --declare BAR <<< '{ name = "John Doe", age = +23 }'
declare -r -A BAR=([age]=23 [name]=$'John Doe')
$ dhall-to-bash --declare BAR <<< '[1, 2, 3]'
declare -r -A BAR=(1 2 3)
$ dhall-to-bash --declare BAR <<< '[] : Optional Natural'
unset BAR
$ dhall-to-bash --declare BAR <<< '[+2] : Optional Natural'
declare -r -i BAR=2

The --declare flag emits a valid Bash statement that you can pass to eval, like this:

$ eval $(dhall-to-bash --declare LIST <<< '[1, 2, 3]')
$ for i in "${LIST[@]}"; do echo "${i}"; done
1
2
3
$ eval $(dhall-to-bash --declare RECORD <<< '{ name = "John Doe", age = +23 }')
$ echo "Name: ${RECORD[name]}, Age: ${RECORD[age]}"
Name: John Doe, Age: 23


Code distribution

Dhall is also distributed programming language, meaning that you can reference code fragments by URL, like this:

$ dhall-to-bash --declare LIST
let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate
in  replicate +10 Bool True
<Ctrl-D>
declare -r -a LIST=(true true true true true true true true true true)

The above example illustrates how Dhall's Prelude is distributed over IPFS (which is like a distributed hashtable for the web).

You can also reference local code by path, too, just like Bash:

$ echo '"John Doe"' > ./name
$ echo '+23' > ./age
$ echo '{ name = ./name , age = ./age }' > ./config
$ dhall-to-bash --declare CONFIG <<< './config'
declare -r -A CONFIG=([age]=23 [name]=$'John Doe')
$ eval $(dhall-to-bash --declare CONFIG <<< './config')
$ echo "${CONFIG[age]}"
23
$ dhall-to-bash <<< './config .age'
23


Types

Dhall is also a typed language that never crashes, never throws exceptions, and never endlessly loops because a configuration file should never "break". Try to break the language if you don't believe me!

The strong type system also comes with user-friendly type errors that are concise by default:

$ dhall-to-bash --declare FOO
let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate
in  replicate 10 Bool True
<Ctrl-D>

replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a)List a

Error: Wrong type of function argument

replicate 10

(stdin):2:5

... but they can go into much more detail if you ask:

$ dhall-to-bash --declare FOO --explain
let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate
in  replicate 10 Bool True
<Ctrl-D>

replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a)List a

Error: Wrong type of function argument

Explanation: Every function declares what type or kind of argument to accept

For example:


    ┌───────────────────────────────┐
    │ λ(x : Bool)x : Bool → Bool │  This anonymous function only accepts
    └───────────────────────────────┘  arguments that have type ❰Bool❱
                        ⇧
                        The function's input type


    ┌───────────────────────────────┐
    │ Natural/even : Natural → Bool │  This built-in function only accepts
    └───────────────────────────────┘  arguments that have type ❰Natural❱

                     The function's input type


    ┌───────────────────────────────┐
    │ λ(a : Type)a : Type → Type │  This anonymous function only accepts
    └───────────────────────────────┘  arguments that have kind ❰Type❱
                        ⇧
                        The function's input kind


    ┌────────────────────┐
    │ List : Type → Type │  This built-in function only accepts arguments that
    └────────────────────┘  have kind ❰Type❱

             The function's input kind


For example, the following expressions are valid:


    ┌────────────────────────┐
    │ (λ(x : Bool)x) True │  ❰True❱ has type ❰Bool❱, which matches the type
    └────────────────────────┘  of argument that the anonymous function accepts


    ┌─────────────────┐
    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,


    ┌────────────────────────┐
    │ (λ(a : Type)a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
    └────────────────────────┘  of argument that the anonymous function accepts


    ┌───────────┐
    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
    └───────────┘  that that the ❰List❱ function accepts


However, you can not apply a function to the wrong type or kind of argument

For example, the following expressions are not valid:


    ┌───────────────────────┐
    │ (λ(x : Bool)x) "A" │  ❰"A"has type ❰Text❱, but the anonymous function
    └───────────────────────┘  expects an argument that has type ❰Bool❱


    ┌──────────────────┐
    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
    └──────────────────┘  expects an argument that has type ❰Natural❱


    ┌────────────────────────┐
    │ (λ(a : Type)a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
    └────────────────────────┘  function expects an argument of kind ❰Type❱


    ┌────────┐
    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
    └────────┘  argument that has kind ❰Type❱


You tried to invoke the following function:

↳ replicate

... which expects an argument of type or kind:

↳ Natural

... on the following argument:

↳ 10

... which has a different type or kind:

↳ Integer

Some common reasons why you might get this error:

● You omit a function argument by mistake:


    ┌───────────────────────┐
    │ List/head   [1, 2, 3] │
    └───────────────────────┘
                ⇧
                ❰List/head❱ is missing the first argument,
                which should be: ❰Integer❱


● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱

    ┌────────────────┐
    │ Natural/even 2 │
    └────────────────┘
                   ⇧
                   This should be ❰+2❱

────────────────────────────────────────────────────────────────────────────────

replicate 10

(stdin):2:5

These detailed explanations provide miniature language tutorials that help new users pick up the language basics as they go.


Conclusion

If you would like to use this project you can install dhall-bash from Hackage:

... or you can check out the original project on Github, too:

I'll continue to work on adding new Dhall integrations to other languages and file formats. If you would like to contribute there are already two projects started by others to provide native Dhall support in Rust and Scala:

... and if you're feeling more adventurous you can contribute Dhall bindings to a new programming language!