{-# 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
    -- $optional

    -- * Records
    -- $records

    -- * Functions
    -- $functions

    -- * Strings
    -- $strings

    -- * Combine
    -- $combine

    -- * Let expressions
    -- $let

    -- * Unions
    -- $unions

    -- * Polymorphic functions
    -- $polymorphic

    -- * Total
    -- $total

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

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

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

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

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

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

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

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

    -- ** @Optional@
    -- $optional

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

    -- * Prelude
    -- $prelude

    -- * Conclusion
    -- $conclusion

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

import Data.Vector (Vector)
import Dhall (Interpret(..), Type, detailed, input)

-- $introduction
--
-- The simplest way to use Dhall is to ignore the programming language features
-- and use it as a strongly typed configuration format.  For example, suppose
-- that you create the following configuration file:
-- 
-- > $ cat ./config
-- > { foo = 1
-- > , bar = [3.0, 4.0, 5.0] : List Double
-- > }
-- 
-- You can read the above configuration file into Haskell using the following
-- code:
-- 
-- > -- example.hs
-- > 
-- > {-# LANGUAGE DeriveGeneric     #-}
-- > {-# LANGUAGE OverloadedStrings #-}
-- > 
-- > import Dhall
-- > 
-- > data Example = Example { foo :: Integer, bar :: Vector Double }
-- >     deriving (Generic, Show)
-- > 
-- > instance Interpret Example
-- > 
-- > main :: IO ()
-- > main = do
-- >     x <- input auto "./config"
-- >     print (x :: Example)
-- 
-- If you compile and run the above example, the program prints the corresponding
-- Haskell record:
-- 
-- > $ ./example
-- > Example {foo = 1, bar = [3.0,4.0,5.0]}
--
-- You can also load some types directly into Haskell without having to define a
-- record, like this:
--
-- > >>> :set -XOverloadedStrings
-- > >>> input auto "True" :: IO Bool
-- > True
--
-- The `input` function can decode any value if we specify the value's expected
-- `Type`:
--
-- > input
-- >     :: Type a  -- Expected type
-- >     -> Text    -- Dhall program
-- >     -> IO a    -- Decoded expression
--
-- ... and we can either specify an explicit type like `bool`:
--
-- > bool :: Type Bool
-- > 
-- > input bool :: Text -> IO Bool
-- >
-- > input bool "True" :: IO Bool
-- >
-- > >>> input bool "True"
-- > True
--
-- ... or we can use `auto` to let the compiler infer what type to decode from
-- the expected return type:
--
-- > auto :: Interpret a => Type a
-- >
-- > input auto :: Interpret a => Text -> IO a
-- >
-- > >>> input auto "True" :: IO Bool
-- > True
--
-- You can see what types `auto` supports \"out-of-the-box\" by browsing the
-- instances for the `Interpret` class.  For example, the following instance
-- says that we can directly decode any Dhall expression that evaluates to a
-- @Bool@ into a Haskell `Bool`:
--
-- > instance Interpret Bool
--
-- ... which is why we could directly decode the string @\"True\"@ into the
-- value `True`.
--
-- There is also another instance that says that if we can decode a value of
-- type @a@, then we can also decode a @List@ of values as a `Vector` of @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] : List Bool" :: IO (Vector Bool)
-- > [True,False]
--
-- We could also specify what type to decode by providing an explicit `Type`
-- instead of using `auto` with a type annotation:
--
-- > >>> input (vector bool) "[True, False] : List Bool"
-- > [True, False]
--
-- __Exercise:__ Create a @./config@ file that the following program can decode:
--
-- > {-# LANGUAGE DeriveGeneric     #-}
-- > {-# LANGUAGE OverloadedStrings #-}
-- > 
-- > import Dhall
-- > 
-- > data Person = Person { age :: Integer, name :: Text }
-- >     deriving (Generic, Show)
-- > 
-- > instance Interpret Person
-- > 
-- > main :: IO ()
-- > main = do
-- >     x <- input auto "./config"
-- >     print (x :: Person)
--
-- __Exercise:__ Create a @./config@ file that the following program can decode:
--
-- > {-# LANGUAGE OverloadedStrings #-}
-- > 
-- > import Data.Functor.Identity
-- > import Dhall
-- > 
-- > instance Interpret a => Interpret (Identity a)
-- > 
-- > main :: IO ()
-- > main = do
-- >     x <- input auto "./config"
-- >     print (x :: Identity Double)

-- $types
--
-- Suppose that we try to decode a value of the wrong type, like this:
--
-- > >>> input auto "1" :: IO Bool
-- > *** Exception: 
-- > Error: Expression doesn't match annotation
-- > 
-- > 1 : Bool
-- > 
-- > (input):1:1
--
-- The interpreter complains because the string @\"1\"@ cannot be decoded into a
-- Haskell value of type `Bool`.
--
-- The code excerpt from the above error message has two components:
--
-- * the expression being type checked (i.e. @1@)
-- * the expression's expected type (i.e. @Bool@)
--
-- > Expression
-- > ⇩
-- > 1 : Bool
-- >     ⇧
-- >     Expected type
--
-- The @(:)@ symbol is how Dhall annotates values with their expected types.
-- This notation is equivalent to type annotations in Haskell using the @(::)@
-- symbol.  Whenever you see:
--
-- > x : t
--
-- ... you should read that as \"we expect the expression @x@ to have type
-- @t@\". However, we might be wrong and if our expected type does not match the
-- expression's actual type then the type checker will complain.
--
-- In this case, the expression @1@ does not have type @Bool@ so type checking
-- fails with an exception.
--
-- __Exercise:__ Load the Dhall library into @ghci@ and run these commands to get
-- get a more detailed error message:
--
-- > >>> import Dhall
-- > >>> :set -XOverloadedStrings
-- > >>> detailed (input auto "1") :: IO Bool
-- > ...
--
-- ... then read the entire error message
--
-- __Exercise:__ Fix the type error, either by changing the value to decode or
-- changing the expected type

-- $imports
--
-- You might wonder why in some cases we can decode a configuration file:
--
-- > >>> writeFile "bool" "True"
-- > >>> input auto "./bool" :: IO Bool
-- > True
--
-- ... and in other cases we can decode a value directly:
--
-- > >>> input auto "True" :: IO Bool
-- > True
--
-- This is because importing a configuration from a file is a special case of a
-- more general language feature: Dhall expressions can reference other
-- expressions by their file path.
--
-- To illustrate this, let's create three files:
-- 
-- > $ echo "True"  > bool1
-- > $ echo "False" > bool2
-- > $ echo "./bool1 && ./bool2" > both
--
-- ... and read in all three files in a single expression:
-- 
-- > >>> input auto "[ ./bool1 , ./bool2 , ./both ] : List Bool" :: IO (Vector Bool)
-- > [True,False,False]
--
-- Each file path is replaced with the Dhall expression contained within that
-- file.  If that file contains references to other files then those references
-- are transitively resolved.
--
-- In other words: configuration files can reference other configuration files,
-- either by their relative or absolute paths.  This means that we can split a
-- configuration file into multiple files, like this:
--
-- > $ cat > ./config <<EOF
-- > { foo = 1
-- > , bar = ./bar
-- > }
-- > EOF
--
-- > $ echo "[ 3.0, 4.0, 5.0 ] : List Double" > ./bar
--
-- > $ ./example
-- > Example {foo = 1, bar = [3.0,4.0,5.0]}
--
-- However, the Dhall language will forbid cycles in these file references.  For
-- example, if we create the following cycle:
--
-- > $ echo './file1' > file2
-- > $ echo './file2' > file1
--
-- ... then the interpreter will reject the import:
--
-- > >>> input auto "./file1" :: IO Integer
-- > *** Exception: 
-- > ↳ ./file1
-- >   ↳ ./file2
-- >
-- > Cyclic import: ./file1
--
-- You can also import expressions by URL.  For example, you can find a Dhall
-- expression hosted at this URL using @ipfs@:
--
-- <https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB>
--
-- > $ curl https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB
-- > True
--
-- ... and you can reference that expression either directly:
--
-- > >>> input auto "https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
-- > True
-- 
-- ... or inside of a larger expression:
--
-- > >>> input auto "False == https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
-- > False
--
-- You're not limited to hosting Dhall expressions on @ipfs@.  You can host a
-- Dhall expression anywhere that you can host UTF8-encoded text on the web, such
-- as Github, a pastebin, or your own web server.
--
-- You can import types, too.  For example, we can change our @./bar@ file to:
--
-- > $ echo "[ 3.0, 4.0, 5.0 ] : List ./type" > ./bar
--
-- ... then specify the @./type@ in a separate file:
--
-- > $ echo "Double" > ./type
--
-- ... and everything still type checks:
--
-- > $ ./example
-- > Example {foo = 1, bar = [3.0,4.0,5.0]}
--
-- Note that all imports must be terminated by whitespace or you will get either
-- an import error or a parse error, like this:
--
-- > >>> writeFile "baz" "2.0"
-- > >>> input auto "./baz: Double" :: IO Double
-- > *** Exception: 
-- > ↳ ./baz: 
-- > 
-- > Error: Missing file
--
-- This is because the parser thinks that @./baz:@ is a single token due to
-- the missing whitespace before the colon and tries to import a file named
-- @./baz:@, which does not exist.  To fix the problem we have to add a space
-- after @./baz@:
--
-- > >>> input auto "./baz : Double" :: IO Double
-- > 2.0
--
-- __Exercise:__ There is a @not@ function hosted online here:
--
-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>
--
-- Visit that link and read the documentation.  Then try to guess what this
-- code returns:
--
-- > >>> input auto "https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
-- > ???
--
-- Run the code to test your guess

-- $lists
--
-- You can store 0 or more values of the same type in a list, like this:
--
-- > [1, 2, 3] : List Integer
--
-- Every list must be followed by the type of the list.  The type annotation is
-- not optional and you will get an error if you omit the annotation:
--
-- > >>> input auto "[1, 2, 3]" :: IO (Vector Integer)
-- > *** Exception: (input):1:10: error: unexpected
-- >     EOF, expected: ":"
-- > [1, 2, 3]<EOF> 
-- >          ^     
--
-- Also, list elements must all have the same type which must match the declared
-- type of the list.  You will get an error if you try to store any other type
-- of element:
--
-- > input auto "[1, True, 3] : List Integer" :: IO (Vector Integer)
-- > *** Exception: 
-- > Error: List element has the wrong type
-- > 
-- > [1, True, 3] : List Integer
-- > 
-- > (input):1:1
--
-- __Exercise:__ Create a @./config@ file that decodes to the following result:
--
-- > >>> input auto "./config" :: IO (Vector (Vector Integer))
-- > [[1,2,3],[4,5,6]]

-- $optional
--
-- @Optional@ values are exactly like lists except they can only hold 0 or 1
-- elements.  They cannot hold 2 or more elements:
--
-- For example, these are valid @Optional@ values:
--
-- > [1] : Optional Integer
-- >
-- > []  : Optional Integer
--
-- ... but this is /not/ valid:
--
-- > [1, 2] : Optional Integer  -- NOT valid
--
-- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes:
--
-- > >>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)
-- > Just 1
-- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer)
-- > Nothing
--
-- __Exercise:__ What is the shortest possible @./config@ file that you can decode
-- like this:
--
-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))
-- > ???
--
-- __Exercise:__ Try to decode an @Optional@ value with more than one element and
-- see what happens

-- $records
--
-- Record literals are delimited by curly braces and their fields are separated
-- by commas.  For example, this is a valid record literal:
--
-- > { foo = True
-- > , bar = 2
-- > , baz = 4.2
-- > }
--
-- A record type is like a record literal except instead of specifying each
-- field's value we specify each field's type.  For example, the preceding
-- record literal has the following record type:
--
-- > { foo : Bool
-- > , bar : Integer
-- > , baz : Double
-- > }
--
-- If you want to specify an empty record literal, you must use @{=}@, which is
-- special syntax reserved for empty records.  If you want to specify the empty
-- record type, then you use @{}@.  If you forget which is which you can always
-- ask the @dhall@ compiler to remind you of the type for each one:
--
-- > $ dhall
-- > {=}
-- > <Ctrl-D>
-- > {}
-- > 
-- > {=}
--
-- > $ dhall
-- > {}
-- > <Ctrl-D>
-- > Type
-- > 
-- > {}
--
-- You can access a field of a record using the following syntax:
--
-- > record.fieldName
--
-- ... which means to access the value of the field named @fieldName@ from the
-- @record@.  For example:
--
-- > >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double
-- > 4.2
--
-- __Exercise__: What is the type of this record:
--
-- > { foo = 1
-- > , bar =
-- >     { baz = 2.0
-- >     , qux = True
-- >     }
-- > }
--
-- __Exercise__: Save the above code to a file named @./record@ and then try to
-- access the value of the @baz@ field

-- $functions
--
-- The Dhall programming language also supports user-defined anonymous
-- functions.  For example, we can save the following anonymous function to a
-- file:
--
-- > $ cat > makeBools
-- > \(n : Bool) ->
-- >     [ n && True, n && False, n || True, n || False ] : List Bool
-- > <Ctrl-D>
--
-- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB)
-- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into that
-- sort of thing):
--
-- > $ cat > makeBools
-- > λ(n : Bool) →
-- >     [ n && True, n && False, n || True, n || False ] : List Bool
-- > <Ctrl-D>
--
-- You can read 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.
--
-- We can test our @makeBools@ function directly from the command line. This
-- library comes with a command-line executable program named @dhall@ that you
-- can use to both type-check files and convert them to a normal form.  Our
-- compiler takes a program on standard input and then prints the program's type
-- to standard error followed by the program's normal form to standard output:
--
-- > $ dhall
-- > ./makeBools
-- > <Ctrl-D>
-- > ∀(n : Bool) → List Bool
-- > 
-- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool
--
-- The first line says that @makeBools@ is a function of one argument named @n@
-- that has type @Bool@ and the function returns a @List@ of @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 && True, n && False, n || True, n || False] : List Bool
--
-- ... which in this case happens to be identical to our original program.
--
-- To apply a function to an argument you separate the function and argument by
-- whitespace (just like Haskell):
--
-- @f x@
--
-- You can read the above as \"apply the function @f@ to the argument @x@\".  This
-- means that we can \"apply\" our @./makeBools@ function to a @Bool@ argument
-- like this:
--
-- > $ dhall
-- > ./makeBools True
-- > <Ctrl-D>
-- > List Bool
-- > 
-- > [True, False, True, True] : List Bool
--
-- Remember that file paths are synonymous with their contents, so the above
-- code is exactly equivalent to:
-- 
-- > $ dhall
-- > (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) True
-- > <Ctrl-D>
-- > List Bool
-- > 
-- > [True, False, True, True] : List Bool
--
-- When you apply an anonymous function to an argument, you substitute the
-- \"bound variable" with the function's argument:
--
-- >    Bound variable
-- >    ⇩
-- > (λ(n : Bool) → ...) True
-- >                     ⇧
-- >                     Function argument
--
-- So in our above example, we would replace all occurrences of @n@ with @True@,
-- like this:
--
-- > -- If we replace all of these `n`s with `True` ...
-- > [n && True, n && False, n || True, n || False] : List Bool
-- >
-- > -- ... then we get this:
-- > [True && True, True && False, True || True, True || False] : List Bool
-- >
-- > -- ... which reduces to the following normal form:
-- > [True, False, True, True] : List Bool
--
-- Now that we've verified that our function type checks and works, we can use
-- the same function within Haskell:
--
-- > >>> input auto "./makeBools True" :: IO (Vector Bool)
-- > [True,False,True,True]
--
-- __Exercise__: Create a file named @getFoo@ that is a function of the following
-- type:
--
-- > ∀(r : { foo : Bool, bar : Text }) → Bool
--
-- This function should take a single input argument named @r@ that is a record
-- with two fields.  The function should return the value of the @foo@ field.
--
-- __Exercise__: Use the @dhall@ compiler to infer the type of the function you
-- just created and verify that your function has the correct type
--
-- __Exercise__: Use the @dhall@ compiler to apply your function to a sample
-- record

