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

    {-| Dhall is a programming language specialized for configuration files.  This
        module contains a tutorial explaning 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

        -- * Unions
        -- $unions

        -- * Polymorphic functions
        -- $polymorphic

        -- * Total
        -- $total

        -- * Headers
        -- $headers

        -- * Import integrity
        -- $integrity

        -- * Raw text
        -- $rawText

        -- * Formatting code
        -- $format

        -- * Built-in functions
        -- $builtins

        -- ** Caveats
        -- $caveats

        -- ** Overview
        -- $builtinOverview

        -- ** @Bool@
        -- $bool

        -- *** @(||)@
        -- $or

        -- *** @(&&)@
        -- $and

        -- *** @(==)@
        -- $equal

        -- *** @(!=)@
        -- $unequal

        -- *** @if@\/@then@\/@else@
        -- $ifthenelse

        -- ** @Natural@
        -- $natural

        -- *** @(+)@
        -- $plus

        -- *** @(*)@
        -- $times

        -- *** @Natural/even@
        -- $even

        -- *** @Natural/odd@
        -- $odd

        -- *** @Natural/isZero@
        -- $isZero

        -- *** @Natural/fold@
        -- $naturalFold

        -- *** @Natural/build@
        -- $naturalBuild

        -- ** @Integer@
        -- $integer

        -- ** @Double@
        -- $double

        -- ** @Text@
        -- $text

        -- *** @(++)@
        -- $textAppend

        -- ** @List@
        -- $list

        -- *** @(#)@
        -- $listAppend

        -- *** @List/fold@
        -- $listFold

        -- *** @List/build@
        -- $listBuild

        -- *** @List/length@
        -- $listLength

        -- *** @List/head@
        -- $listHead

        -- *** @List/last@
        -- $listLast

        -- *** @List/indexed@
        -- $listIndexed

        -- *** @List/reverse@
        -- $listReverse

        -- ** @Optional@
        -- $optional1

        -- *** @Optional/fold@
        -- $optionalFold

        -- * 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:
    --
    -- > $ 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))

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

    -- $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
    -- ''
    --
    -- $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 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))

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

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

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

    -- $builtinOverview
    --
    -- 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:
    --

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

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

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

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

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

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

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

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

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

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

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

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

    -- $textAppend
    --
    -- 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:

    -- $listAppend
    --
    -- 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)

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

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

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

    -- $listHead
    --
    -- 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)

    -- $listLast
    --
    -- 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)

    -- $listIndexed
    --
    -- 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)

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

    -- $optional1
    --
    -- 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:

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

    -- $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:
    --
    -- <https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall How to translate recursive code to Dhall>