dhall-1.19.1: A configuration language guaranteed to terminate

Safe Haskell | None
Language | Haskell2010

Dhall.Tutorial

Contents

- Introduction
- Types
- Imports
- Lists
- Optional values
- Records
- Functions
- Compiler
- Strings
- Combine
- Let expressions
- Unions
- Polymorphic functions
- Total
- Headers
- Import integrity
- Raw text
- Formatting code
- Built-in functions
  - Caveats
  - Overview
  - `Bool`
    - `(||)`
    - `(&&)`
    - `(==)`
    - `(!=)`
    - `if`/`then`/`else`
  - `Natural`
    - `(+)`
    - `(*)`
    - `Natural/even`
    - `Natural/odd`
    - `Natural/isZero`
    - `Natural/fold`
    - `Natural/build`
  - `Integer`
  - `Double`
  - `Text`
    - `(++)`
  - `List`
    - `(#)`
    - `List/fold`
    - `List/build`
    - `List/length`
    - `List/head`
    - `List/last`
    - `List/indexed`
    - `List/reverse`
  - `Optional`
    - `Optional/fold`
- Prelude
- Conclusion
- Frequently Asked Questions (FAQ)

Description

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

Synopsis

# 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]
    }

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 :: Natural, 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 `a`s:

    instance Interpret a => Interpret (Vector a)

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

    >>> input auto "[True, False]" :: 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]"
    [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
    ...
    - Bool
    + Natural
    ...
    1 : Bool
    ...
    (input):1:1
    ...

The interpreter complains because the string `"1"` cannot be decoded into a Haskell value of type `Bool`. This part of the type error:

    - Bool
    + Natural

... means that the expected type was `Bool` but the inferred type of the expression `1` was `Natural`.

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 ]" :: 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]" > ./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 Natural
    *** Exception:
    ↳ ./file1
      ↳ ./file2
    ...
    Cyclic import: ./file1

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

https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True

    $ curl https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True
    True

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

    input auto "https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool

True

... or inside of a larger expression:

    input auto "False == https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool

False

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

You can also import Dhall expressions from environment variables, too:

    >>> System.Environment.setEnv "FOO" "1"
    >>> input auto "env:FOO" :: IO Natural
    1

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 .../baz:
    ...

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://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not

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

    >>> input auto "https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: 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]

Every list can be followed by the type of the list. The type annotation is required for empty lists but optional for non-empty lists. You will get a type error if you provide an empty list without a type annotation:

    >>> input auto "[]" :: IO (Vector Natural)
    *** Exception:
    ...Error...: An empty list requires a type annotation
    ...
    []
    (input):1:1

Also, list elements must all have the same type. You will get an error if you try to store elements of different types in a list:

    >>> input auto "[1, True, 3]" :: IO (Vector Natural)
    *** Exception:
    ...Error...: List elements should all have the same type
    ...
    - Natural
    + Bool
    ...
        True
    ...
    (input):1:5
    ...

Exercise: What is the shortest `./config` file that you can decode using this command:

    >>> input auto "./config" :: IO (Vector (Vector Natural))

# Optional values

`Optional` values are either of the form `Some aValue` or `None aType`.

For example, these are valid `Optional` values:

    Some 1

    None Natural

... which both have type `Optional Natural`

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

    >>> input auto "Some 1" :: IO (Maybe Natural)
    Just 1
    >>> input auto "None Natural" :: IO (Maybe Natural)
    Nothing

Exercise: Author a `./config` file that you can decode like this:

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

# 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 : Natural
    , 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

... and you can project out multiple fields into a new record using this syntax:

    someRecord.{ field₀, field₁, … }

For example:

    $ dhall
    { x = 1, y = True, z = "ABC" }.{ x, y }
    <Ctrl-D>
    { x : Natural, y : Bool }

    { x = 1, y = True }

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 ]
    <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 ]
    <Ctrl-D>

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

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.

