Dhall.Tutorial

Dhall is a programming language specialized for configuration files. This module contains a tutorial explaning how to author configuration files using this language

Introduction

The simplest way to use Dhall is to ignore the programming language features and use it as a strongly typed configuration format. For example, suppose that you create the following configuration file:

$ cat ./config
{ foo = 1
, bar = [3.0, 4.0, 5.0] : List Double
}

You can read the above configuration file into Haskell using the following code:

-- example.hs

{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE OverloadedStrings #-}

import Dhall

data Example = Example { foo :: Integer, bar :: Vector Double }
    deriving (Generic, Show)

instance Interpret Example

main :: IO ()
main = do
    x <- input auto "./config"
    print (x :: Example)

If you compile and run the above example, the program prints the corresponding Haskell record:

$ ./example
Example {foo = 1, bar = [3.0,4.0,5.0]}

You can also load some types directly into Haskell without having to define a record, like this:

>>> :set -XOverloadedStrings
>>> input auto "True" :: IO Bool
True

The input function can decode any value if we specify the value's expected Type:

input
    :: Type a  -- Expected type
    -> Text    -- Dhall program
    -> IO a    -- Decoded expression

... and we can either specify an explicit type like bool:

bool :: Type Bool

input bool :: Text -> IO Bool

input bool "True" :: IO Bool

>>> input bool "True"
True

... or we can use auto to let the compiler infer what type to decode from the expected return type:

auto :: Interpret a => Type a

input auto :: Interpret a => Text -> IO a

>>> input auto "True" :: IO Bool
True

You can see what types auto supports "out-of-the-box" by browsing the instances for the Interpret class. For example, the following instance says that we can directly decode any Dhall expression that evaluates to a Bool into a Haskell Bool:

instance Interpret Bool

... which is why we could directly decode the string "True" into the value True.

There is also another instance that says that if we can decode a value of type a, then we can also decode a List of values as a Vector of as:

instance Interpret a => Interpret (Vector a)

Therefore, since we can decode a Bool, we must also be able to decode a List of Bools, like this:

>>> input auto "[True, False] : List Bool" :: IO (Vector Bool)
[True,False]

We could also specify what type to decode by providing an explicit Type instead of using auto with a type annotation:

>>> input (vector bool) "[True, False] : List Bool"
[True, False]

Exercise: Create a ./config file that the following program can decode:

{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE OverloadedStrings #-}

import Dhall

data Person = Person { age :: Natural, name :: Text }
    deriving (Generic, Show)

instance Interpret Person

main :: IO ()
main = do
    x <- input auto "./config"
    print (x :: Person)

Exercise: Create a ./config file that the following program can decode:

{-# LANGUAGE OverloadedStrings #-}

import Data.Functor.Identity
import Dhall

instance Interpret a => Interpret (Identity a)

main :: IO ()
main = do
    x <- input auto "./config"
    print (x :: Identity Double)

Types

Suppose that we try to decode a value of the wrong type, like this:

>>> input auto "1" :: IO Bool
*** Exception: 
Error: Expression doesn't match annotation

1 : Bool

(input):1:1

The interpreter complains because the string "1" cannot be decoded into a Haskell value of type Bool.

The code excerpt from the above error message has two components:

• the expression being type checked (i.e. 1)
• the expression's expected type (i.e. Bool)

Expression
⇩
1 : Bool
    ⇧
    Expected type

The (:) symbol is how Dhall annotates values with their expected types. This notation is equivalent to type annotations in Haskell using the (::) symbol. Whenever you see:

x : t

... you should read that as "we expect the expression x to have type t". However, we might be wrong and if our expected type does not match the expression's actual type then the type checker will complain.

In this case, the expression 1 does not have type Bool so type checking fails with an exception.

Exercise: Load the Dhall library into ghci and run these commands to get get a more detailed error message:

>>> import Dhall
>>> :set -XOverloadedStrings
>>> detailed (input auto "1") :: IO Bool
...

... then read the entire error message

Exercise: Fix the type error, either by changing the value to decode or changing the expected type

Imports

You might wonder why in some cases we can decode a configuration file:

>>> writeFile "bool" "True"
>>> input auto "./bool" :: IO Bool
True

... and in other cases we can decode a value directly:

>>> input auto "True" :: IO Bool
True

This is because importing a configuration from a file is a special case of a more general language feature: Dhall expressions can reference other expressions by their file path.

To illustrate this, let's create three files:

$ echo "True"  > bool1
$ echo "False" > bool2
$ echo "./bool1 && ./bool2" > both

... and read in all three files in a single expression:

>>> input auto "[ ./bool1 , ./bool2 , ./both ] : List Bool" :: IO (Vector Bool)
[True,False,False]

Each file path is replaced with the Dhall expression contained within that file. If that file contains references to other files then those references are transitively resolved.

In other words: configuration files can reference other configuration files, either by their relative or absolute paths. This means that we can split a configuration file into multiple files, like this:

$ cat > ./config <<EOF
{ foo = 1
, bar = ./bar
}
EOF

$ echo "[ 3.0, 4.0, 5.0 ] : List Double" > ./bar

$ ./example
Example {foo = 1, bar = [3.0,4.0,5.0]}

However, the Dhall language will forbid cycles in these file references. For example, if we create the following cycle:

$ echo './file1' > file2
$ echo './file2' > file1

... then the interpreter will reject the import:

>>> input auto "./file1" :: IO Integer
*** Exception: 
↳ ./file1
  ↳ ./file2

Cyclic import: ./file1

You can also import expressions by URL. For example, you can find a Dhall expression hosted at this URL using ipfs:

https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB

$ curl https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB
True

... and you can reference that expression either directly:

>>> input auto "https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
True

... or inside of a larger expression:

>>> input auto "False == https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
False

You're not limited to hosting Dhall expressions on ipfs. You can host a Dhall expression anywhere that you can host UTF8-encoded text on the web, such as Github, a pastebin, or your own web server.

You can import types, too. For example, we can change our ./bar file to:

$ echo "[ 3.0, 4.0, 5.0 ] : List ./type" > ./bar

... then specify the ./type in a separate file:

$ echo "Double" > ./type

... and everything still type checks:

$ ./example
Example {foo = 1, bar = [3.0,4.0,5.0]}

Note that all imports must be terminated by whitespace or you will get either an import error or a parse error, like this:

>>> writeFile "baz" "2.0"
>>> input auto "./baz: Double" :: IO Double
*** Exception: 
↳ ./baz: 

Error: Missing file

This is because the parser thinks that ./baz: is a single token due to the missing whitespace before the colon and tries to import a file named ./baz:, which does not exist. To fix the problem we have to add a space after ./baz:

>>> input auto "./baz : Double" :: IO Double
2.0

Exercise: There is a not function hosted online here:

https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not

Visit that link and read the documentation. Then try to guess what this code returns:

>>> input auto "https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
???

Run the code to test your guess

Lists

You can store 0 or more values of the same type in a list, like this:

[1, 2, 3] : List Integer

Every list must be followed by the type of the list. The type annotation is not optional and you will get an error if you omit the annotation:

>>> input auto "[1, 2, 3]" :: IO (Vector Integer)
*** Exception: (input):1:10: error: unexpected
    EOF, expected: ":"
[1, 2, 3]<EOF> 
         ^     

Also, list elements must all have the same type which must match the declared type of the list. You will get an error if you try to store any other type of element:

input auto "[1, True, 3] : List Integer" :: IO (Vector Integer)
*** Exception: 
Error: List element has the wrong type

[1, True, 3] : List Integer

(input):1:1

Exercise: Create a ./config file that decodes to the following result:

>>> input auto "./config" :: IO (Vector (Vector Integer))
[[1,2,3],[4,5,6]]

Optional values

Optional values are exactly like lists except they can only hold 0 or 1 elements. They cannot hold 2 or more elements:

For example, these are valid Optional values:

[1] : Optional Integer

[]  : Optional Integer

... but this is not valid:

[1, 2] : Optional Integer  -- NOT valid

An Optional corresponds to Haskell's Maybe type for decoding purposes:

>>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)
Just 1
>>> input auto "[] : Optional Integer" :: IO (Maybe Integer)
Nothing

Exercise: What is the shortest possible ./config file that you can decode like this:

>>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))
???

