    {-# OPTIONS_GHC -fno-warn-unused-imports #-}

    {-| Dhall is a programming language specialized for configuration files.  This
        module contains a tutorial explaining how to author configuration files
        using this language
    -}
    module Dhall.Tutorial (
        -- * Introduction
        -- $introduction

        -- * Types
        -- $types

        -- * Imports
        -- $imports

        -- * Lists
        -- $lists

        -- * Optional values
        -- $optional0

        -- * Records
        -- $records

        -- * Functions
        -- $functions

        -- * Compiler
        -- $compiler

        -- * Strings
        -- $strings

        -- * Combine
        -- $combine

        -- * Let expressions
        -- $let

        -- * Defaults
        -- $defaults

        -- * Unions
        -- $unions

        -- * Polymorphic functions
        -- $polymorphic

        -- * Total
        -- $total

        -- * Assertions
        -- $assertions

        -- * Headers
        -- $headers

        -- * Import integrity
        -- $integrity

        -- * Raw text
        -- $rawText

        -- * Formatting code
        -- $format

        -- * Built-in functions
        -- $builtins

        -- ** Caveats
        -- $caveats

        -- ** Extending the language
        -- $extending

        -- ** Substitutions
        -- $substitutions

        -- * Prelude
        -- $prelude

        -- * Conclusion
        -- $conclusion

        -- * Frequently Asked Questions (FAQ)
        -- $faq
        ) where

    import Data.Vector (Vector)
    import Dhall

    -- $setup
    --
    -- >>> :set -XOverloadedStrings

    -- $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:
    --
    -- > -- ./config.dhall
    -- > { 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 FromDhall Example
    -- >
    -- > main :: IO ()
    -- > main = do
    -- >     x <- input auto "./config.dhall"
    -- >     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:
    --
    -- >>> import Dhall
    -- >>> :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 :: FromDhall a => Type a
    -- >
    -- > input auto :: FromDhall 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 `FromDhall` 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 FromDhall 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 FromDhall a => FromDhall (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.dhall@ file that the following program can
    -- decode:
    --
    -- > {-# LANGUAGE DeriveAnyClass    #-}
    -- > {-# LANGUAGE DeriveGeneric     #-}
    -- > {-# LANGUAGE OverloadedStrings #-}
    -- >
    -- > import Dhall
    -- >
    -- > data Person = Person { age :: Natural, name :: Text }
    -- >     deriving (Generic, FromDhall, Show)
    -- >
    -- > main :: IO ()
    -- > main = do
    -- >     x <- input auto "./config.dhall"
    -- >     print (x :: Person)
    --
    -- __Exercise:__ Create a @./config.dhall@ file that the following program can
    -- decode:
    --
    -- > {-# LANGUAGE OverloadedStrings #-}
    -- >
    -- > import Data.Functor.Identity
    -- > import Dhall
    -- >
    -- > instance FromDhall a => FromDhall (Identity a)
    -- >
    -- > main :: IO ()
    -- > main = do
    -- >     x <- input auto "./config.dhall"
    -- >     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│ 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:
    --
    -- > -- ./config.dhall
    -- > { foo = 1
    -- > , bar = ./bar.dhall
    -- > }
    --
    -- > -- ./bar.dhall
    -- > [3.0, 4.0, 5.0]
    --
    -- ... which is equivalent to our original configuration:
    --
    -- > -- ./config.dhall
    -- > { 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,
    -- such 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:
    --
    -- > -- ./bar.dhall
    -- > [3.0, 4.0, 5.0] : List ./type.dhall
    --
    -- ... then specify the type in a separate file:
    --
    -- > -- ./type.dhall
    -- > Double
    --
    -- ... and everything still type checks:
    --
    -- > $ ./example
    -- > Example {foo = 1, bar = [3.0,4.0,5.0]}
    --
    -- Note that imports should be terminated by whitespace or parentheses otherwise
    -- 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://prelude.dhall-lang.org/Bool/not>
    --
    -- Visit that link and read the documentation.  Then try to guess what this
    -- code returns:
    --
    -- > >>> input auto "https://prelude.dhall-lang.org/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
    -- ...
    -- 1│ []
    -- ...
    -- (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
    -- ...
    -- 1│     True
    -- ...
    -- (input):1:5
    -- ...
    --
    -- __Exercise:__ Replace the @\"???\"@ with an expression that successfully
    -- decodes to the specified type:
    --
    -- > >>> input auto "???" :: IO (Vector (Vector Natural))

    -- $optional0
    --
    -- @Optional@ values are either of the form @Some value@ or @None type@.
    --
    -- 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:__ Replace the @\"???\"@ with an expression that successfully
    -- decodes to the specified type:
    --
    -- > >>> input auto "???" :: 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 type <<< '{=}'
    -- > {}
    --
    -- > $ dhall type <<< '{}'
    -- > Type
    --
    -- This is our first use of the @dhall@ command-line tool (provided by this
    -- package), which provides a @type@ subcommand for inferring an expression's
    -- type.  By default the tool reads the expression on standard input and outputs
    -- the type to standard output.
    --
    -- Note that @<<<@ is a feature specific to the Bash shell to feed a string to
    -- a command's standard input.  If you are using another shell, then you can
    -- instead do this:
    --
    -- > $ echo '{=}' | dhall type
    -- > {}
    --
    -- __Exercise__: Use the @dhall type@ command to infer the type of this record:
    --
    -- > -- ./nested.dhall
    -- > { foo = 1
    -- > , bar =
    -- >     { baz = 2.0
    -- >     , qux = True
    -- >     }
    -- > }
    --
    -- You can specify nested fields using dot-separated keys, like this:
    --
    -- > { foo = 1, bar.baz = 2.0, bar.qux = True }
    --
    -- ... which is equivalent to:
    --
    -- > { foo = 1, bar = { baz = 2.0, qux = True } }
    --
    -- You can also 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 }'
    -- > { x = 1, y = True }
    --
    -- This is our first example of using the @dhall@ command-line tool with no
    -- subcommand (like @type@), which evaluates the provided expression.  By
    -- default, this reads the expression on standard input and outputs the
    -- evaluated result on standard output.
    --
    -- __Exercise__: Save the above @./nested.dhall@ file and then try to access the
    -- value of the @baz@ field.  Test that this works by interpreting your code
    -- using the @dhall@ command.
    --
    -- You can convert a record to a list of key-value pairs (a.k.a. a \"Map\") by
    -- using the `toMap` keyword.  For example:
    --
    -- > $ dhall <<< 'toMap { foo = 1, bar = 2 }'
    -- > [ { mapKey = "bar", mapValue = 2 }, { mapKey = "foo", mapValue = 1 } ]
    --
    -- This conversion only works if all field of the record have the same type.
    -- This comes in handy when you need to convert a Dhall record to the Dhall
    -- equivalent of a homogeneous map (i.e. Haskell's @"Data.Map"@).

    -- $functions
    --
    -- The Dhall programming language also supports user-defined anonymous
    -- functions.  For example, we can save the following anonymous function to a
    -- file:
    --
    -- > -- ./makeBools.dhall
    -- > \(n : Bool) ->
    -- >     [ n && True, n && False, n || True, n || False ]
    --
    -- ... 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):
    --
    -- > $ -- ./makeBools.dhall
    -- > λ(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.dhall" :: IO (Bool -> Vector Bool)
    -- >>> makeBools True
    -- [True,False,True,True]
    --
    -- The reason this works is that there is an `FromDhall` instance for simple
    -- functions:
    --
    -- > instance (ToDhall a, FromDhall b) => FromDhall (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 `FromDhall`, you can derive `ToDhall` 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, ToDhall)
    -- >
    -- > 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 --annotate <<< './makeBools.dhall'
    -- > (λ(n : Bool) → [ n, False, True, n ]) : ∀(n : Bool) → List Bool
    --
    -- The @--annotate@ flag adds a type signature to the output to let us know
    -- what type the interpreter inferred for our expression.  The type signature
    -- is @∀(n : Bool) → List Bool@ which 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@).
    --
    -- This expression 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.dhall True'
    -- > [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'
    -- > [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.dhall 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@ command to infer the type of the function you
    -- just created and verify that your function has the correct type
    --
    -- __Exercise__: Use the @dhall@ command to apply your function to a sample
    -- record

    -- $strings
    -- Dhall supports ordinary string literals with Haskell-style escaping rules:
    --
    -- > $ dhall
    -- > "Hello, \"world\"!"
    -- > <Ctrl-D>
    -- > "Hello, \"world\"!"
    --
    -- ... and Dhall also supports Nix-style multi-line string literals:
    --
    -- > $ dhall
    -- > ''
    -- >     #!/bin/bash
    -- >
    -- >     echo "Hi!"
    -- > ''
    -- > <Ctrl-D>
    -- > "\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"
    -- > let age  = 21
    -- > in  "My name is ${name} and my age is ${Natural/show age}"
    -- > <Ctrl-D>
    -- > "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 = "ABC", baz = True, foo = 1 }
    -- > $ dhall
    -- > { foo = 1, bar = "ABC" } ⫽ { bar = True }  -- Fancy unicode
    -- > <Ctrl-D>
    -- > { bar = True, foo = 1 }
    --
    -- Note that the order of record fields does not matter.  The compiler
    -- automatically sorts the fields.
    --
    -- If you need to set or add a deeply nested field you can use the @with@
    -- keyword, like this:
    --
    -- > $ dhall <<< '{ x.y = 1 } with x.z = True'
    -- > { x = { y = 1, z = True } }
    --
    -- > $ dhall <<< '{ x.y = 1 } with x.y = 2'
    -- > { x.y = 2 }
    --
    -- The @with@ keyword is syntactic sugar for the @//@ operator which follows
    -- these rules:
    --
    -- > -- Nested case
    -- > record with k.ks… = value  ⇒  record // { k = record.k with ks… = value }
    -- >
    -- > -- Base case
    -- > record with k = value      ⇒  record // { k = value }
    --
    -- 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 = "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 }
    -- >
    -- > (input):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
    --
    -- 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>
    -- > "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>
    -- > "haha"
    --
    -- You need to nest @let@ expressions if you want to define more than one value
    -- in this way:
    --
    -- > $ dhall
    -- > let x = "Hello, "
    -- > let y = "world!"
    -- > in  x ++ y
    -- > <Ctrl-D>
    -- > "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>
    -- > "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
    -- >
    -- > (input):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://prelude.dhall-lang.org/Bool/not
    -- > in  not True
    -- > <Ctrl-D>
    -- > 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
    -- > 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"
    -- > let x = x ++ "ha"
    -- > in  x
    --
    -- __Exercise:__ What about this code?
    --
    -- > let x = x ++ "ha"
    -- > in  x

    -- $defaults
    --
    -- For records with a large number of defaultable fields you can use the
    -- @::@ operator to auto-complete a record.  For example:
    --
    -- > let greet =
    -- >           \(args : { greeting : Text, name : Text })
    -- >       ->  "${args.greeting}, ${args.name}!"
    -- >
    -- > let Greeting =
    -- >       { Type = { greeting : Text, name : Text }
    -- >       , default = { greeting = "Hello", name = "John" }
    -- >       }
    -- >
    -- > in  ''
    -- >     ${greet Greeting::{=}}
    -- >     ${greet Greeting::{ greeting = "Hola" }}
    -- >     ${greet Greeting::{ name = "Jane" }}
    -- >     ${greet Greeting::{ greeting = "Hola", name = "Jane" }}
    -- >     ''
    --
    -- This operator is syntactic sugar.  Specifically an expression of the form:
    --
    -- > T::r
    --
    -- ... is equivalent to:
    --
    -- > (T.default // r) : T.Type
    --
    -- So, for example:
    --
    -- > Greeting::{ greeting = "Hola" }
    --
    -- ... is the same thing as:
    --
    -- > (Greeting.default // { greeting = "Hola" }) : Greeting.Type
    --
    -- ... which is the same thing as:
    --
    -- > ({ greeting = "Hello", name = "John" } // { greeting = "Hola" }) : { greeting : Text, name : Text }
    --
    -- ... which is the same thing as:
    --
    -- > { greeting = "Hola", name = "John" }

    -- $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\" and the above type is equivalent to @Either Natural Bool@.
    --
    -- 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.
    --
    -- You can specify the value of a union constructor like this:
    --
    -- > let Union = < Left : Natural | Right : Bool>
    -- >
    -- > in  [ Union.Left 0, Union.Right True ]
    --
    -- In other words, you can access a union constructor as a field of a union
    -- type and use that constructor to wrap a value of a type appropriate for
    -- that alternative.  In the above example, the @Left@ constructor can wrap
    -- a @Natural@ value and the @Right@ constructor can wrap a @Bool@ value.  We
    -- can also confirm that by inspecting their type:
    --
    -- > $ echo '< Left : Natural | Right : Bool>' > ./Union
    --
    -- > $ dhall --annotate <<< '(./Union).Left'
    -- >   < Left : Natural | Right : Bool >.Left
    -- > : ∀(Left : Natural) → < Left : Natural | Right : Bool >
    --
    -- > $ dhall --annotate <<< '(./Union).Right'
    -- >   < Left : Natural | Right : Bool >.Right
    -- > : ∀(Right : Bool) → < Left : Natural | Right : Bool >
    --
    -- In other words, the @Left@ constructor is a function from a @Natural@ to a
    -- value of our @Union@ type and the @Right@ constructor is a separate function
    -- from a @Bool@ to that same @Union@ type.
    --
    -- 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@ constructor or a @Bool@ wrapped in the @Right@ constructor .  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
    -- > EOF
    --
    -- Now our @./process@ function can handle both alternatives:
    --
    -- > $ dhall <<< './process ((./Union).Left 3)'
    -- > False
    --
    -- > $ dhall <<< './process ((./Union).Right True)'
    -- > 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 an optional 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) = f x
    --
    -- So, for example:
    --
    -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Left 3)
    -- >     = Natural/even 3
    -- >     = False
    --
    -- ... and similarly:
    --
    -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Right True)
    -- >     = (λ(b : Bool) → b) True
    -- >     = True
    --
    -- Notice that each handler has to return the same type of result (@Bool@ in
    -- this case).
    --
    -- You can also store more 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 } >
    --
    -- You can even go a step further and omit the type of an alternative if it
    -- stores no data, like this:
    --
    -- > < Empty | Person : { name : Text, age : Natural } >
    --
    -- The above Dhall type resembles the following equivalent Haskell data type:
    --
    -- > data Example = Empty | Person { name :: Text, age :: Text }
    --
    -- Empty alternatives like @Empty@ require no argument:
    --
    -- > let Example = < Empty | Person : { name : Text, age : Natural } >
    -- >
    -- > in  [ Example.Empty  -- Note the absence of any argument to `Empty`
    -- >     , Example.Person { name = "John", age = 23 }
    -- >     , Example.Person { name = "Amy" , age = 25 }
    -- >     ]
    --
    -- ... and when you @merge@ an empty alternative the correspond handler takes no
    -- argument:
    --
    -- >     λ(x : < Empty | Person : { name : Text, age : Natural } >)
    -- > →   merge
    -- >     {   Empty = "Unknown"  -- Note the absence of a `λ`
    -- >
    -- >     ,   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
    --
    -- 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
    --
    -- Let's ask the interpreter for the type of this function:
    -- the first line:
    --
    -- > $ dhall type <<< './id'
    -- > ∀(a : Type) → ∀(x : a) → a
    --
    -- 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 type <<< './id Natural'
    -- > ∀(x : Natural) → Natural
    --
    -- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a
    -- @Bool@ argument:
    --
    -- > $ dhall type <<< './id Bool'
    -- > ∀(x : Bool) → Bool
    --
    -- 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'
    -- > 4
    --
    -- > $ dhall <<< './id Bool True'
    -- > 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 --annotate
    -- > List/reverse
    -- > <Ctrl-D>
    -- > List/reverse : ∀(a : Type) → List a → List a
    --
    -- The first argument to @List/reverse@ is the type of the list to reverse:
    --
    -- > $ dhall
    -- > List/reverse Bool
    -- > <Ctrl-D>
    -- > List/reverse Bool : List Bool → List Bool
    --
    -- ... and the second argument is the list to reverse:
    --
    -- > $ dhall
    -- > List/reverse Bool [True, False]
    -- > <Ctrl-D>
    -- > [False, True]
    --
    -- 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 type <<< 'λ(_ : Text) → 1'
    -- > Text → Natural
    --
    -- 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) → 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://prelude.dhall-lang.org/List/map
    -- > in  λ(f : Natural → Natural) → List/map Natural Natural f [1, 2, 3]
    -- > <Ctrl-D>
    -- > λ(f : Natural → Natural) → [f 1, f 2, f 3]
    --
    -- 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)'
    -- > None Natural
    --
    -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can
    -- find here:
    --
    -- <https://prelude.dhall-lang.org/List/replicate>
    --
    -- Test what the following Dhall expression normalizes to:
    --
    -- > let replicate = https://prelude.dhall-lang.org/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).

    -- $assertions
    --
    -- You can add compile-time assertions which you can use to add tests to your
    -- code.  For example, we can add some tests to our @not@ function like this:
    --
    -- > let not
    -- >     : Bool → Bool
    -- >     = λ(b : Bool) → b == False
    -- >
    -- > let example0 = assert : not False === True
    -- >
    -- > let example1 = assert : not True === False
    -- >
    -- > in  not
    --
    -- The expression @assert : not False == True@ is a type-checking assertion
    -- that two expressions have the same normal form.  If the two expressions differ
    -- then type-checking rejects the code.
    --
    -- For example, suppose that we change the example to add an incorrect assertion:
    --
    -- > -- ./test.dhall
    -- >
    -- > let not
    -- >     : Bool → Bool
    -- >     = λ(b : Bool) → b == False
    -- >
    -- > let example0 = assert : not False === True
    -- >
    -- > let example1 = assert : not True === True  -- Oops!
    -- >
    -- > in  not
    --
    -- The type-checker then rejects the assertion with the following error message:
    --
    -- > $ dhall <<< './test.dhall'
    -- >
    -- > ↳ ./test.dhall
    -- >
    -- > Error: Assertion failed
    -- >
    -- > - False
    -- > + True
    -- >
    -- > 7│                assert : not True === True -- Oops!
    -- > 8│
    -- >
    -- > ./test.dhall:7:16
    -- >
    -- > 1│ ./test.dhall
    -- >
    -- > (input):1:1
    --
    -- You can compare expressions that contain variables, too, which is equivalent
    -- to symbolic reasoning:
    --
    -- > $ dhall <<< '\(n : Natural) -> assert : n === (n + 0)'
    -- > λ(n : Natural) → assert : n ≡ n
    --
    -- Dhall accepts this because the language has built-in support for normalizing
    -- @n + 0@ to @n@, so both sides of the comparison normalize to the same value:
    -- @n@.
    --
    -- Note that this sort of symbolic reasoning is limited and can only detect
    -- equality of normal forms.  Some equivalent expressions will be rejected
    -- if they don't share the same normal form, such as these:
    --
    -- > $ dhall <<< '\(n : Natural) -> assert : Natural/even (n + n) === True'
    -- >
    -- > Use "dhall --explain" for detailed errors
    -- >
    -- > n : Natural
    -- >
    -- > Error: Assertion failed
    -- >
    -- > - … …
    -- > + True
    -- >
    -- > 1│                   assert : Natural/even (n + n) === True
    -- >
    -- > (input):1:19
    --
    -- Here the interpreter is not smart enough to simplify @Natural/even (n + n)@
    -- to @True@ so the assertion fails.
    --
    -- If you prefer to use Unicode, then the Unicode equivalent of @===@ is @≡@
    -- (U+2261).

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

    -- $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:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
    --
    -- > $ 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
    --
    -- Any import protected by a semantic integrity check is automatically cached
    -- locally underneath either @~\/.cache\/dhall\/1220${HASH}@ or
    -- @${XDG_CACHE_HOME}\/dhall/1220${HASH}@ if you define the @XDG_CACHE_HOME@
    -- environment variable.
    --
    -- For example, after you import @./foo@ the contents of `./bar` are locally
    -- cached in a fully-evaluated and binary-encoded form which you can inspect by
    -- running:
    --
    -- > $ dhall decode < ~/.cache/dhall/1220d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
    -- > 1
    --
    -- Subsequent attempts to resolve the same import will automatically retrieve
    -- the import from the cache.  This matters less for local imports, but comes in
    -- handy for remote imports to avoid redownloading them.
    --
    -- The local cache takes precedence when resolving imports, so changing the
    -- original import afterwards will have no affect until you update the hash.
    -- From Dhall's point of view, the hash is the true address and the file path
    -- is just a suggestion for how to obtain the import if it's not already cached.
    --
    -- You can disable the cache by setting `XDG_CACHE_HOME` to `/var/empty` (an
    -- empty and unwritable directory), like this:
    --
    -- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo'
    -- > Natural
    -- >
    -- > 1
    --
    -- We'll use this trick to test changes to the protected import in the following
    -- examples.
    --
    -- Now, suppose 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:
    --
    -- > $ XDG_CACHE_HOME=/var/empty 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:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
    --
    -- Now suppose that you actually 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:
    --
    -- > XDG_CACHE_HOME=/var/empty dhall <<< './foo'
    -- >
    -- > Error: Import integrity check failed
    -- >
    -- > Expected hash:
    -- >
    -- > ↳ d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
    -- >
    -- > Actual hash:
    -- >
    -- > ↳ 4caf97e8c445d4d4b5c5b992973e098ed4ae88a355915f5a59db640a589bc9cb
    --
    -- This is because the @./bar@ file now represents a new value (@2@ instead of
    -- @1@), even though the text of the @./bar@ file 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 now succeed again because the final result is @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://prelude.dhall-lang.org/List/replicate
    -- > in  replicate 5
    -- > $
    -- > $ dhall freeze --inplace ./foo.dhall
    -- > $ cat ./foo.dhall
    -- > let replicate =
    -- >       https://prelude.dhall-lang.org/List/replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347
    -- >
    -- > in  replicate 5

    -- $rawText
    --
    -- 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.

    -- $format
    --
    -- 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 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://prelude.dhall-lang.org/List/replicate
    -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
    -- > <Ctrl-D>
    -- > let replicate = https://prelude.dhall-lang.org/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
    --
    -- Carefully note that the code formatter does not preserve all comments.
    -- Currently, the formatter only preserves two types of comments:
    --
    -- * Leading comments at the beginning of the file
    -- * Comments within a @let@ binding
    --
    -- For example:
    --
    -- > $ 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
    --
    -- Also:
    --
    -- > let {- This comment will be preserved -}
    -- >     x {- This comment will also be preserved-} =
    -- >     {- ... and this one will be preserved, too -}
    -- >       1
    -- >
    -- > in  x
    --
    -- 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://prelude.dhall-lang.org/List/replicate
    -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
    -- > <Ctrl-D>
    -- > [ [ [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   ]
    -- > , [ [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   ]
    -- > , [ [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   ]
    -- > , [ [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   ]
    -- > , [ [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   , [ 1, 1, 1, 1, 1 ]
    -- >   ]
    -- > ]

    -- $builtins
    --
    -- 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 language provides built-in support for the following primitive types:
    --
    -- * @Bool@ values
    -- * @Natural@ values
    -- * @Integer@ values
    -- * @Double@ values
    -- * @Text@ values
    --
    -- ... as well as support for the following derived types:
    --
    -- * @List@s of values
    -- * @Optional@ values
    -- * Anonymous records
    -- * Anonymous unions
    --
    -- You can find an up-to-date list of available built-in functions and operators
    -- here:
    --
    -- <https://github.com/dhall-lang/dhall-lang/wiki/Built-in-types%2C-functions%2C-and-operators Built-in types, functions, and operators>

    -- $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
    -- >
    -- > (input):1:1
    --
    -- In fact, there are no built-in functions for @Integer@s (or @Double@s) other
    -- than @Integer/show@ and @Double/show@.  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.
    --
    -- However, you can extend the language with your own built-ins using the
    -- Haskell API, as described in the next section.

    -- $extending
    --
    -- You can use the Haskell API to extend the Dhall configuration language with
    -- new built-in functions.  This section contains a simple Haskell recipe to add
    -- a new @Natural/equal@ built-in function of type:
    --
    -- > Natural/equal : Natural → Natural → Bool
    --
    -- To do so, we:
    --
    -- * extend the type-checking context to include the type of @Natural/equal@
    -- * extend the normalizer to evaluate all occurrences of @Natural/equal@
    --
    -- ... like this:
    --
    -- > -- example.hs
    -- >
    -- > {-# LANGUAGE OverloadedStrings #-}
    -- >
    -- > module Main where
    -- >
    -- > import Dhall.Core (Expr(..), ReifiedNormalizer(..))
    -- >
    -- > import qualified Data.Text.IO
    -- > import qualified Dhall
    -- > import qualified Dhall.Context
    -- > import qualified Lens.Family   as Lens
    -- >
    -- > main :: IO ()
    -- > main = do
    -- >     text <- Data.Text.IO.getContents
    -- >
    -- >     let startingContext = transform Dhall.Context.empty
    -- >           where
    -- >             transform = Dhall.Context.insert "Natural/equal" naturalEqualType
    -- >
    -- >             naturalEqualType =
    -- >                 Pi "_" Natural (Pi "_" Natural Bool)
    -- >
    -- >     let normalizer (App (App (Var "Natural/equal") (NaturalLit x)) (NaturalLit y)) =
    -- >             Just (BoolLit (x == y))
    -- >         normalizer _ =
    -- >             Nothing
    -- >
    -- >     let inputSettings = transform Dhall.defaultInputSettings
    -- >           where
    -- >             transform =
    -- >                   Lens.set Dhall.normalizer      (Just (ReifiedNormalizer (pure . normalizer)))
    -- >                 . Lens.set Dhall.startingContext startingContext
    -- >
    -- >     x <- Dhall.inputWithSettings inputSettings Dhall.auto text
    -- >
    -- >     Data.Text.IO.putStrLn x
    --
    -- Here is an example use of the above program:
    --
    -- > $ ./example <<< 'if Natural/equal 2 (1 + 1) then "Equal" else "Not equal"'
    -- > Equal
    --
    -- Note that existing Dhall tools that type-check expressions will reject
    -- expressions containing unexpected free variable such as @Natural/equal@:
    --
    -- > $ dhall <<< 'Natural/equal 2 (1 + 1)'
    -- >
    -- > Use "dhall --explain" for detailed errors
    -- >
    -- > Error: Unbound variable
    -- >
    -- > Natural/equal
    -- >
    -- > (input):1:1
    --
    -- You will need to either:
    --
    -- * create your own parallel versions of these tools, or:
    -- * < https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-i-change-the-language try to upstream your built-ins into the language>
    --
    -- The general guidelines for adding new built-ins to the language are:
    --
    -- * Keep built-ins easy to implement across language bindings
    -- * Prefer general purpose built-ins or built-ins appropriate for the task of program configuration
    -- * Design built-ins to catch errors as early as possible (i.e. when type-checking the configuration)

    -- $substitutions
    --
    -- Substitutions are another way to extend the language.
    -- Suppose we have the following Haskell datatype:
    --
    -- > data Result = Failure Integer | Success String
    -- >     deriving (Eq, Generic, Show)
    -- >
    -- > instance FromDhall Result
    --
    -- We can use it in Dhall like that:
    --
    -- > -- example.dhall
    -- >
    -- > let Result = < Failure : Integer | Success Text >
    -- > in Result.Failure 1
    --
    -- Right now it is quite easy to keep these two definitions (the one in Haskell source and the one in the Dhall file) synchronized:
    -- If we implement a new feature in the Haskell source we update the corresponding type in the Dhall file.
    -- But what happens if our application is growing and our Result type contains e.g. 10 unions with possible types embedded in it?
    -- Maintaining the code will get tedious. Luckily we can extract the correct Dhall type from the Haskell definition:
    --
    -- > resultDecoder :: Dhall.Decoder Result
    -- > resultDecoder = Dhall.auto
    -- >
    -- > resultType :: Expr Src Void
    -- > resultType = Dhall.expected resultDecoder
    -- >
    -- > resultTypeString :: String
    -- > resultTypeString = show $ pretty resultType
    --
    -- Now we just have to inject that type into the Dhall code and we are done. One common way to do that is to wrap the import of example.dhall in a let expression:
    --
    -- > Dhall.input (Dhall.auto :: Dhall.Decoder Result) ("let Result = " ++ Data.Text.pack resultTypeString ++ " in ./example.dhall")
    --
    -- Now we can omit the definition of Result in our example.dhall file. While this will work perfectly Dhall provides a cleaner solution for our \"injection problem\":
    --
    -- > {-# LANGUAGE OverloadedStrings #-}
    -- >
    -- > myexample :: IO Result
    -- > myexample = let
    -- >    evaluateSettings = Lens.over Dhall.substitutions (Dhall.Map.insert "Result" resultType) Dhall.defaultEvaluateSettings
    -- >    in Dhall.inputFileWithSettings evaluateSettings resultDecoder "example.dhall"
    --
    -- Substitutions are a simple 'Dhall.Map.Map' mapping variables to expressions. The application of these substitutions reflect the order of the insertions in the substitution map:
    --
    -- > {-# LANGUAGE OverloadedStrings #-}
    -- >
    -- > substitute (Dhall.Core.Var "Foo") (Dhall.Map.fromList [("Foo", Dhall.Core.Var "Bar"), ("Bar", Dhall.Core.BoolLit True)])
    --
    -- results in @Dhall.Core.Var \"Baz\"@ since we first substitute \"Foo\" with \"Bar\" and then the resulting \"Bar\" with the final @True@.
    --
    -- Notable differences to the other extensions of the builtin language:
    --
    --  * This approach works well with the inputFile/inputFileWithSettings functions while the let-wrapping will not.
    --
    --  * In contrast to the custom built-ins described above substitutions are made BEFORE the type-checking.

    -- $prelude
    --
    -- There is also a Prelude available at:
    --
    -- <https://prelude.dhall-lang.org>
    --
    -- 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, which
    -- you can reference using this URL:
    --
    -- <https://prelude.dhall-lang.org/Bool/not>
    --
    -- The @not@ function is just a UTF8-encoded text file hosted online with the
    -- following contents
    --
    -- > $ $ dhall <<< 'https://prelude.dhall-lang.org/Bool/not as Text'
    -- > ''
    -- > {-
    -- > Flip the value of a `Bool`
    -- > -}
    -- > let not : Bool → Bool = λ(b : Bool) → b == False
    -- >
    -- > let example0 = assert : not True ≡ False
    -- >
    -- > let example1 = assert : not False ≡ True
    -- >
    -- > 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
    -- * tests
    --
    -- The performance penalty for adding these helpful features is negligible,
    -- especially if you protect the import with a semantic integrity check because
    -- then the import would be cached compactly as @λ(_ : Bool) → _ == False@.
    --
    -- You can use this @not@ function either directly:
    --
    -- > $ dhall
    -- > https://prelude.dhall-lang.org/Bool/not True
    -- > <Ctrl-D>
    -- > False
    --
    -- ... or assign the URL to a shorter name:
    --
    -- > $ dhall
    -- > let Bool/not = https://prelude.dhall-lang.org/Bool/not
    -- > in  Bool/not True
    -- > <Ctrl-D>
    -- > 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:
    --
    -- > $ dhall <<< 'https://prelude.dhall-lang.org/Natural/even as Text'
    -- > ''
    -- > {-
    -- > Returns `True` if a number if even and returns `False` otherwise
    -- > -}
    -- > let even : Natural → Bool = Natural/even
    -- >
    -- > let example0 = assert : even 3 ≡ False
    -- >
    -- > let example1 = assert : even 0 ≡ True
    -- >
    -- > 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/dhall-lang.git
    -- > $ tree dhall-lang/Prelude
    -- > dhall-lang/Prelude
    -- > ├── Bool
    -- > │   ├── and
    -- > │   ├── build
    -- > │   ├── even
    -- > │   ├── fold
    -- > │   ├── not
    -- > │   ├── odd
    -- > │   ├── or
    -- > │   ├── package.dhall
    -- > │   └── show
    -- > ├── Double
    -- > │   ├── package.dhall
    -- > │   └── show
    -- > ├── Function
    -- > │   ├── compose
    -- > │   └── package.dhall
    -- > ├── Integer
    -- > │   ├── package.dhall
    -- > │   ├── show
    -- > │   └── toDouble
    -- > ├── JSON
    -- > │   ├── Nesting
    -- > │   ├── Tagged
    -- > │   ├── Type
    -- > │   ├── array
    -- > │   ├── bool
    -- > │   ├── keyText
    -- > │   ├── keyValue
    -- > │   ├── null
    -- > │   ├── number
    -- > │   ├── object
    -- > │   ├── package.dhall
    -- > │   ├── render
    -- > │   └── string
    -- > ├── List
    -- > │   ├── all
    -- > │   ├── any
    -- > │   ├── build
    -- > │   ├── concat
    -- > │   ├── concatMap
    -- > │   ├── default
    -- > │   ├── empty
    -- > │   ├── filter
    -- > │   ├── fold
    -- > │   ├── generate
    -- > │   ├── head
    -- > │   ├── indexed
    -- > │   ├── iterate
    -- > │   ├── last
    -- > │   ├── length
    -- > │   ├── map
    -- > │   ├── null
    -- > │   ├── package.dhall
    -- > │   ├── replicate
    -- > │   ├── reverse
    -- > │   ├── shifted
    -- > │   └── unzip
    -- > ├── Location
    -- > │   ├── Type
    -- > │   └── package.dhall
    -- > ├── Map
    -- > │   ├── Entry
    -- > │   ├── Type
    -- > │   ├── empty
    -- > │   ├── keyText
    -- > │   ├── keyValue
    -- > │   ├── keys
    -- > │   ├── map
    -- > │   ├── package.dhall
    -- > │   └── values
    -- > ├── Monoid
    -- > ├── Natural
    -- > │   ├── build
    -- > │   ├── enumerate
    -- > │   ├── equal
    -- > │   ├── even
    -- > │   ├── fold
    -- > │   ├── greaterThan
    -- > │   ├── greaterThanEqual
    -- > │   ├── isZero
    -- > │   ├── lessThan
    -- > │   ├── lessThanEqual
    -- > │   ├── odd
    -- > │   ├── package.dhall
    -- > │   ├── product
    -- > │   ├── show
    -- > │   ├── subtract
    -- > │   ├── sum
    -- > │   ├── toDouble
    -- > │   └── toInteger
    -- > ├── Optional
    -- > │   ├── all
    -- > │   ├── any
    -- > │   ├── build
    -- > │   ├── concat
    -- > │   ├── default
    -- > │   ├── filter
    -- > │   ├── fold
    -- > │   ├── head
    -- > │   ├── last
    -- > │   ├── length
    -- > │   ├── map
    -- > │   ├── null
    -- > │   ├── package.dhall
    -- > │   ├── toList
    -- > │   └── unzip
    -- > ├── Text
    -- > │   ├── concat
    -- > │   ├── concatMap
    -- > │   ├── concatMapSep
    -- > │   ├── concatSep
    -- > │   ├── default
    -- > │   ├── defaultMap
    -- > │   ├── package.dhall
    -- > │   └── show
    -- > ├── XML
    -- > │   ├── Type
    -- > │   ├── attribute
    -- > │   ├── element
    -- > │   ├── emptyAttributes
    -- > │   ├── leaf
    -- > │   ├── package.dhall
    -- > │   ├── render
    -- > │   └── text
    -- > └── package.dhall
    --
    -- Browse the Prelude online to learn more by seeing what functions are
    -- available and reading their inline documentation:
    --
    -- <https://prelude.dhall-lang.org>
    --
    -- __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://prelude.dhall-lang.org/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://prelude.dhall-lang.org/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 languages that do not yet have Dhall integrations so that Dhall configuration files
    -- can be read into those languages, too.

    -- $faq
    --
    -- <https://github.com/dhall-lang/dhall-lang/wiki/Frequently-Asked-Questions-(FAQ) Frequently Asked Questions (FAQ)>