You can import this function into Haskell, too:

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

The reason this works is that there is an `Interpret` instance for simple functions:

    instance (Inject a, Interpret b) => Interpret (a -> b)

Thanks to currying, this instance works for functions of multiple simple arguments:

    >>> dhallAnd <- input auto "λ(x : Bool) → λ(y : Bool) → x && y" :: IO (Bool -> Bool -> Bool)
    >>> dhallAnd True False
    False

However, you can't convert anything more complex than that (like a polymorphic or higher-order function). You will need to apply those functions to their arguments within Dhall before converting their result to a Haskell value.

Just like `Interpret`, you can derive `Inject` for user-defined data types:

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

    module Main where

    import Dhall

    data Example0 = Example0 { foo :: Bool, bar :: Bool }
        deriving (Generic, Inject)

    main = do
        f <- input auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar"
        print (f (Example0 { foo = True, bar = False }) :: Bool)
        print (f (Example0 { foo = True, bar = True  }) :: Bool)

The above program prints:

    False
    True

# Compiler

We can also 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, False, True, n ]

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 `Bool`s. 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 `Type`s:

    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, False, True, n ]

... and the interpreter was able to simplify our expression by noting that:

-     n && True  = n

-     n && False = False

-     n || True  = True

-     n || False = n

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]

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]) True
    <Ctrl-D>
    List Bool

    [True, False, True, True]

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]

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

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

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

# Strings

Dhall supports ordinary string literals with Haskell-style escaping rules:

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

    "Hello, \"world\"!"

... and Dhall also supports Nix-style multi-line string literals:

    dhall
    ''
        #!/bin/bash

        echo "Hi!"
    ''
    <Ctrl-D>
    Text

    "\n#!/bin/bash\n\necho \"Hi!\"\n"

These "double single quote strings" ignore all special characters, with one exception: if you want to include a `''` in the string, you will need to escape it with a preceding `'` (i.e. use `'''` to insert `''` into the final string).

These strings also strip leading whitespace using the same rules as Nix. Specifically: "it strips from each line a number of spaces equal to the minimal indentation of the string as a whole (disregarding the indentation of empty lines)."

You can also interpolate expressions into strings using `${...}` syntax. For example:

    $ dhall
        let name = "John Doe"
    in  let age  = 21
    in  "My name is ${name} and my age is ${Natural/show age}"
    <Ctrl-D>
    Text

    "My name is John Doe and my age is 21"

Note that you can only interpolate expressions of type `Text`

If you need to insert a `"${"` into a string without interpolation then use `"''${"` (same as Nix)

    ''
        for file in *; do
          echo "Found ''${file}"
        done
    ''

# Combine

You can combine two records, using either the `(//)` operator or the `(/\)` operator.

The `(//)` operator (or `(⫽)` U+2AFD) combines the fields of both records, preferring fields from the right record if they share fields in common:

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

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

    { bar = True, foo = 1 }

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

The `(/\)` operator (or `(∧)` U+2227) also lets you combine records, but behaves differently if the records share fields in common. The operator combines shared fields recursively if they are both records:

    $ 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 } }

... but fails with a type error if either shared field 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?

You can analogously combine record types using the `//\\` operator (or `(⩓)` U+2A53):

    $ dhall
    { foo : Natural } ⩓ { bar : Text }
    <Ctrl-D>
    { foo : Natural, bar : Text }

... which behaves the exact same, except at the type level, meaning that the operator descends recursively into record types:

    $ dhall
    { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural }
    <Ctrl-D>
    { foo : { bar : Text, baz : Bool }, qux : Natural }

# 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"

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>
    Error: Invalid input

    (stdin):1:11:
      |
    1 | let twice (x : Text) = x ++ x in twice "ha"
      |           ^
    unexpected '('
    expecting ':', '=', or the rest of label

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://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not
    in  not True
    <Ctrl-D>
    Bool

    False