Exercise: Try to decode an Optional value with more than one element and see what happens

Records

Record literals are delimited by curly braces and their fields are separated by commas. For example, this is a valid record literal:

{ foo = True
, bar = 2
, baz = 4.2
}

A record type is like a record literal except instead of specifying each field's value we specify each field's type. For example, the preceding record literal has the following record type:

{ foo : Bool
, bar : Integer
, baz : Double
}

If you want to specify an empty record literal, you must use {=}, which is special syntax reserved for empty records. If you want to specify the empty record type, then you use {}. If you forget which is which you can always ask the dhall compiler to remind you of the type for each one:

$ dhall
{=}
<Ctrl-D>
{}

{=}

$ dhall
{}
<Ctrl-D>
Type

{}

You can access a field of a record using the following syntax:

record.fieldName

... which means to access the value of the field named fieldName from the record. For example:

>>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double
4.2

Exercise: What is the type of this record:

{ foo = 1
, bar =
    { baz = 2.0
    , qux = True
    }
}

Exercise: Save the above code to a file named ./record and then try to access the value of the baz field

Functions

The Dhall programming language also supports user-defined anonymous functions. For example, we can save the following anonymous function to a file:

$ cat > makeBools
\(n : Bool) ->
        [ n && True, n && False, n || True, n || False ] : List Bool