-- $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).\"
--
-- Unlike Nix-style strings, you cannot interpolate variables into the string.

-- $combine
--
-- You can combine two records, using the @(/\\)@ operator or the
-- corresponding Unicode @(∧)@ (U+2227) operator:
--
-- > $ dhall
-- > { foo = 1, bar = "ABC" } /\ { baz = True }
-- > <Ctrl-D>
-- > { bar : Text, baz : Bool, foo : Integer }
-- > 
-- > { bar = "ABC", baz = True, foo = 1 }
--
-- > $ dhall
-- > { foo = 1, bar = "ABC" } ∧ { baz = True }  -- Fancy unicode
-- > <Ctrl-D>
-- > { bar : Text, baz : Bool, foo : Integer }
-- > 
-- > { bar = "ABC", baz = True, foo = 1 }
--
-- Note that the order of record fields does not matter.  The compiler
-- automatically sorts the fields when normalizing expressions.
--
-- The @(∧)@ operator also merges records recursively.  For example:
--
-- > $ dhall
-- > { foo = { bar = True }, baz = "ABC" } ∧ { foo = { qux = 1.0 } }
-- > <Ctrl-D>
-- > { baz : Text, foo : { bar : Bool, qux : Double } }
-- > 
-- > { baz = "ABC", foo = { bar = True, qux = 1.0 } }
--
-- However, you cannot combine two records if they share a field that is not a
-- record:
--
-- > $ dhall
-- > { foo = 1, bar = "ABC" } ∧ { foo = True }
-- > <Ctrl-D>
-- > Use "dhall --explain" for detailed errors
-- > 
-- > Error: Field collision
-- > 
-- > { foo = 1, bar = "ABC" } ∧ { foo = True }
-- > 
-- > (stdin):1:1
--
-- __Exercise__: Combine any record with the empty record.  What do you expect to
-- happen?