... or to define synonyms for types:

    $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name'
    List Text

    [ "John", "Mary" ]

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`.

You can also omit the type annotation when merging a union with one or more alternatives, like this:

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

You can also store more than one value or less than one value within alternatives using Dhall's support for anonymous records. You can nest an anonymous record within a union such as in this type:

    < Empty : {} | Person : { name : Text, age : Natural } >

This union of records resembles following equivalent Haskell data type:

    data Example = Empty | Person { name :: Text, age :: Text }

You can resemble Haskell further by defining convenient constructors for each alternative, like this:

        let Empty  = < Empty = {=} | Person : { name : Text, age : Natural } >
    in  let Person =
            λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} >
    in  [   Empty
        ,   Person { name = "John", age = 23 }
        ,   Person { name = "Amy" , age = 25 }
        ,   Empty
        ]

... and Dhall even provides the `constructors` keyword to automate this common pattern:

        let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >
    in  [   MyType.Empty {=}
        ,   MyType.Person { name = "John", age = 23 }
        ,   MyType.Person { name = "Amy" , age = 25 }
        ]

The `constructors` keyword takes a union type argument and returns a record with one field per union type constructor:

    $ dhall
    constructors < Empty : {} | Person : { name : Text, age : Natural } >
    <Ctrl-D>

    { Empty  :
        ∀(Empty : {}) → < Empty : {} | Person : { age : Natural, name : Text } >
    , Person :
          ∀(Person : { age : Natural, name : Text })
        → < Empty : {} | Person : { age : Natural, name : Text } >
    }

    { Empty  =
        λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >
    , Person =
          λ(Person : { age : Natural, name : Text })
        → < Person = Person | Empty : {} >
    }

You can also extract fields during pattern matching such as in the following function which renders each value to `Text`:

        λ(x : < Empty : {} | Person : { name : Text, age : Natural } >)
    →   merge
        {   Empty = λ(_ : {}) → "Unknown"

        ,   Person =
                λ(person : { name : Text, age : Natural })
            →   "Name: ${person.name}, Age: ${Natural/show person.age}"
        }
        x

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

    List < Left : Natural | 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 `Natural`, we create a function that expects an `Natural` argument:

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

    λ(x : Natural) → 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 Natural 4
    <Ctrl-D>
    Natural

    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]
    <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 → Natural

    λ(_ : Text) → 1

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

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 Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map
    in  λ(f : Natural → Natural) → Prelude/List/map Natural Natural f [1, 2, 3]
    <Ctrl-D>
    ∀(f : Natural → Natural) → List Natural

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

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 Natural ([] : List Natural)
    <Ctrl-D>
    Optional Natural

    None Natural

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

https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate

Test what the following Dhall expression normalizes to:

    let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/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)

# Headers

Sometimes you would like to provide additional request headers when importing Dhall expressions from URLs. For example, you might want to provide an authorization header or specify the expected content type.

Dhall URL imports let you add or modify request headers with the `using` keyword:

    https://example.com/example.dhall using ./headers

... where you can replace `./headers` with any import that points to a Dhall expression of the following type:

    List { header : Text, value : Text }

For example, if you needed to specify the content type correctly in order to download the file, then your `./headers` file might look like this:

    $ cat headers
    [ { header = "Accept", value = "application/dhall" } ]

... or if you needed to provide an authorization token to access a private GitHub repository, then your headers could look like this:

    [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN as Text}" } ]

This would read your GitHub API token from the `GITHUB_TOKEN` environment variable and supply that token in the authorization header.

You cannot inline the headers within the same file as the URL. You must provide them as a separate import. That means that this is not legal code:

    http://example.com/example.dhall using [ { header = "Accept", value = "application/dhall" } ]  -- NOT legal

Dhall will forward imports if you import an expression from a URL that contains a relative import. For example, if you import an expression like this:

    http://example.com/example.dhall using ./headers

... and `http://example.com/example.dhall` contains a relative import of `./foo` then Dhall will import `http://example.com/foo` using the same `./headers` file.