<Ctrl-D>

... or we can use Dhall's support for Unicode characters to use λ (U+03BB) instead of \ and → (U+2192) instead of -> (for people who are into that sort of thing):

$ cat > makeBools
λ(n : Bool) →
        [ n && True, n && False, n || True, n || False ] : List Bool
<Ctrl-D>

You can read either one as a function of one argument named n that has type Bool. This function returns a List of Bools. Each element of the List depends on the input argument.

The (ASCII) syntax for anonymous functions resembles the syntax for anonymous functions in Haskell. The only difference is that Dhall requires you to annotate the type of the function's input.

We can test our makeBools function directly from the command line. This library comes with a command-line executable program named dhall that you can use to both type-check files and convert them to a normal form. Our compiler takes a program on standard input and then prints the program's type to standard error followed by the program's normal form to standard output:

$ dhall
./makeBools
<Ctrl-D>
∀(n : Bool) → List Bool

λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool

The first line says that makeBools is a function of one argument named n that has type Bool and the function returns a List of Bools. The ∀ (U+2200) symbol is shorthand for the ASCII forall keyword:

∀(x : a) → b        -- This type ...

forall (x : a) → b  -- ... is the same as this type

... and Dhall's forall keyword behaves the same way as Haskell's forall keyword for input values that are Types:

forall (x : Type) → b  -- This Dhall type ...

forall x . b           -- ... is the same as this Haskell type

The part where Dhall differs from Haskell is that you can also use ∀/forall to give names to non-Type arguments (such as the first argument to makeBools).

The second line of Dhall's output is our program's normal form:

λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool

... which in this case happens to be identical to our original program.

To apply a function to an argument you separate the function and argument by whitespace (just like Haskell):

f x

You can read the above as "apply the function f to the argument x". This means that we can "apply" our ./makeBools function to a Bool argument like this:

$ dhall
./makeBools True
<Ctrl-D>
List Bool

[True, False, True, True] : List Bool

Remember that file paths are synonymous with their contents, so the above code is exactly equivalent to:

$ dhall
(λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) True
<Ctrl-D>
List Bool

[True, False, True, True] : List Bool

When you apply an anonymous function to an argument, you substitute the "bound variable" with the function's argument:

   Bound variable
   ⇩
(λ(n : Bool) → ...) True
                    ⇧
                    Function argument

So in our above example, we would replace all occurrences of n with True, like this:

-- If we replace all of these `n`s with `True` ...
[n && True, n && False, n || True, n || False] : List Bool

-- ... then we get this:
[True && True, True && False, True || True, True || False] : List Bool

-- ... which reduces to the following normal form:
[True, False, True, True] : List Bool

Now that we've verified that our function type checks and works, we can use the same function within Haskell:

>>> input auto "./makeBools True" :: IO (Vector Bool)
[True,False,True,True]

Exercise: Create a file named getFoo that is a function of the following type:

∀(r : { foo : Bool, bar : Text }) → Bool

This function should take a single input argument named r that is a record with two fields. The function should return the value of the foo field.

Exercise: Use the dhall compiler to infer the type of the function you just created and verify that your function has the correct type

Exercise: Use the dhall compiler to apply your function to a sample record

Combine

You can combine two records, using the (/\) operator or the corresponding Unicode (∧) (U+2227) operator:

$ dhall
{ foo = 1, bar = "ABC" } /\ { baz = True }
<Ctrl-D>
{ bar : Text, baz : Bool, foo : Integer }

{ bar = "ABC", baz = True, foo = 1 }

$ dhall
{ foo = 1, bar = "ABC" } ∧ { baz = True }  -- Fancy unicode
<Ctrl-D>
{ bar : Text, baz : Bool, foo : Integer }

{ bar = "ABC", baz = True, foo = 1 }

Note that the order of record fields does not matter. The compiler automatically sorts the fields when normalizing expressions.

The (∧) operator also merges records recursively. For example:

$ dhall
{ foo = { bar = True }, baz = "ABC" } ∧ { foo = { qux = 1.0 } }
<Ctrl-D>
{ baz : Text, foo : { bar : Bool, qux : Double } }

{ baz = "ABC", foo = { bar = True, qux = 1.0 } }

However, you cannot combine two records if they share a field that is not a record:

$ dhall
{ foo = 1, bar = "ABC" } ∧ { foo = True }
<Ctrl-D>
Use "dhall --explain" for detailed errors

Error: Field collision

{ foo = 1, bar = "ABC" } ∧ { foo = True }

(stdin):1:1

Exercise: Combine any record with the empty record. What do you expect to happen?

Let expressions

Dhall also supports let expressions, which you can use to define intermediate values in the course of a computation, like this:

$ dhall
let x = "ha" in x ++ x
<Ctrl-D>
Text

"haha"

You can also annotate the types of values defined within a let expression, like this:

$ dhall
let x : Text = "ha" in x ++ x
<Ctrl-D>
Text

"haha"

Every let expression of the form:

let x : t = y in e

... is exactly equivalent to:

(λ(x : t) → e) y

So for example, this let expression:

let x : Text = "ha" in x ++ x

... is equivalent to:

(λ(x : Text) → x ++ x) "ha"

... which in turn reduces to:

"ha" ++ "ha"

... which in turn reduces to:

"haha"

You need to nest let expressions if you want to define more than one value in this way:

$ dhall
    let x = "Hello, "
in  let y = "world!"
in  x ++ y
<Ctrl-D>
Text

"Hello, world!"

Dhall is whitespace-insensitive, so feel free to format things over multiple lines or indent in any way that you please.

If you want to define a named function, just give a name to an anonymous function:

$ dhall
let twice = λ(x : Text) → x ++ x in twice "ha"
<Ctrl-D>
Text

"haha"

Unlike Haskell, Dhall does not support function arguments on the left-hand side of the equals sign, so this will not work:

$ dhall
let twice (x : Text) = x ++ x in twice "ha"
<Ctrl-D>
(stdin):1:11: error: expected: ":",
    "="
let twice (x : Text) = x ++ x in twice "ha" 
          ^

The error message says that Dhall expected either a (:) (i.e. the beginning of a type annotation) or a (=) (the beginning of the assignment) and not a function argument.

You can also use let expressions to rename imports, like this:

$ dhall
let not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
in  not True
<Ctrl-D>
Bool

False

Exercise: What do you think the following code will normalize to?

    let x = 1
in  let x = 2
in  x

Test your guess using the dhall compiler

Exercise: Now try to guess what this code will normalize to:

    let x = "ha"
in  let x = x ++ "ha"
in  x

Exercise: What about this code?

let x = x ++ "ha"
in  x

Unions

A union is a value that can be one of many alternative types of values. For example, the following union type:

< Left : Natural | Right : Bool >

... represents a value that can be either a Natural or a Bool value. If you are familiar with Haskell these are exactly analogous to Haskell's "sum types".

Each alternative is associated with a tag that distinguishes that alternative from other alternatives. In the above example, the Left tag is used for the Natural alternative and the Right tag is used for the Bool alternative.

A union literal specifies the value of one alternative and the types of the remaining alternatives. For example, both of the following union literals have the same type, which is the above union type:

< Left  = +0   | Right : Bool    >

< Right = True | Left  : Natural >

You can consume a union using the built-in merge function. For example, suppose we want to convert our union to a Bool but we want to behave differently depending on whether or not the union is a Natural wrapped in the Left alternative or a Bool wrapped in the Right alternative. We would write:

$ cat > process <<EOF
    λ(union : < Left : Natural | Right : Bool >)
→   let handlers =
            { Left  = Natural/even  -- Natural/even is a built-in function
            , Right = λ(b : Bool) → b
            }
in  merge handlers union : Bool
EOF

Now our ./process function can handle both alternatives:

$ dhall
./process < Left = +3 | Right : Bool >
<Ctrl-D>
Bool

False

$ dhall
./process < Right = True | Left : Natural >
<Ctrl-D>
Bool

True

Every merge has the following form:

merge handlers union : type

... where:

• union is the union you want to consume
• handlers is a record with one function per alternative of the union
• type is the declared result type of the merge

The merge function selects which function to apply from the record based on which alternative the union selects:

merge { Foo = f, ... } < Foo = x | ... > : t = f x : t

So, for example:

merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool
    = Natural/even +3 : Bool
    = False

... and similarly:

merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > : Bool
    = (λ(b : Bool) → b) True : Bool
    = True

Notice that each handler has to return the same type of result (Bool in this case) which must also match the declared result type of the merge.

Exercise: Create a list of the following type with at least one element: per alternative:

List < Left : Integer | Right : Double >

Polymorphic functions

The Dhall language supports defining polymorphic functions (a.k.a. "generic" functions) that work on more than one type of value. However, Dhall differs from Haskell by not inferring the types of these polymorphic functions. Instead, you must be explicit about what type of value the function is specialized to.

Take, for example, Haskell's identity function named id:

id :: a -> a
id = \x -> x

The identity function is polymorphic, meaning that id works on values of different types:

>>> id 4
4
>>> id True
True

The equivalent function in Dhall is:

λ(a : Type) → λ(x : a) → x

Notice how this function takes two arguments instead of one. The first argument is the type of the second argument.

Let's illustrate how this works by actually using the above function:

$ echo "λ(a : Type) → λ(x : a) → x" > id

