Dhall is a programmable configuration language that provides a non-repetitive alternative to YAML.
You can think of Dhall as: JSON + functions + types + imports
Note that while Dhall is programmable, Dhall is not Turing-complete. Many of Dhall's features take advantage of this restriction to provide stronger safety guarantees and more powerful tooling.
You can try the language live in your browser by visiting the official website:
- Getting Started
- Tutorials
- Features
- Documentation
- Standard Library
- Development Status
- Overview
- Design Philosophy
- Name
The easiest way to get started experimenting with Dhall is to install the
dhall-to-json
and/or dhall-to-yaml
executables, which enable you to
generate JSON and YAML, respectively, on the command line. Platform- and
runtime-specific installation instructions can be found in the Dhall
wiki.
For a short introduction, read:
To learn more about core language features, read:
For an even longer hands-on tutorial, read:
- Total - Evaluation always terminates and never hangs or infinitely loops
- Safe - Evaluation never crashes or throws exceptions
- Distributed - Expressions can reference other expressions by URL or path
- Strongly normalizing - All expressions (even functions) have a normal form
- Statically typed - Configurations can be validated ahead-of-time
- Strongly typed - No coercions, casts or subtyping
- Built-in data types - Includes lists, anonymous records and anonymous unions
The Dhall language originated as a Haskell-specific configuration file format and is expanding to support more languages and file formats. Consequently, the Haskell package for Dhall still hosts the official tutorial and language manual:
... which will eventually become a language-agnostic tutorial
You can also read about the original motivation behind the language here:
Finally, we have a cheatsheet for a very condensed overview and quick lookup:
Dhall's Standard Library is called Prelude
. It implements various utilities to
work with the builtin types. Where to find it:
- Official link - https://prelude.dhall-lang.org
- Github repo
- Nix:
both
dhall
anddhall.prelude
derivations are built, install thePrelude
with e.g.nix-env -iA nixpkgs.dhall.prelude
The current version and versioning policy is detailed in the Versioning document, and you can see the latest changes in the Changelog.
There is an effort under way to formalize the language semantics for Dhall, to help with porting it to other languages. If you would like to assist with either standardizing the language or creating new bindings just open a new issue or contribute to existing ones in the issue tracker.
You can use Dhall in one of three ways:
- Interpreter: You can install a language-independent command-line program that can import, type-check and evaluate Dhall expressions
- Language binding: You can use a language-specific library to load Dhall configuration files directly into your programs
- Compilers: You can compile Dhall expressions to several common configuration file formats using command-line utilities
I recommend the following progression for adopting Dhall:
- Install the interpreter to learn more about the language
- If you like what you see, then:
- If your preferred programming language supports Dhall:
- Use the language binding to configure your programs using Dhall
- If your language does not yet support Dhall
- Compile Dhall to a supported configuration format (such as JSON)
- If your preferred programming language supports Dhall:
The following sections tour each of these use cases in more detail
You can install a Dhall interpreter that can type-check and evaluate Dhall expressions from the command line. You can use this interpreter to:
-
Learn how the language works:
$ dhall <<< 'True && False' Bool False
The first line of output shows the inferred type of an expression:
$ dhall <<< 'List/length' ∀(a : Type) → List a → Natural List/length
The second line of output shows the fully evaluated normal form of an expression:
$ dhall <<< 'λ(x : Text) → let y = True in if y != False then x else "?"' ∀(x : Text) → Text λ(x : Text) → x
-
Validate a configuration file ahead of time against a schema:
$ cat config { foo = List/length Natural [2, 3, 5], bar = True && False }
$ cat schema { foo : Natural, bar : Bool }
Dhall lets you import expressions and types by their path:
$ dhall <<< './config : ./schema' { bar : Bool, foo : Natural } { bar = False, foo = 3 }
Schema validation is the same thing as a type annotation
-
Detect type errors:
$ dhall <<< 'λ(x : Integer) → x && True' Use "dhall --explain" for detailed errors Error: ❰&&❱ only works on ❰Bool❱s x && True (stdin):1:18
You can ask the type checker to go into more detail using the
--explain
flag:$ dhall --explain <<< 'λ(x : Integer) → x && True' x : Integer Error: ❰&&❱ only works on ❰Bool❱s Explanation: The ❰&&❱ operator expects two arguments that have type ❰Bool❱ For example, this is a valid use of ❰&&❱: ┌───────────────┐ │ True && False │ └───────────────┘ You provided this argument: ↳ x ... which does not have type ❰Bool❱ but instead has type: ↳ Integer ──────────────────────────────────────────────────────────────────────────────── x && True (stdin):1:18
-
Resolve remote expressions:
dhall <<< 'https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate' ∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a λ(n : Natural) → λ(a : Type) → λ(x : a) → List/build a (λ(list : Type) → λ(cons : a → list → list) → Natural/fold n list (cons x))
You can import arbitrary expressions by URL. In fact, the Dhall Prelude is hosted on GitHub to be imported in this way:
-
Reduce an expression to normal form:
$ cat ./example let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate let exclaim = λ(t : Text) → t ++ "!" in λ(x : Text) → replicate 3 Text (exclaim x)
You can reduce functions to normal form, even when they haven't been applied to all of their arguments
$ dhall <<< './example' ∀(x : Text) → List Text λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"] : List Text
The normal form is equivalent to the original program except stripped of all imports and indirection
Learn more:
You can use Dhall to configure programs written in other languages. This is the most common use case for Dhall: a type-safe and non-Turing-complete configuration language
Dhall currently supports four complete language bindings:
... and four language bindings in progress:
The following language bindings wrap prebuilt Dhall packages or executables:
go-dhallconfig
- Go package that wraps thedhall-to-json
executableclay-dhall
- C bindings to the Haskell library
The following bindings are not maintained but you may find them useful as a starting point:
You can load Dhall expressions into Haskell using the input
function:
>>> input auto "True && False' :: IO Bool
False
The compiler validates the expression against the expected type:
>>> input auto "1" :: IO Bool
*** Exception:
Error: Expression doesn't match annotation
1 : Bool
(input):1:1
You can even marshall some Dhall functions into Haskell:
>>> twice <- input auto "λ(x : Integer) → [x, x]" :: IO (Integer -> [Integer])
>>> twice 5
[5,5]
You can also decode Dhall expressions into Haskell types that derive
Generic
:
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
import Dhall
data Example = Example { foo :: Natural, bar :: Vector Double }
deriving (Generic, Show)
instance Interpret Example
main :: IO ()
main = do
x <- input auto "./config"
print (x :: Example)
... which reads in this configuration file:
$ cat ./config
{ foo = 1
, bar = [3.0, 4.0, 5.0]
}
... and prints the configuration:
$ ./example
Example {foo = 1, bar = [3.0,4.0,5.0]}
Learn more:
nixpkgs
provides a dhallToNix
utility which you can use to translate a
Dhall expression to the corresponding Nix expression. This lets you carve out
a typed and total subset of Nix
For example, this Dhall expression:
let
pkgs = import <nixpkgs> { };
in
pkgs.dhallToNix ''
{ foo = λ(x : Bool) → [x, x]
, bar = Natural/even 2
, baz = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Text/concat
}
''
... translates to this Nix expression
{ foo = x : [ x x ];
bar = true;
baz = xs:
(t: xs: t: cons:
builtins.foldl' (f: y: ys: f (cons y ys)) (ys: ys) xs
) {} xs {} (x: y: x + y) "";
}
Learn more:
You can load Dhall expressions into Ruby using Dhall.load
:
Dhall.load("True && False").then do |value|
value # => #<Dhall::Bool value=false>
end
You can even marshall Dhall functions into Ruby:
Dhall.load("λ(x : Integer) → [x, x]").then do |f|
f.call(1) # => #<Dhall::List elements=[#<Dhall::Natural value=1>, #<Dhall::Natural value=1>]>
end
Learn more:
You can compile Dhall expressions to other configuration formats, such as:
- JSON and YAML
- Bash declarations
- Text (i.e. Dhall as a template engine)
These compilers can only translate a subset of Dhall to these other formats. For example, you cannot translate Dhall functions to JSON
The dhall-to-json
executable lets you compile Dhall expressions to JSON:
$ dhall-to-json <<< '{ foo = 1, bar = True, baz = [1, 2, 3] }'
{"foo":1,"baz":[1,2,3],"bar":true}
YAML is already a superset of JSON, but the dhall-to-yaml
executable lets you
compile Dhall expressions to idiomatic YAML syntax, too:
dhall-to-yaml <<< '{ foo = 1, bar = True, baz = [1, 2, 3] }'
foo: 1
baz:
- 1
- 2
- 3
bar: true
Some configuration file formats are supersets of JSON such as the
HashiCorp configuration language (Used to configure terraform
) so you
can compile Dhall expressions to these configuration file formats, too.
Learn more:
You can also compile Dhall expressions to either Bash expressions:
$ dhall-to-bash <<< 'List/length Bool [True, False]'
2
... or Bash declarations:
$ dhall-to-bash --declare FOO <<< '{ bar = 1, baz = "ABC" }'
declare -r -A FOO=([bar]=1 [baz]=ABC)
$ eval $(dhall-to-bash --declare FOO <<< '{ bar = 1, baz = "ABC" }')
$ echo ${FOO[bar]}
1
$ echo ${FOO[baz]}
ABC
Learn more:
You can also use the dhall-to-text
executable as a template engine
For example, given this template:
$ cat function
λ(record : { name : Text
, value : Double
, taxed_value : Double
, in_ca : Bool
}
) → ''
Hello ${record.name}
You have just won ${Double/show record.value} dollars!
${ if record.in_ca
then "Well, ${Double/show record.taxed_value} dollars, after taxes"
else ""
}
''
... and this payload:
$ cat value
{ name = "Chris"
, value = 10000.0
, taxed_value = 6000.0
, in_ca = True
}
... you can apply the template to the payload and render the result using the
dhall-to-text
executable:
$ dhall-to-text <<< './function ./value'
Hello Chris
You have just won 10000.0 dollars!
Well, 6000.0 dollars, after taxes
Learn more:
Programming languages are all about design tradeoffs and the Dhall language uses the following guiding principles (in order of descending priority) that help navigate those tradeoffs:
-
Polish
The language should delight users. Error messages should be fantastic, execution should be snappy, documentation should be excellent, and everything should "just work".
-
Simplicity
When in doubt, cut it out. Every configuration language needs bindings to multiple programming languages, and the more complex the configuration language the more difficult to create new bindings. Let the host language that you bind to compensate for any missing features from Dhall.
-
Beginner-friendliness
Dhall needs to be a language that anybody can learn in a day and debug with little to no assistance from others. Otherwise people can't recommend Dhall to their team with confidence.
-
Robustness
A configuration language needs to be rock solid. The last thing a person wants to debug is their configuration file. The language should never hang or crash. Ever.
-
Consistency
There should only be one way to do something. Users should be able to instantly discern whether or not something is possible within the Dhall language or not.
The Dhall configuration language is also designed to negate many of the common objections to programmable configuration files, such as:
"Config files shouldn't be Turing complete"
Dhall is not Turing-complete. Evaluation always terminates, no exceptions
"Configuration languages become unreadable due to abstraction and indirection"
Every Dhall configuration file can be reduced to a normal form which eliminates all abstraction and indirection
"Users will go crazy with syntax and user-defined constructs"
Dhall is a very minimal programming language. For example: you cannot even compare strings for equality. The language also forbids many other common operations in order to force users to keep things simple
The biggest issue with using Dhall as a configuration language is that there are currently only Haskell bindings. If you would like to contribute bindings to another language then go for it, otherwise I will do my best to contribute them as time permits.
The language is named after a Dustman from the game Planescape: Torment who belongs to a faction obsessed with death (termination). The logo represents his quill and inkwell
The name rhymes with "tall"/"call"/"hall" (i.e. "dɔl" for a US speaker or "dɔːl" for a UK speaker using the International Phonetic Alphabet).