# Import integrity

Sometimes you want to use share code while still ensuring that the imported value never changes and can't be corrupted by a malicious attacker. Dhall provides built-in support for hashing imported values to verify that their value never changes

For example, suppose you save the following two files:

    $ cat ./foo
    ./bar sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b

    $ cat ./bar
    ./baz

    $ cat ./baz
    1

The first file named `./foo` contains an example of an integrity check. You can add `sha256:XXX` after any import (such as after `./bar`), where `XXX` is an expected 64-character `sha256` hash of the Dhall value. To be precise, the hash represents a `sha256` hash of the UTF-8 encoding of a canonical text representation of the fully resolved and normalized abstract syntax tree of the imported expression.

Dhall will verify that the expected hash matches the actual hash of the imported Dhall value and reject the import if there is a hash mismatch:

    $ dhall <<< './foo'
    Natural

    1

This implies that the hash only changes if the Dhall value changes. For example, if you add a comment to the `./bar` file:

    $ cat ./bar
    -- This comment does not change the hash
    ./baz

... then `./foo` will still successfully import `./bar` because the hash only depends on the normalized value and does not depend on meaningless changes to whitespace or comments:

    $ dhall <<< './foo'  # This still succeeds
    Natural

    1

You can compute the Hash for any import by using the hash subcommand of this package. For example:

    dhall hash <<< './bar'
    sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b

Then you can paste that output into your code after the import

Now suppose that you you change the value of the `./baz` file:

    $ cat ./baz
    2

... then the `./foo` file will fail to import `./bar`, even though the text of the `./bar` file technically never changed:

    dhall <<< './foo'

    Error: Import integrity check failed

    Expected hash:

    ↳ 6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b

    Actual hash:

    ↳ d4735e3a265e16eee03f59718b9b5d03019c07d8b6c51f90da3a666eec13ab35

This is because the `./bar` file now represents a new value (`2` instead of `1`), even though the text of the `./bar` is still the same. Since the value changed the hash must change as well. However, we could change `./baz` to:

    $ cat baz
    if True then 1 else 2

... and the import would succeed again because the final result is still `1`.

The integrity hash ensures that your import's final meaning can never change, so an attacker can never compromise an imported value protected by a hash unless they can break SHA-256 encryption. The hash not only protects the file that you immediately import, but also protects every transitive import as well.

You can also safely refactor your imported dependencies knowing that the refactor will not change your hash so long as your refactor is behavior-preserving. This provides an easy way to detect refactoring errors that you might accidentally introduce. The hash not only protects you from attackers, but also protects against human error, too!

If you have a file which either doesn't already use hashed imports, or you changed some of the imports and want to update the hashes you can use the freeze command to either add or update hashes:

    cat foo.dhall

'' let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate

in replicate 5 '' > dhall freeze --inplace ./foo.dhall > cat ./foo.dhall '' let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate sha256:b0e3ec1797b32c80c0bcb7e8254b08c7e9e35e75e6b410c7ac21477ab90167ad in replicate 5 ''

# Raw text

Sometimes you want to import the contents of a raw text file as a Dhall value of type `Text`. For example, one of the fields of a record might be the contents of a software license:

    { package = "dhall"
    , author  = "Gabriel Gonzalez"
    , license = ./LICENSE
    }

