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

-- $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 :: 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]" :: 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 :: 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 ]" :: 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 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 also import Dhall expressions from environment variables, too:
--
-- > >>> System.Environment.setEnv "FOO" "1"
-- > >>> input auto "env:FOO" :: IO Integer
-- > 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
--
-- 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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not>
--
-- Visit that link and read the documentation.  Then try to guess what this
-- code returns:
--
-- > >>> input auto "https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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]
--
-- 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 Integer)
-- > *** Exception: 
-- > Error: Empty lists need a type annotation
-- > 
-- > []
-- > 
-- > (input):1:1
-- > >>> input auto "[] : List Integer" :: IO (Vector Integer)
-- > []
--
-- 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 Integer)
-- > *** Exception: 
-- > Error: List elements should have the same type
-- > 
-- > [1, True, 3]
-- > 
-- > (input):1:1
--
-- __Exercise:__ What is the shortest @./config@ file that you can decode using
-- this command:
--
-- > >>> input auto "./config" :: IO (Vector (Vector Integer))

-- $optional0
--
-- @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
--
-- You cannot omit the type annotation for @Optional@ values.  The type
-- annotation is mandatory
--
-- __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 ]
-- > <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 && True, n && False, n || True, n || False]
--
-- 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]
--
-- ... 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]
--
-- 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 ${Integer/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 : Integer }
-- > 
-- > { bar = "ABC", baz = True, foo = 1 }
-- > $ dhall
-- > { foo = 1, bar = "ABC" } ⫽ { bar = True }  -- Fancy unicode
-- > <Ctrl-D>
-- > { bar : Bool, foo : Integer }
-- > 
-- > { 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?

-- $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>
-- > (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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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 --pretty
-- > 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 : 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]
-- > <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 Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map
-- > in  λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3]
-- > <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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate>
--
-- Test what the following Dhall expression normalizes to:
--
-- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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)

-- $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 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 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 using ./headers
-- 
-- ... and @http:\/\/example.com@ 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'
-- > Integer
-- > 
-- > 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
-- > Integer
-- > 
-- > 1
--
-- You can compute the Hash for any import by using the @dhall-hash@ utility
-- installed by 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!

-- $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
--
-- This package also provides a @dhall-format@ executable 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 @dhall-format@ executable:
--
-- > $ 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://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate 
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
-- > <Ctrl-D>
-- >     let replicate =
-- >           https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate 
-- > 
-- > in  replicate
-- >     +5
-- >     (List (List Integer))
-- >     (replicate +5 (List Integer) (replicate +5 Integer 1))
--
-- If you want to evaluate and format an expression then you can combine the
-- @dhall@ and @dhall-format@ executables:
--
-- > $ dhall | dhall-format
-- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate 
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
-- > <Ctrl-D>
-- > List (List (List Integer))
-- > 
-- >   [   [ [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       ]
-- >     : List (List Integer)
-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       ]
-- >     : List (List Integer)
-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       ]
-- >     : List (List Integer)
-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       ]
-- >     : List (List Integer)
-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
-- >       ]
-- >     : List (List Integer)
-- >   ]
-- > : List (List (List Integer))
--
-- You can also use the formatter to modify files in place using the
-- @--inplace@ flag:
--
-- > $ 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

-- $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 : 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 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 empty @List@ must end with a mandatory type annotation, for example:
--
-- > [] : List Integer
--
-- The built-in operations on @List@s are:

-- $listAppend
--
-- Example:
--
-- > $ dhall
-- > [1, 2, 3] # [4, 5, 6]
-- > <Ctrl-D>
-- > List Integer
-- >
-- > [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://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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 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]
-- > <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]
-- > <Ctrl-D>
-- > Optional Integer
-- > 
-- > [1] : Optional Integer
--
-- Type:
--
-- > ─────────────────────────────────────
-- > Γ ⊢ List/head ∀(a : Type) → List a → Optional a
--
-- Rules:
--
-- > let Prelude/Optional/head  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/head
-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat
-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap
-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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) = [x] : Optional a
-- > 
-- > 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 Integer [1, 2, 3]
-- > <Ctrl-D>
-- > Optional Integer
-- > 
-- > [1] : Optional Integer
--
-- Type:
--
-- > ─────────────────────────────────────
-- > Γ ⊢ List/last : ∀(a : Type) → List a → Optional a
--
-- Rules:
--
-- > let Prelude/Optional/last  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/last
-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat
-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap
-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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) = [x] : Optional a
-- > 
-- > 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://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/shifted
-- > let Prelude/List/concat  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat
-- > let Prelude/List/map     = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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 Integer [1, 2, 3]
-- > <Ctrl-D>
-- > List Integer
-- > 
-- > [3, 2, 1] : List Integer
--
-- Type:
--
-- > ─────────────────────────────────────────────────
-- > Γ ⊢ List/reverse : ∀(a : Type) → List a → List a
--
-- Rules:
--
-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map
-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat
-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/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 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:
--
-- <http://prelude.dhall-lang.org>
--
-- ... which currenty redirects to:
--
-- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not>
--
-- The @not@ function is just a UTF8-encoded text file hosted online with the
-- following contents
--
-- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not True
-- > <Ctrl-D>
-- > Bool
-- > 
-- > False
--
-- ... or assign the URL to a shorter name:
--
-- > $ dhall
-- > let Bool/not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/
-- > $ tree Prelude
-- > Prelude
-- > ├── Bool
-- > │   ├── and
-- > │   ├── build
-- > │   ├── even
-- > │   ├── fold
-- > │   ├── not
-- > │   ├── odd
-- > │   ├── or
-- > │   └── show
-- > ├── Double
-- > │   └── show
-- > ├── Integer
-- > │   └── show
-- > ├── 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
-- > │   ├── show
-- > │   ├── sum
-- > │   └── toInteger
-- > ├── Optional
-- > │   ├── build
-- > │   ├── concat
-- > │   ├── fold
-- > │   ├── head
-- > │   ├── last
-- > │   ├── map
-- > │   ├── toList
-- > │   └── unzip
-- > ├── Text
-- > │   └── concat
-- > └── index.html
--
-- ... or if you have an @ipfs@ daemon running, you can mount the Prelude
-- locally like this:
--
-- > $ ipfs mount
-- > $ cd /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude
--
-- Browse the Prelude online to learn more by seeing what functions are
-- available and reading their inline documentation:
--
-- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/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/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>