If we supply the function alone to the compiler we get the inferred type as the first line:

$ dhall
./id
<Ctrl-D>
∀(a : Type) → ∀(x : a) → a

λ(a : Type) → λ(x : a) → x

You can read the type (∀(a : Type) → ∀(x : a) → a) as saying: "This is the type of a function whose first argument is named a and is a Type. The second argument is named x and has type a (i.e. the value of the first argument). The result also has type a."

This means that the type of the second argument changes depending on what type we provide for the first argument. When we apply ./id to Integer, we create a function that expects an Integer argument:

$ dhall
./id Integer
<Ctrl-D>
∀(x : Integer) → Integer

λ(x : Integer) → x

Similarly, when we apply ./id to Bool, we create a function that expects a Bool argument:

$ dhall
./id Bool
<Ctrl-D>
∀(x : Bool) → Bool

λ(x : Bool) → x

We can then supply the final argument to each of those functions to show that they both work on their respective types:

$ dhall
./id Integer 4
<Ctrl-D>
Integer

4

$ dhall
./id Bool True
<Ctrl-D>
Bool

True

Built-in functions can also be polymorphic, too. For example, we can ask the compiler for the type of List/reverse, the function that reverses a list:

$ dhall
List/reverse
<Ctrl-D>
∀(a : Type) → List a → List a

List/reverse

The first argument to List/reverse is the type of the list to reverse:

$ dhall
List/reverse Bool
<Ctrl-D>
List Bool → List Bool

List/reverse Bool

... and the second argument is the list to reverse:

$ dhall
List/reverse Bool ([True, False] : List Bool)
<Ctrl-D>
List Bool

[False, True] : List Bool

Note that the second argument has no name. This type:

∀(a : Type) → List a → List a

... is equivalent to this type:

∀(a : Type) → ∀(_ : List a) → List a

In other words, if you don't see the ∀ symbol surrounding a function argument type then that means that the name of the argument is "_". This is true even for user-defined functions:

$ dhall
λ(_ : Text) → 1
<Ctrl-D>
Text → Integer

λ(_ : Text) → 1

The type (Text → Integer) is the same as (∀(_ : Text) → Integer)

Exercise : Translate Haskell's flip function to Dhall

Total

Dhall is a total programming language, which means that Dhall is not Turing-complete and evaluation of every Dhall program is guaranteed to eventually halt. There is no upper bound on how long the program might take to evaluate, but the program is guaranteed to terminate in a finite amount of time and not hang forever.

This guarantees that all Dhall programs can be safely reduced to a normal form where as many functions have been evaluated as possible. In fact, Dhall expressions can be evaluated even if all function arguments haven't been fully applied. For example, the following program is an anonymous function:

$ dhall
\(n : Bool) -> +10 * +10
<Ctrl-D>
∀(n : Bool) → Natural

λ(n : Bool) → +100

... and even though the function is still missing the first argument named n the compiler is smart enough to evaluate the body of the anonymous function ahead of time before the function has even been invoked.

We can use the map function from the Prelude to illustrate an even more complex example:

$ dhall
    let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
in  λ(f : Integer → Integer) → List/map Integer Integer f ([1, 2, 3] : List Integer)
<Ctrl-D>
∀(f : Integer → Integer) → List Integer

λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer

Dhall can apply our function to each element of the list even before we specify which function to apply.

The language will also never crash or throw any exceptions. Every computation will succeed and produce something, even if the result might be an Optional value:

$ dhall
List/head Integer ([] : List Integer)
<Ctrl-D>
Optional Integer

[] : Optional Integer

Exercise: The Dhall Prelude provides a replicate function which you can find here:

https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate

Test what the following Dhall expression normalizes to:

let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate
in  replicate +10

Exercise: If you have a lot of spare time, try to "break the compiler" by finding an input expression that crashes or loops forever (and file a bug report if you succeed)

Built-in functions

Dhall is a restricted programming language that only supports simple built-in functions and operators. If you want to do anything fancier you will need to load your data into Haskell for further processing

This section covers types, functions, and operators that are built into the language, meaning that you do not need to import any code to use them. Additionally, Dhall also comes with a Prelude (covered in the next section) hosted online that contains functions derived from these base utilities. The Prelude also re-exports all built-in functions for people who prefer consistency.

The following documentation on built-ins is provided primarily as a reference. You don't need to read about every single built-in and you may want to skip to the following Prelude section.

Caveats

Dhall differs in a few important ways from other programming languages, so you should keep the following caveats in mind:

First, Dhall only supports addition and multiplication on Natural numbers (i.e. non-negative integers), which are not the same type of number as Integers (which can be negative). A Natural number is a number prefixed with the + symbol. If you try to add or multiply two Integers (without the + prefix) you will get a type error:

$ dhall
2 + 2
<Ctrl-D>
Use "dhall --explain" for detailed errors