Normally if you wanted to import a text file you would need to wrap the contents of the file in double single-quotes, like this:

    $ cat LICENSE
    ''
    Copyright (c) 2017 Gabriel Gonzalez
    All rights reserved.

    ...
    (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
    SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
    ''

... which does not work well if you need to reuse the same text file for other programs

However, Dhall supports importing a raw text file by adding `as Text` to the end of the import, like this:

    { package = "dhall"
    , author  = "Gabriel Gonzalez"
    , license = ./LICENSE as Text
    }

... and then you can use the original text file unmodified:

    $ cat LICENSE
    Copyright (c) 2017 Gabriel Gonzalez
    All rights reserved.

    ...
    (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
    SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

# Formatting code

A format subcommand is also available that you can use to automatically format Dhall expressions. For example, we can take the following unformatted Dhall expression:

    $ cat ./unformatted
    λ(a : Type) → λ(kvss : List (List { index : Natural, value : a })) →
    List/build { index : Natural, value : a } (λ(list : Type) → λ(cons : {
    index : Natural, value : a } → list → list) → λ(nil : list) →
    (List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff :
    Natural → list } (λ(kvs : List { index : Natural, value : a }) → λ(y : {
    count : Natural, diff : Natural → list }) → { count = y.count + List/length
    { index : Natural, value : a } kvs, diff = λ(n : Natural) → List/fold {
    index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a
    }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value }
    z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count =
    0, diff = λ(_ : Natural) → nil }).diff 0)

... and run the expression through the the formatter:

    $ dhall format < ./unformatted
      λ(a : Type)
    → λ(kvss : List (List { index : Natural, value : a }))
    → List/build
      { index : Natural, value : a }
      (   λ(list : Type)
        → λ(cons : { index : Natural, value : a } → list → list)
        → λ(nil : list)
        → ( List/fold
            (List { index : Natural, value : a })
            kvss
            { count : Natural, diff : Natural → list }
            (   λ(kvs : List { index : Natural, value : a })
              → λ(y : { count : Natural, diff : Natural → list })
              → { count = y.count + List/length { index : Natural, value : a } kvs
                , diff  =
                      λ(n : Natural)
                    → List/fold
                      { index : Natural, value : a }
                      kvs
                      list
                      (   λ(kvOld : { index : Natural, value : a })
                        → λ(z : list)
                        → cons { index = kvOld.index + n, value = kvOld.value } z
                      )
                      (y.diff (n + List/length { index : Natural, value : a } kvs))
                }
            )
            { count = 0, diff = λ(_ : Natural) → nil }
          ).diff
          0
      )

The executable formats expressions without resolving, type-checking, or normalizing them:

    $ dhall format
    let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate
    in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
    <Ctrl-D>
        let replicate =
              https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate

    in  replicate
        5
        (List (List Natural))
        (replicate 5 (List Natural) (replicate 5 Natural 1))

You can also use the formatter to modify files in place using the `--inplace` flag (i.e. for formatting source code):

    $ dhall format --inplace ./unformatted
    $ cat ./unformatted
      λ(a : Type)
    → λ(kvss : List (List { index : Natural, value : a }))
    → List/build
      { index : Natural, value : a }
      (   λ(list : Type)
        → λ(cons : { index : Natural, value : a } → list → list)
        → λ(nil : list)
        → ( List/fold
            (List { index : Natural, value : a })
            kvss
            { count : Natural, diff : Natural → list }
            (   λ(kvs : List { index : Natural, value : a })
              → λ(y : { count : Natural, diff : Natural → list })
              → { count = y.count + List/length { index : Natural, value : a } kvs
                , diff  =
                      λ(n : Natural)
                    → List/fold
                      { index : Natural, value : a }
                      kvs
                      list
                      (   λ(kvOld : { index : Natural, value : a })
                        → λ(z : list)
                        → cons { index = kvOld.index + n, value = kvOld.value } z
                      )
                      (y.diff (n + List/length { index : Natural, value : a } kvs))
                }
            )
            { count = 0, diff = λ(_ : Natural) → nil }
          ).diff
          0
      )

Carefully note that the code formatter does not preserve all comments. Currently, the formatter only preserves leading comments and whitespace up until the last newline preceding the code. In other words:

    $ dhall format
    {- This comment will be preserved by the formatter -}
    -- ... and this comment will be preserved, too
    {- This comment will *NOT* be preserved -} 1
    -- ... and this comment will also *NOT* be preserved
    <Ctrl-D>
    {- This comment will be preserved by the formatter -}
    -- ... and this comment will be preserved, too
    1

Note that you do not need to format the output of the `dhall` interpreter. The interpreter already automatically formats multi-line expressions, too:

    $ dhall
    let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate
    in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
    <Ctrl-D>
    List (List (List Natural))

      [   [ [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          ]
        : List (List Natural)
      ,   [ [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          ]
        : List (List Natural)
      ,   [ [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          ]
        : List (List Natural)
      ,   [ [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          ]
        : List (List Natural)
      ,   [ [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          , [ 1, 1, 1, 1, 1 ] : List Natural
          ]
        : List (List Natural)
      ]
    : List (List (List Natural))

# 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 `Integer`s (which can be negative). An `Integer` number is a number prefixed with either a `+` or `-` symbol whereas a `Natural` number has no leading sign. If you try to add or multiply two `Integer`s 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 `Integer`s (or `Double`s). 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 `Bool`s. 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>
    Natural

    3

Type:

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

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 non-negative numbers without any leading sign, like this:

    4 : Natural

If you add a `+` or `-` 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 prefixed with a `+` (if they are non-negative) or a `-` sign (if they are negative), like this:

    +3 : Integer
    -2 : Integer

If you omit the sign then they are `Natural` literals and not `Integer`s

There are no built-in operations on `Integer`s. 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 `Double`s. 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 empty `List` must end with a mandatory type annotation, for example:

    [] : List Natural

The built-in operations on `List`s are:

### `(#)`

Example:

    $ dhall
    [1, 2, 3] # [4, 5, 6]
    <Ctrl-D>
    List Natural

    [1, 2, 3, 4, 5, 6]

Type:

    Γ ⊢ x : List a    Γ ⊢ y : List a
    ─────────────────────────────────
    Γ ⊢ x # y : List a

Rules:

    ([] : List a) # xs = xs

    xs # ([] : List a) = xs

    (xs # ys) # zs = xs # (ys # zs)

### `List/fold`

Example:

    $ dhall
    List/fold Bool [True, False, True] 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 Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat

    List/fold a (Prelude/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 Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))
    <Ctrl-D>
    List Natural

    [1, 2, 3] : List Natural

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 Natural [1, 2, 3]
    <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 Natural [1, 2, 3]
    <Ctrl-D>
    Optional Natural

    Some 1

Type:

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

Rules:

    let Prelude/Optional/head  = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Optional/head
    let Prelude/List/concat    = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat
    let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap
    let Prelude/List/map       = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map

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

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

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

### `List/last`

Example:

    $ dhall
    List/last Natural [1, 2, 3]
    <Ctrl-D>
    Optional Natural

    Some 1

Type:

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

Rules:

    let Prelude/Optional/last  = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Optional/last
    let Prelude/List/concat    = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat
    let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap
    let Prelude/List/map       = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map

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

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

    List/last b (Prelude/List/concatMap a b f m)
        = Prelude/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"]
    <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 Prelude/List/shifted = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/shifted
    let Prelude/List/concat  = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat
    let Prelude/List/map     = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map

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

### `List/reverse`

Example:

    $ dhall
    List/reverse Natural [1, 2, 3]
    <Ctrl-D>
    List Natural

    [3, 2, 1] : List Natural

Type:

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

Rules:

    let Prelude/List/map       = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map
    let Prelude/List/concat    = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat
    let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap

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

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

    List/reverse b (Prelude/List/concatMap a b f xs)
        = Prelude/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`

Dhall `Optional` literals are either `Some` followed by a value:

    Γ ⊢ x : t   Γ ⊢ t : Type
    ────────────────────────
    Γ ⊢ Some x : Optional t

... or `None` followed by a type:

    ───────────────────────────────────
    Γ ⊢ None : ∀(t : Type) → Optional t

Note that `None` is a valid standalone function

The built-in operations on `Optional` values are:

### `Optional/fold`

Example:

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

    "ABC"

Type:

    ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
    Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(some : a → optional) → ∀(none : optional) → optional

Rules:

    Optional/fold a (None a) o j n = n

    Optional/fold a (Some x) o j n = j x

# Prelude

There is also a Prelude available at:

http://prelude.dhall-lang.org

... which currenty redirects to:

https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75

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://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not

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

    $ curl https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/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://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not True
    <Ctrl-D>
    Bool

    False

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

    $ dhall
    let Bool/not = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/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 `Prelude/Natural/even`, which re-exports the built-in `Natural/even` function:

    $ curl https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/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 clone the Prelude locally to your filesystem if you prefer using `git clone`, like this:

    $ git clone https://github.com/dhall-lang/Prelude.git
    $ tree Prelude
    Prelude
    ├── Bool
    │   ├── and
    │   ├── build
    │   ├── even
    │   ├── fold
    │   ├── not
    │   ├── odd
    │   ├── or
    │   ├── package.dhall
    │   └── show
    ├── Double
    │   ├── package.dhall
    │   └── show
    ├── Integer
    │   ├── package.dhall
    │   └── show
    ├── List
    │   ├── all
    │   ├── any
    │   ├── build
    │   ├── concat
    │   ├── concatMap
    │   ├── filter
    │   ├── fold
    │   ├── generate
    │   ├── head
    │   ├── indexed
    │   ├── iterate
    │   ├── last
    │   ├── length
    │   ├── map
    │   ├── null
    │   ├── package.dhall
    │   ├── replicate
    │   ├── reverse
    │   ├── shifted
    │   └── unzip
    ├── Monoid
    ├── Natural
    │   ├── build
    │   ├── enumerate
    │   ├── even
    │   ├── fold
    │   ├── isZero
    │   ├── odd
    │   ├── package.dhall
    │   ├── product
    │   ├── show
    │   ├── sum
    │   └── toInteger
    ├── Optional
    │   ├── None
    │   ├── Some
    │   ├── all
    │   ├── any
    │   ├── build
    │   ├── concat
    │   ├── filter
    │   ├── fold
    │   ├── head
    │   ├── last
    │   ├── length
    │   ├── map
    │   ├── null
    │   ├── package.dhall
    │   ├── toList
    │   └── unzip
    ├── Record
    │   ├── keyText
    │   ├── keyValue
    │   └── package.dhall
    ├── Text
    │   ├── concat
    │   ├── concatMap
    │   ├── concatMapSep
    │   ├── concatSep
    │   └── package.dhall
    └── package.dhall

    8 directories, 70 files

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

https://github.com/dhall-lang/Prelude

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

You can also import the entire Prelude as a single large record for convenience:

    $ dhall
        let Prelude = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/package.dhall

    in    λ(x : Text)
        → Prelude.`List`.length Text (Prelude.`List`.replicate 10 Text x)
    <Ctrl-D>
    ∀(x : Text) → Natural

    λ(x : Text) → 10

The organization of the package mirrors the layout of the Prelude, meaning that every directory is stored as a record whose children are the fields of that record.

Exercise: Browse the Prelude by running:

    $ dhall <<< 'https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/package.dhall'

# 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/dhall-lang/dhall-haskell/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.

# Frequently Asked Questions (FAQ)

- Why do empty lists require a type annotation?

Unlike Haskell, Dhall cannot infer a polymorphic type for the empty list because Dhall represents polymorphic values as functions of types, like this:

    λ(a : Type) → [] : List a

If the compiler treated an empty list literal as syntactic short-hand for the above polymorphic function then you'd get the unexpected behavior where a list literal is a function if the list has 0 elements but not a function otherwise.

- Does Dhall support user-defined recursive types?

No, but you can translate recursive code to non-recursive code by following this guide:

How to translate recursive code to Dhall