-- $let
--
-- Dhall also supports @let@ expressions, which you can use to define
-- intermediate values in the course of a computation, like this:
--
-- > $ dhall
-- > let x = "ha" in x ++ x
-- > <Ctrl-D>
-- > Text
-- >
-- > "haha"
--
-- You can also annotate the types of values defined within a @let@ expression,
-- like this:
--
-- > $ dhall
-- > let x : Text = "ha" in x ++ x
-- > <Ctrl-D>
-- > Text
-- >
-- > "haha"
--
-- Every @let@ expression of the form:
--
-- > let x : t = y in e
--
-- ... is exactly equivalent to:
--
-- > (λ(x : t) → e) y
--
-- So for example, this @let@ expression:
--
-- > let x : Text = "ha" in x ++ x
--
-- ... is equivalent to:
--
-- > (λ(x : Text) → x ++ x) "ha"
--
-- ... which in turn reduces to:
--
-- > "ha" ++ "ha"
--
-- ... which in turn reduces to:
--
-- > "haha"
--
-- You need to nest @let@ expressions if you want to define more than one value
-- in this way:
--
-- > $ dhall
-- >     let x = "Hello, "
-- > in  let y = "world!"
-- > in  x ++ y
-- > <Ctrl-D>
-- > Text
-- > 
-- > "Hello, world!"
--
-- Dhall is whitespace-insensitive, so feel free to format things over multiple
-- lines or indent in any way that you please.
--
-- If you want to define a named function, just give a name to an anonymous
-- function:
--
-- > $ dhall
-- > let twice = λ(x : Text) → x ++ x in twice "ha"
-- > <Ctrl-D>
-- > Text
-- > 
-- > "haha"
--
-- Unlike Haskell, Dhall does not support function arguments on the left-hand
-- side of the equals sign, so this will not work:
--
-- > $ dhall
-- > let twice (x : Text) = x ++ x in twice "ha"
-- > <Ctrl-D>
-- > (stdin):1:11: error: expected: ":",
-- >     "="
-- > let twice (x : Text) = x ++ x in twice "ha" 
-- >           ^
--
-- The error message says that Dhall expected either a @(:)@ (i.e. the beginning
-- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a
-- function argument.
--
-- You can also use @let@ expressions to rename imports, like this:
--
-- > $ dhall
-- > let not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
-- > in  not True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- __Exercise:__ What do you think the following code will normalize to?
--
-- >     let x = 1
-- > in  let x = 2
-- > in  x
--
-- Test your guess using the @dhall@ compiler
--
-- __Exercise:__ Now try to guess what this code will normalize to:
--
-- >     let x = "ha"
-- > in  let x = x ++ "ha"
-- > in  x
--
-- __Exercise:__ What about this code?
--
-- > let x = x ++ "ha"
-- > in  x

-- $unions
--
-- A union is a value that can be one of many alternative types of values.  For
-- example, the following union type:
--
-- > < Left : Natural | Right : Bool >
--
-- ... represents a value that can be either a @Natural@ or a @Bool@ value.  If
-- you are familiar with Haskell these are exactly analogous to Haskell's
-- \"sum types\".
--
-- Each alternative is associated with a tag that distinguishes that alternative
-- from other alternatives.  In the above example, the @Left@ tag is used for
-- the @Natural@ alternative and the @Right@ tag is used for the @Bool@
-- alternative.
--
-- A union literal specifies the value of one alternative and the types of the
-- remaining alternatives.  For example, both of the following union literals
-- have the same type, which is the above union type:
--
-- > < Left  = +0   | Right : Bool    >
--
-- > < Right = True | Left  : Natural >
--
-- You can consume a union using the built-in @merge@ function.  For example,
-- suppose we want to convert our union to a @Bool@ but we want to behave
-- differently depending on whether or not the union is a @Natural@ wrapped in
-- the @Left@ alternative or a @Bool@ wrapped in the @Right@ alternative.  We
-- would write:
--
-- > $ cat > process <<EOF
-- >     λ(union : < Left : Natural | Right : Bool >)
-- > →   let handlers =
-- >             { Left  = Natural/even  -- Natural/even is a built-in function
-- >             , Right = λ(b : Bool) → b
-- >             }
-- > in  merge handlers union : Bool
-- > EOF
--
-- Now our @./process@ function can handle both alternatives:
--
-- > $ dhall
-- > ./process < Left = +3 | Right : Bool >
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- > $ dhall
-- > ./process < Right = True | Left : Natural >
-- > <Ctrl-D>
-- > Bool
-- > 
-- > True
--
-- Every @merge@ has the following form:
--
-- > merge handlers union : type
--
-- ... where: 
--
-- * @union@ is the union you want to consume
-- * @handlers@ is a record with one function per alternative of the union
-- * @type@ is the declared result type of the @merge@
--
-- The @merge@ function selects which function to apply from the record based on
-- which alternative the union selects:
--
-- > merge { Foo = f, ... } < Foo = x | ... > : t = f x : t
--
-- So, for example:
--
-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool
-- >     = Natural/even +3 : Bool
-- >     = False
--
-- ... and similarly:
--
-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > : Bool
-- >     = (λ(b : Bool) → b) True : Bool
-- >     = True
--
-- Notice that each handler has to return the same type of result (@Bool@ in
-- this case) which must also match the declared result type of the @merge@.
--
-- __Exercise__: Create a list of the following type with at least one element:
-- per alternative:
--
-- > List < Left : Integer | Right : Double >

-- $polymorphic
--
-- The Dhall language supports defining polymorphic functions (a.k.a.
-- \"generic\" functions) that work on more than one type of value.  However,
-- Dhall differs from Haskell by not inferring the types of these polymorphic
-- functions.  Instead, you must be explicit about what type of value the
-- function is specialized to.
--
-- Take, for example, Haskell's identity function named @id@:
--
-- > id :: a -> a
-- > id = \x -> x
--
-- The identity function is polymorphic, meaning that `id` works on values of
-- different types:
--
-- > >>> id 4
-- > 4
-- > >>> id True
-- > True
--
-- The equivalent function in Dhall is:
--
-- > λ(a : Type) → λ(x : a) → x
--
-- Notice how this function takes two arguments instead of one.  The first
-- argument is the type of the second argument.
--
-- Let's illustrate how this works by actually using the above function:
--
-- > $ echo "λ(a : Type) → λ(x : a) → x" > id
--
-- If we supply the function alone to the compiler we get the inferred type as
-- the first line:
-- 
-- > $ dhall
-- > ./id
-- > <Ctrl-D>
-- > ∀(a : Type) → ∀(x : a) → a
-- > 
-- > λ(a : Type) → λ(x : a) → x
--
-- You can read the type @(∀(a : Type) → ∀(x : a) → a)@ as saying: \"This is the
-- type of a function whose first argument is named @a@ and is a @Type@.  The
-- second argument is named @x@ and has type @a@ (i.e. the value of the first
-- argument).  The result also has type @a@.\"
--
-- This means that the type of the second argument changes depending on what
-- type we provide for the first argument.  When we apply @./id@ to @Integer@, we
-- create a function that expects an @Integer@ argument:
--
-- > $ dhall
-- > ./id Integer
-- > <Ctrl-D>
-- > ∀(x : Integer) → Integer
-- > 
-- > λ(x : Integer) → x
--
-- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a
-- @Bool@ argument:
--
-- > $ dhall
-- > ./id Bool
-- > <Ctrl-D>
-- > ∀(x : Bool) → Bool
-- > 
-- > λ(x : Bool) → x
--
-- We can then supply the final argument to each of those functions to show
-- that they both work on their respective types:
--
-- > $ dhall
-- > ./id Integer 4
-- > <Ctrl-D>
-- > Integer
-- > 
-- > 4
--
-- > $ dhall
-- > ./id Bool True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > True
--
-- Built-in functions can also be polymorphic, too.  For example, we can ask
-- the compiler for the type of @List/reverse@, the function that reverses a
-- list:
--
-- > $ dhall
-- > List/reverse
-- > <Ctrl-D>
-- > ∀(a : Type) → List a → List a
-- > 
-- > List/reverse
--
-- The first argument to @List/reverse@ is the type of the list to reverse:
--
-- > $ dhall
-- > List/reverse Bool
-- > <Ctrl-D>
-- > List Bool → List Bool
-- > 
-- > List/reverse Bool
--
-- ... and the second argument is the list to reverse:
--
-- > $ dhall
-- > List/reverse Bool ([True, False] : List Bool)
-- > <Ctrl-D>
-- > List Bool
-- > 
-- > [False, True] : List Bool
--
-- Note that the second argument has no name.  This type:
--
-- > ∀(a : Type) → List a → List a
--
-- ... is equivalent to this type:
--
-- > ∀(a : Type) → ∀(_ : List a) → List a
--
-- In other words, if you don't see the @∀@ symbol surrounding a function
-- argument type then that means that the name of the argument is @"_"@.  This
-- is true even for user-defined functions:
--
-- > $ dhall
-- > λ(_ : Text) → 1
-- > <Ctrl-D>
-- > Text → Integer
-- > 
-- > λ(_ : Text) → 1
--
-- The type @(Text → Integer)@ is the same as @(∀(_ : Text) → Integer)@
--
-- __Exercise__ : Translate Haskell's `flip` function to Dhall

-- $total
--
-- Dhall is a total programming language, which means that Dhall is not
-- Turing-complete and evaluation of every Dhall program is guaranteed to
-- eventually halt.  There is no upper bound on how long the program might take
-- to evaluate, but the program is guaranteed to terminate in a finite amount of
-- time and not hang forever.
--
-- This guarantees that all Dhall programs can be safely reduced to a normal
-- form where as many functions have been evaluated as possible.  In fact, Dhall
-- expressions can be evaluated even if all function arguments haven't been fully
-- applied.  For example, the following program is an anonymous function:
--
-- > $ dhall
-- > \(n : Bool) -> +10 * +10
-- > <Ctrl-D>
-- > ∀(n : Bool) → Natural
-- > 
-- > λ(n : Bool) → +100
--
-- ... and even though the function is still missing the first argument named
-- @n@ the compiler is smart enough to evaluate the body of the anonymous
-- function ahead of time before the function has even been invoked.
--
-- We can use the @map@ function from the Prelude to illustrate an even more
-- complex example:
--
-- > $ dhall
-- >     let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
-- > in  λ(f : Integer → Integer) → List/map Integer Integer f ([1, 2, 3] : List Integer)
-- > <Ctrl-D>
-- > ∀(f : Integer → Integer) → List Integer
-- > 
-- > λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer
--
-- Dhall can apply our function to each element of the list even before we specify
-- which function to apply.
--
-- The language will also never crash or throw any exceptions.  Every
-- computation will succeed and produce something, even if the result might be
-- an @Optional@ value:
--
-- > $ dhall
-- > List/head Integer ([] : List Integer)
-- > <Ctrl-D>
-- > Optional Integer
-- > 
-- > [] : Optional Integer
--
-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can
-- find here:
--
-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate>
--
-- Test what the following Dhall expression normalizes to:
--
-- > let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate
-- > in  replicate +10
--
-- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by
-- finding an input expression that crashes or loops forever (and file a bug
-- report if you succeed)

-- $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).  A @Natural@ number is a number prefixed
-- with the @+@ symbol.  If you try to add or multiply two @Integer@s (without
-- the @+@ prefix) you will get a type error:
--
-- > $ dhall
-- > 2 + 2
-- > <Ctrl-D>
-- > Use "dhall --explain" for detailed errors
-- > 
-- > Error: ❰+❱ only works on ❰Natural❱s
-- > 
-- > 2 + 2
-- > 
-- > (stdin):1:1
--
-- In fact, there are no built-in functions for @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>
-- > Integer
-- > 
-- > 3
--
-- Type:
--
-- >                Γ ⊢ t : Type
-- >                ─────────────────────
-- > Γ ⊢ b : Bool   Γ ⊢ l : t   Γ ⊢ r : t
-- > ────────────────────────────────────
-- > Γ ⊢ if b then l else r
--
-- Rules:
--
-- > if b then True else False = b
-- > 
-- > if True  then l else r = l
-- > 
-- > if False then l else r = r

-- $natural
--
-- @Natural@ literals are numbers prefixed by a @+@ sign, like this:
--
-- > +4 : Natural
--
-- If you omit the @+@ sign then you get an @Integer@ literal, which is a
-- different type of value

-- $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 either prefixed with a @-@ sign (if they are negative)
-- or no sign (if they are positive), like this:
--
-- >  3 : Integer
-- > -2 : Integer
--
-- If you prefix them with a @+@ sign then they are @Natural@ literals and not
-- @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 @List@ must end with a mandatory type annotation
--
-- The built-in operations on @List@s are:

-- $listFold
--
-- Example:
--
-- > $ dhall
-- > List/fold Bool ([True, False, True] : List Bool) Bool (λ(x : Bool) → λ(y : Bool) → x && y) True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- Type:
--
-- > ────────────────────────────────────────────────────────────────────────────────────────────────────────
-- > Γ ⊢ List/fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list
--
-- Rules:
--
-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
-- >
-- > List/fold a (List/concat a xss) b c
-- >     = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)
-- >
-- > List/fold a ([] : List a) b c n = n
-- >
-- > List/fold a ([x] : List a) b c = c x