Error: ❰+❱ only works on ❰Natural❱s

2 + 2

(stdin):1:1

In fact, there are no built-in functions for Integers (or Doubles). As far as the language is concerned they are opaque values that can only be shuffled around but not used in any meaningful way until they have been loaded into Haskell.

Second, the equality (==) and inequality (/=) operators only work on Bools. You cannot test any other types of values for equality.

Overview

Each of the following sections provides an overview of builtin functions and operators for each type. For each function you get:

• An example use of that function
• A "type judgement" explaining when that function or operator is well typed

For example, for the following judgement:

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x && y : Bool

... you can read that as saying: "if x has type Bool and y has type Bool, then x && y has type Bool"

Similarly, for the following judgement:

─────────────────────────────────
Γ ⊢ Natural/even : Natural → Bool

... you can read that as saying: "Natural/even always has type Natural → Bool"

• Rules for how that function or operator behaves

These rules are just equalities that come in handy when reasoning about code. For example, the section on (&&) has the following rules:

(x && y) && z = x && (y && z)

x && True = x

True && x = x

These rules are also a contract for how the compiler should behave. If you ever observe code that does not obey these rules you should file a bug report.

Bool

There are two values that have type Bool named True and False:

───────────────
Γ ⊢ True : Bool

────────────────
Γ ⊢ False : Bool

The built-in operations for values of type Bool are:

(||)

Example:

$ dhall
True || False
<Ctrl-D>
Bool

True

Type:

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x || y : Bool

Rules:

(x || y) || z = x || (y || z)

x || False = x

False || x = x

x || (y && z) = (x || y) && (x || z)

x || True = True

True || x = True

(&&)

Example:

$ dhall
True && False
<Ctrl-D>
Bool

False

Type:

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x && y : Bool

Rules:

(x && y) && z = x && (y && z)

x && True = x

True && x = x

x && (y || z) = (x && y) || (x && z)

x && False = False

False && x = False

(==)

Example:

$ dhall
True == False
<Ctrl-D>
Bool

False

Type:

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x == y : Bool

Rules:

(x == y) == z = x == (y == z)

x == True = x

True == x = x

x == x = True

(/=)

Example:

$ dhall
True != False
<Ctrl-D>
Bool

True

Type:

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x != y : Bool

Rules:

(x != y) != z = x != (y != z)

x != False = x

False != x = x

x != x = False

if/then/else

Example:

$ dhall
if True then 3 else 5
<Ctrl-D>
Integer

3

Type:

               Γ ⊢ t : Type
               ─────────────────────
Γ ⊢ b : Bool   Γ ⊢ l : t   Γ ⊢ r : t
────────────────────────────────────
Γ ⊢ if b then l else r

Rules:

if b then True else False = b

if True  then l else r = l

if False then l else r = r

Natural

Natural literals are numbers prefixed by a + sign, like this:

+4 : Natural

If you omit the + sign then you get an Integer literal, which is a different type of value

(+)

Example:

$ dhall
+2 + +3
<Ctrl-D>
Natural

+5

Type:

Γ ⊢ x : Natural   Γ ⊢ y : Natural
─────────────────────────────────
Γ ⊢ x + y : Natural

Rules:

(x + y) + z = x + (y + z)

x + +0 = x

+0 + x = x

(*)

Example:

$ dhall
+2 * +3
<Ctrl-D>
Natural

+6

Type:

Γ ⊢ x : Natural   Γ ⊢ y : Natural
─────────────────────────────────
Γ ⊢ x * y : Natural

Rules:

(x * y) * z = x * (y * z)

x * +1 = x

+1 * x = x

(x + y) * z = (x * z) + (y * z)

x * (y + z) = (x * y) + (x * z)

x * +0 = +0

+0 * x = +0

Natural/even

Example:

$ dhall
Natural/even +6
<Ctrl-D>
Bool

True

Type:

─────────────────────────────────
Γ ⊢ Natural/even : Natural → Bool

Rules:

Natural/even (x + y) = Natural/even x == Natural/even y

Natural/even +0 = True

Natural/even (x * y) = Natural/even x || Natural/even y

Natural/even +1 = False

Natural/odd

Example:

$ dhall
Natural/odd +6
<Ctrl-D>
Bool

False

Type:

────────────────────────────────
Γ ⊢ Natural/odd : Natural → Bool

Rules:

Natural/odd (x + y) = Natural/odd x /= Natural/odd y

Natural/odd +0 = False

Natural/odd (x * y) = Natural/odd x && Natural/odd y

Natural/odd +1 = True

Natural/isZero

Example:

$ dhall
Natural/isZero +6
<Ctrl-D>
Bool

False

Type:

───────────────────────────────────
Γ ⊢ Natural/isZero : Natural → Bool