-- $listBuild
--
-- Example:
--
-- > $ dhall
-- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))
-- > <Ctrl-D>
-- > List Integer
-- > 
-- > [1, 2, 3] : List Integer
--
-- Type:
--
-- > ───────────────────────────────────────────────────────────────────────────────────────────────────────────
-- > Γ ⊢ List/build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a
--
-- Rules:
--
-- > List/build t (List/fold t x) = x
-- >
-- > List/fold t (List/build t x) = x

-- $listLength
--
-- Example:
--
-- > $ dhall
-- > List/length Integer ([1, 2, 3] : List Integer)
-- > <Ctrl-D>
-- > Natural
-- > 
-- > +3
--
-- Type:
--
-- > ────────────────────────────────────────────────
-- > Γ ⊢ List/length : ∀(a : Type) → List a → Natural
--
-- Rules:
--
-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0

-- $listHead
--
-- Example:
--
-- > $ dhall
-- > List/head Integer ([1, 2, 3] : List Integer)
-- > <Ctrl-D>
-- > Optional Integer
-- > 
-- > [1] : Optional Integer
--
-- Type:
--
-- > ─────────────────────────────────────
-- > Γ ⊢ List/head ∀(a : Type) → List a → Optional a
--
-- Rules:
--
-- > let Optional/head  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/head
-- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap
-- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
-- > 
-- > List/head a (List/concat a xss) =
-- >     Optional/head a (List/map (List a) (Optional a) (List/head a) xss)
-- > 
-- > List/head a ([x] : List a) = [x] : Optional a
-- > 
-- > List/head b (List/concatMap a b f m)
-- >     = Optional/concatMap a b (λ(x : a) → List/head b (f x)) (List/head a m)