Rules:

Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y

Natural/isZero +0 = True

Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y

Natural/isZero +1 = False

Natural/fold

Example:

$ dhall
Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome"
<Ctrl-D>
Text

"You're welcome!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"

Type:

──────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Natural/fold : Natural → ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural

Rules:

Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z)

Natural/fold +0 n s z = z

Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s)

Natural/fold 1 n s = s

Natural/build

Example:

$ dhall
Natural/build (λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ zero))
<Ctrl-D>
Natural

+2

Type:

─────────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Natural/build : (∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural) → Natural

Rules:

Natural/fold (Natural/build x) = x

Natural/build (Natural/fold x) = x

Integer

Integer literals are either prefixed with a - sign (if they are negative) or no sign (if they are positive), like this:

 3 : Integer
-2 : Integer

If you prefix them with a + sign then they are Natural literals and not Integers

There are no built-in operations on Integers. For all practical purposes they are opaque values within the Dhall language

Double

A Double literal is a floating point value with at least one decimal place, such as:

-2.0     : Double
 3.14159 : Double

There are no built-in operations on Doubles. For all practical purposes they are opaque values within the Dhall language

Text

A Text literal is just a sequence of characters enclosed in double quotes, like:

"ABC" : Text

The only thing you can do with Text values is concatenate them

(++)

Example:

$ dhall
"Hello, " ++ "world!"
<Ctrl-D>
Text

"Hello, world!"

Type:

Γ ⊢ x : Text   Γ ⊢ y : Text
───────────────────────────
Γ ⊢ x && y : Text

Rules:

(x ++ y) ++ z = x ++ (y ++ z)

x ++ "" = x

"" ++ x = x

List

Dhall List literals are a sequence of values inside of brackets separated by commas:

Γ ⊢ t : Type   Γ ⊢ x : t   Γ ⊢ y : t   ...
──────────────────────────────────────────
Γ ⊢ [x, y, ... ] : List t

Also, every List must end with a mandatory type annotation

The built-in operations on Lists are:

List/fold

Example:

$ dhall
List/fold Bool ([True, False, True] : List Bool) Bool (λ(x : Bool) → λ(y : Bool) → x && y) True
<Ctrl-D>
Bool

False

Type:

────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ List/fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list

Rules:

let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat

List/fold a (List/concat a xss) b c
    = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)

List/fold a ([] : List a) b c n = n

List/fold a ([x] : List a) b c = c x

List/build

Example:

$ dhall
List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))
<Ctrl-D>
List Integer

[1, 2, 3] : List Integer

Type:

───────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ List/build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a

Rules:

List/build t (List/fold t x) = x

List/fold t (List/build t x) = x

List/length

Example:

$ dhall
List/length Integer ([1, 2, 3] : List Integer)
<Ctrl-D>
Natural

+3

Type:

────────────────────────────────────────────────
Γ ⊢ List/length : ∀(a : Type) → List a → Natural

Rules:

List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0

List/head

Example:

$ dhall
List/head Integer ([1, 2, 3] : List Integer)
<Ctrl-D>
Optional Integer

[1] : Optional Integer

Type:

─────────────────────────────────────
Γ ⊢ List/head ∀(a : Type) → List a → Optional a

Rules:

let Optional/head  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/head
let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap
let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map

List/head a (List/concat a xss) =
    Optional/head a (List/map (List a) (Optional a) (List/head a) xss)

List/head a ([x] : List a) = [x] : Optional a

List/head b (List/concatMap a b f m)
    = Optional/concatMap a b (λ(x : a) → List/head b (f x)) (List/head a m)

List/last

Example:

$ dhall
List/last Integer ([1, 2, 3] : List Integer)
<Ctrl-D>
Optional Integer

[1] : Optional Integer

Type:

─────────────────────────────────────
Γ ⊢ List/last : ∀(a : Type) → List a → Optional a

Rules:

let Optional/last  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/last
let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap
let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map

List/last a (List/concat a xss) =
    Optional/last a (List/map (List a) (Optional a) (List/last a) xss)

List/last a ([x] : List a) = [x] : Optional a

List/last b (List/concatMap a b f m)
    = Optional/concatMap a b (λ(x : a) → List/last b (f x)) (List/last a m)

List/indexed

Example

$ dhall
List/indexed Text (["ABC", "DEF", "GHI"] : List Text)
<Ctrl-D>
List { index : Natural, value : Text }

[{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text }

Type:

─────────────────────────────────────────────────────────────────────────────
Γ ⊢ List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a }

Rules:

let List/shifted = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/shifted
let List/concat  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
let List/map     = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map

List/indexed a (List/concat a xss) =
    List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)

List/reverse

Example:

$ dhall
List/reverse Integer ([1, 2, 3] : List Integer)
<Ctrl-D>
List Integer