-- $listLast
--
-- Example:
--
-- > $ dhall
-- > List/last Integer ([1, 2, 3] : List Integer)
-- > <Ctrl-D>
-- > Optional Integer
-- > 
-- > [1] : Optional Integer
--
-- Type:
--
-- > ─────────────────────────────────────
-- > Γ ⊢ List/last : ∀(a : Type) → List a → Optional a
--
-- Rules:
--
-- > let Optional/last  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/last
-- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap
-- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
-- > 
-- > List/last a (List/concat a xss) =
-- >     Optional/last a (List/map (List a) (Optional a) (List/last a) xss)
-- > 
-- > List/last a ([x] : List a) = [x] : Optional a
-- > 
-- > List/last b (List/concatMap a b f m)
-- >     = Optional/concatMap a b (λ(x : a) → List/last b (f x)) (List/last a m)

-- $listIndexed
--
-- Example
--
-- > $ dhall
-- > List/indexed Text (["ABC", "DEF", "GHI"] : List Text)
-- > <Ctrl-D>
-- > List { index : Natural, value : Text }
-- > 
-- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text }
--
-- Type:
--
-- > ─────────────────────────────────────────────────────────────────────────────
-- > Γ ⊢ List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a }
--
-- Rules:
--
-- > let List/shifted = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/shifted
-- > let List/concat  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
-- > let List/map     = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
-- > 
-- > List/indexed a (List/concat a xss) =
-- >     List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)

-- $listReverse
--
-- Example:
--
-- > $ dhall
-- > List/reverse Integer ([1, 2, 3] : List Integer)
-- > <Ctrl-D>
-- > List Integer
-- > 
-- > [3, 2, 1] : List Integer
--
-- Type:
--
-- > ─────────────────────────────────────────────────
-- > Γ ⊢ List/reverse : ∀(a : Type) → List a → List a
--
-- Rules:
--
-- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
-- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat
-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap
-- > 
-- > List/reverse a (List/concat a xss)
-- >     = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss))
-- >
-- > List/reverse a ([x] : List a) = [x] : List a
-- >
-- > List/reverse b (List/concatMap a b f xs)
-- >     = List/concatMap a b (λ(x : a) → List/reverse b (f x)) (List/reverse a xs)
-- >
-- > List/reverse a ([x, y] : List a) = [y, x] : List a

-- $optional
--
-- Dhall @Optional@ literals are a 0 or 1 values inside of brackets:
--
-- > Γ ⊢ t : Type   Γ ⊢ x : t
-- > ────────────────────────
-- > Γ ⊢ ([x] : Optional t) : Optional t
--
-- > Γ ⊢ t : Type
-- > ────────────────────────
-- > Γ ⊢ ([] : Optional t) : Optional t
--
-- Also, every @Optional@ literal must end with a mandatory type annotation
--
-- The built-in operations on @Optional@ values are:

-- $optionalFold
--
-- Example:
--
-- > $ dhall
-- > Optional/fold Text (["ABC"] : Optional Text) Text (λ(t : Text) → t) ""
-- > <Ctrl-D>
-- > Text
-- > 
-- > "ABC"
--
-- Type:
--
-- > ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
-- > Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(just : a → optional) → ∀(nothing : optional) → optional
--
-- Rules:
--
-- > Optional/fold a ([]  : Optional a) o j n = n
-- >
-- > Optional/fold a ([x] : Optional a) o j n = j x

-- $prelude
--
-- There is also a Prelude available at:
--
-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>
--
-- There is nothing \"official\" or \"standard\" about this Prelude other than
-- the fact that it is mentioned in this tutorial.  The \"Prelude\" is just a
-- set of convenient utilities which didn't quite make the cut to be built into
-- the language.  Feel free to host your own custom Prelude if you want!
--
-- If you visit the above link you can browse the Prelude, which has a few
-- subdirectories.  For example, the @Bool@ subdirectory has a @not@ file
-- located here:
--
-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>
--
-- The @not@ function is just a UTF8-encoded text file hosted online with the
-- following contents
--
-- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
-- > {-
-- > Flip the value of a `Bool`
-- > 
-- > Examples:
-- > 
-- > ```
-- > ./not True = False
-- > 
-- > ./not False = True
-- > ```
-- > -}
-- > let not : Bool → Bool
-- >     =   λ(b : Bool) → b == False
-- > 
-- > in  not
--
-- The file could have been much shorter, like this:
--
-- > λ(b : Bool) → b == False
--
-- ... but all the functions exported from the Prelude try to be as
-- self-documenting as possible by including:
--
-- * the name of the function
-- * the type of the function
-- * documentation (including a few examples)
--
-- The performance penalty for adding these helpful features is negligible.
--
-- You can use this @not@ function either directly:
--
-- > $ dhall
-- > https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- ... or assign the URL to a shorter name:
--
-- > $ dhall
-- > let Bool/not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not
-- > in  Bool/not True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- Some functions in the Prelude just re-export built-in functions for
-- consistency and documentation, such as @Prelude\/Natural\/even@, which
-- re-exports the built-in @Natural/even@ function:
--
-- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even
-- > {-
-- > Returns `True` if a number if even and returns `False` otherwise
-- > 
-- > Examples:
-- > 
-- > ```
-- > ./even +3 = False
-- > 
-- > ./even +0 = True
-- > ```
-- > -}
-- > let even : Natural → Bool
-- >     =   Natural/even
-- > 
-- > in  even
--
-- You can also download the Prelude locally to your filesystem if you prefer
-- using local relative paths instead of URLs.  For example, you can use @wget@,
-- like this:
--
-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/
-- > $ tree Prelude
-- > Prelude
-- > ├── Bool
-- > │   ├── and
-- > │   ├── build
-- > │   ├── even
-- > │   ├── fold
-- > │   ├── not
-- > │   ├── odd
-- > │   └── or
-- > ├── List
-- > │   ├── all
-- > │   ├── any
-- > │   ├── build
-- > │   ├── concat
-- > │   ├── filter
-- > │   ├── fold
-- > │   ├── generate
-- > │   ├── head
-- > │   ├── indexed
-- > │   ├── iterate
-- > │   ├── last
-- > │   ├── length
-- > │   ├── map
-- > │   ├── null
-- > │   ├── replicate
-- > │   ├── reverse
-- > │   ├── shifted
-- > │   └── unzip
-- > ├── Monoid
-- > ├── Natural
-- > │   ├── build
-- > │   ├── enumerate
-- > │   ├── even
-- > │   ├── fold
-- > │   ├── isZero
-- > │   ├── odd
-- > │   ├── product
-- > │   └── sum
-- > ├── Optional
-- > │   ├── build
-- > │   ├── concat
-- > │   ├── fold
-- > │   ├── head
-- > │   ├── last
-- > │   ├── map
-- > │   ├── toList
-- > │   └── unzip
-- > └── Text
-- >     └── concat
--
-- ... or if you have an @ipfs@ daemon running, you can mount the Prelude
-- locally like this:
--
-- > $ ipfs mount
-- > $ cd /ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude
--
-- Browse the Prelude online to learn more by seeing what functions are
-- available and reading their inline documentation:
--
-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>
--
-- __Exercise__: Try to use a new Prelude function that has not been covered
-- previously in this tutorial

-- $conclusion
--
-- By this point you should be able to use the Dhall configuration language to
-- author, import, and program configuration files.  If you run into any issues
-- you can report them at:
--
-- <https://github.com/Gabriel439/Haskell-Dhall-Library/issues>
--
-- You can also request features, support, or documentation improvements on the
-- above issue tracker.
--
-- If you would like to contribute to the Dhall project you can try to port Dhall
-- to other languages besides Haskell so that Dhall configuration files can be
-- read into those languages, too.

-- $faq
--
-- * Why do lists require a type annotation?
--
-- Dhall requires type annotations on lists in order to gracefully deal with
-- empty lists.  Without a type annotation the compiler would not be able to
-- infer the type of an empty list expression:
--
-- > []
--
-- 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.
--
-- * Why do lists require a type annotation when using `input`, like this:
-- 
-- > >>> input (list bool) "[True, False] : List Bool"
--
-- The type annotation on a list is not a real type annotation.  Instead, the
-- annotation on a list is part of the mandatory syntax for lists.  This is why
-- you get a parse error instead of a type error if you omit the annotation:
--
-- > dhall
-- > [1, 2]
-- > (stdin):2:1: error: unexpected
-- >     EOF, expected: ":"
-- >     <EOF> 
-- >     ^