[3, 2, 1] : List Integer

Type:

─────────────────────────────────────────────────
Γ ⊢ List/reverse : ∀(a : Type) → List a → List a

Rules:

let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap

List/reverse a (List/concat a xss)
    = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss))

List/reverse a ([x] : List a) = [x] : List a

List/reverse b (List/concatMap a b f xs)
    = List/concatMap a b (λ(x : a) → List/reverse b (f x)) (List/reverse a xs)

List/reverse a ([x, y] : List a) = [y, x] : List a

Optional

Optional values are exactly like lists except they can only hold 0 or 1 elements. They cannot hold 2 or more elements:

For example, these are valid Optional values:

[1] : Optional Integer

[]  : Optional Integer

... but this is not valid:

[1, 2] : Optional Integer  -- NOT valid

An Optional corresponds to Haskell's Maybe type for decoding purposes:

>>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)
Just 1
>>> input auto "[] : Optional Integer" :: IO (Maybe Integer)
Nothing

Exercise: What is the shortest possible ./config file that you can decode like this:

>>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))
???

Exercise: Try to decode an Optional value with more than one element and see what happens

Optional/fold

Example:

$ dhall
Optional/fold Text (["ABC"] : Optional Text) Text (λ(t : Text) → t) ""
<Ctrl-D>
Text

"ABC"

Type:

─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(just : a → optional) → ∀(nothing : optional) → optional

Rules:

Optional/fold a ([]  : Optional a) o j n = n

Optional/fold a ([x] : Optional a) o j n = j x

Prelude

There is also a Prelude available at:

https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude

There is nothing "official" or "standard" about this Prelude other than the fact that it is mentioned in this tutorial. The "Prelude" is just a set of convenient utilities which didn't quite make the cut to be built into the language. Feel free to host your own custom Prelude if you want!

If you visit the above link you can browse the Prelude, which has a few subdirectories. For example, the Bool subdirectory has a not file located here:

https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not

The not function is just a UTF8-encoded text file hosted online with the following contents

$ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
{-
Flip the value of a `Bool`

Examples:

```
./not True = False

./not False = True
```
-}
let not : Bool → Bool
    =   λ(b : Bool) → b == False

in  not

The file could have been much shorter, like this:

λ(b : Bool) → b == False

... but all the functions exported from the Prelude try to be as self-documenting as possible by including:

• the name of the function
• the type of the function
• documentation (including a few examples)

The performance penalty for adding these helpful features is negligible.

You can use this not function either directly:

$ dhall
https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not True
<Ctrl-D>
Bool

False

... or assign the URL to a shorter name:

$ dhall
let Bool/not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
in  Bool/not True
<Ctrl-D>
Bool

False

Some functions in the Prelude just re-export built-in functions for consistency and documentation, such as PreludeNaturaleven, which re-exports the built-in Natural/even function:

$ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even
{-
Returns `True` if a number if even and returns `False` otherwise

Examples:

```
./even +3 = False

./even +0 = True
```
-}
let even : Natural → Bool
    =   Natural/even

in  even

You can also download the Prelude locally to your filesystem if you prefer using local relative paths instead of URLs. For example, you can use wget, like this:

$ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/
$ tree Prelude
Prelude
├── Bool
│   ├── and
│   ├── build
│   ├── even
│   ├── fold
│   ├── not
│   ├── odd
│   └── or
├── List
│   ├── all
│   ├── any
│   ├── build
│   ├── concat
│   ├── filter
│   ├── fold
│   ├── generate
│   ├── head
│   ├── indexed
│   ├── iterate
│   ├── last
│   ├── length
│   ├── map
│   ├── null
│   ├── replicate
│   ├── reverse
│   ├── shifted
│   └── unzip
├── Monoid
├── Natural
│   ├── build
│   ├── enumerate
│   ├── even
│   ├── fold
│   ├── isZero
│   ├── odd
│   ├── product
│   └── sum
├── Optional
│   ├── build
│   ├── concat
│   ├── fold
│   ├── head
│   ├── last
│   ├── map
│   ├── toList
│   └── unzip
└── Text
    └── concat

... or if you have an ipfs daemon running, you can mount the Prelude locally like this:

$ ipfs mount
$ cd /ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude

Browse the Prelude online to learn more by seeing what functions are available and reading their inline documentation:

https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude

Exercise: Try to use a new Prelude function that has not been covered previously in this tutorial

Conclusion

By this point you should be able to use the Dhall configuration language to author, import, and program configuration files. If you run into any issues you can report them at:

https://github.com/Gabriel439/Haskell-Dhall-Library/issues

You can also request features, support, or documentation improvements on the above issue tracker.

If you would like to contribute to the Dhall project you can try to port Dhall to other languages besides Haskell so that Dhall configuration files can be read into those languages, too.