Tutorial.hs

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

{-| Dhall is a programming language specialized for configuration files.  This
    module contains a tutorial explaining how to author configuration files
    using this language

    You might also be interested in the
    <https://docs.dhall-lang.org/tutorials/Language-Tour.html Language Tour>, a
    Haskell-agnostic tour of Dhall's language features.
-}
module Dhall.Tutorial (
    -- * Introduction
    -- $introduction

    -- * Types
    -- $types

    -- * Imports
    -- $imports

    -- * Lists
    -- $lists

    -- * Optional values
    -- $optional0

    -- * Records
    -- $records

    -- * Functions
    -- $functions

    -- * Compiler
    -- $compiler

    -- * Strings
    -- $strings

    -- * Combine
    -- $combine

    -- * Let expressions
    -- $let

    -- * Defaults
    -- $defaults

    -- * Unions
    -- $unions

    -- * Polymorphic functions
    -- $polymorphic

    -- * Total
    -- $total

    -- * Assertions
    -- $assertions

    -- * Headers
    -- $headers

    -- * Import integrity
    -- $integrity

    -- * Raw text
    -- $rawText

    -- * Formatting code
    -- $format

    -- * Built-in functions
    -- $builtins

    -- ** Caveats
    -- $caveats

    -- ** Extending the language
    -- $extending

    -- ** Substitutions
    -- $substitutions

    -- * Prelude
    -- $prelude

    -- * Limitations
    -- $limitations

    -- * Conclusion
    -- $conclusion

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

import Data.Vector (Vector)
import Dhall

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

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

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

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

-- $lists
--
-- You can store 0 or more values of the same type in a list, like this:
--
-- > [1, 2, 3]
--
-- Every list can be followed by the type of the list.  The type annotation is
-- required for empty lists but optional for non-empty lists.  You will get a
-- parse error if you provide an empty list without a type annotation:
--
-- >>> input auto "[]" :: IO (Vector Natural)
-- *** Exception:
-- ...Error...: Invalid input
-- ...
-- (input):1:3:
--   |
-- 1 | []
--   |   ^
-- Empty list literal without annotation
-- ...
--
-- Also, list elements must all have the same type.  You will get an error if
-- you try to store elements of different types in a list:
--
-- >>> input auto "[1, True, 3]" :: IO (Vector Natural)
-- *** Exception:
-- ...Error...: List elements should all have the same type
-- ...
-- - Natural
-- + Bool
-- ...
-- 1│     True
-- ...
-- (input):1:5
-- ...
--
-- __Exercise:__ Replace the @\"???\"@ with an expression that successfully
-- decodes to the specified type:
--
-- > >>> input auto "???" :: IO (Vector (Vector Natural))

-- $optional0
--
-- @Optional@ values are either of the form @Some value@ or @None type@.
--
-- For example, these are valid @Optional@ values:
--
-- > Some 1
-- >
-- > None Natural
--
-- ... which both have type @Optional Natural@
--
-- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes:
--
-- >>> input auto "Some 1" :: IO (Maybe Natural)
-- Just 1
-- >>> input auto "None Natural" :: IO (Maybe Natural)
-- Nothing
--
-- __Exercise:__ Replace the @\"???\"@ with an expression that successfully
-- decodes to the specified type:
--
-- > >>> input auto "???" :: IO (Maybe (Maybe (Maybe Natural)))

-- $records
--
-- Record literals are delimited by curly braces and their fields are separated
-- by commas.  For example, this is a valid record literal:
--
-- > { foo = True
-- > , bar = 2
-- > , baz = 4.2
-- > }
--
-- A record type is like a record literal except instead of specifying each
-- field's value we specify each field's type.  For example, the preceding
-- record literal has the following record type:
--
-- > { foo : Bool
-- > , bar : Natural
-- > , baz : Double
-- > }
--
-- If you want to specify an empty record literal, you must use @{=}@, which is
-- special syntax reserved for empty records.  If you want to specify the empty
-- record type, then you use @{}@.  If you forget which is which you can always
-- ask the @dhall@ compiler to remind you of the type for each one:
--
-- > $ dhall type <<< '{=}'
-- > {}
--
-- > $ dhall type <<< '{}'
-- > Type
--
-- This is our first use of the @dhall@ command-line tool (provided by this
-- package), which provides a @type@ subcommand for inferring an expression's
-- type.  By default the tool reads the expression on standard input and outputs
-- the type to standard output.
--
-- Note that @<<<@ is a feature specific to the Bash shell to feed a string to
-- a command's standard input.  If you are using another shell, then you can
-- instead do this:
--
-- > $ echo '{=}' | dhall type
-- > {}
--
-- __Exercise__: Use the @dhall type@ command to infer the type of this record:
--
-- > -- ./nested.dhall
-- > { foo = 1
-- > , bar =
-- >     { baz = 2.0
-- >     , qux = True
-- >     }
-- > }
--
-- You can specify nested fields using dot-separated keys, like this:
--
-- > { foo = 1, bar.baz = 2.0, bar.qux = True }
--
-- ... which is equivalent to:
--
-- > { foo = 1, bar = { baz = 2.0, qux = True } }
--
-- You can also access a field of a record using the following syntax:
--
-- > record.fieldName
--
-- ... which means to access the value of the field named @fieldName@ from the
-- @record@.  For example:
--
-- >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double
-- 4.2
--
-- ... and you can project out multiple fields into a new record using this
-- syntax:
--
-- > someRecord.{ field₀, field₁, … }
--
-- For example:
--
-- > $ dhall <<< '{ x = 1, y = True, z = "ABC" }.{ x, y }'
-- > { x = 1, y = True }
--
-- This is our first example of using the @dhall@ command-line tool with no
-- subcommand (like @type@), which evaluates the provided expression.  By
-- default, this reads the expression on standard input and outputs the
-- evaluated result on standard output.
--
-- __Exercise__: Save the above @./nested.dhall@ file and then try to access the
-- value of the @baz@ field.  Test that this works by interpreting your code
-- using the @dhall@ command.
--
-- You can convert a record to a list of key-value pairs (a.k.a. a \"Map\") by
-- using the @toMap@ keyword.  For example:
--
-- > $ dhall <<< 'toMap { foo = 1, bar = 2 }'
-- > [ { mapKey = "bar", mapValue = 2 }, { mapKey = "foo", mapValue = 1 } ]
--
-- This conversion only works if all field of the record have the same type.
-- This comes in handy when you need to convert a Dhall record to the Dhall
-- equivalent of a homogeneous map (i.e. Haskell's @"Data.Map"@).

-- $functions
--
-- The Dhall programming language also supports user-defined anonymous
-- functions.  For example, we can save the following anonymous function to a
-- file:
--
-- > -- ./makeBools.dhall
-- > \(n : Bool) ->
-- >     [ n && True, n && False, n || True, n || False ]
--
-- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB)
-- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into
-- that sort of thing):
--
-- > $ -- ./makeBools.dhall
-- > λ(n : Bool) →
-- >     [ n && True, n && False, n || True, n || False ]
-- > <Ctrl-D>
--
-- We'll be sticking to ASCII for the remainder of the tutorial, though, while
-- still pointing out Unicode equivalents as we go.
--
-- You can read this as a function of one argument named @n@ that has type
-- @Bool@.  This function returns a @List@ of @Bool@s.  Each element of the
-- @List@ depends on the input argument named @n@.
--
-- The (ASCII) syntax for anonymous functions resembles the syntax for anonymous
-- functions in Haskell.  The only difference is that Dhall requires you to
-- annotate the type of the function's input.
--
-- You can import this function into Haskell, too:
--
-- >>> makeBools <- input auto "./makeBools.dhall" :: IO (Bool -> Vector Bool)
-- >>> makeBools True
-- [True,False,True,True]
--
-- The reason this works is that there is an `FromDhall` instance for simple
-- functions:
--
-- > instance (ToDhall a, FromDhall b) => FromDhall (a -> b)
--
-- Thanks to currying, this instance works for functions of multiple simple
-- arguments:
--
-- >>> dhallAnd <- input auto "\\(x : Bool) -> \\(y : Bool) -> x && y" :: IO (Bool -> Bool -> Bool)
-- >>> dhallAnd True False
-- False
--
-- However, you can't convert anything more complex than that (like a polymorphic
-- or higher-order function).  You will need to apply those functions to their
-- arguments within Dhall before converting their result to a Haskell value.
--
-- Just like `FromDhall`, you can derive `ToDhall` for user-defined data types:
--
-- > {-# LANGUAGE DeriveAnyClass    #-}
-- > {-# LANGUAGE DeriveGeneric     #-}
-- > {-# LANGUAGE OverloadedStrings #-}
-- >
-- > module Main where
-- >
-- > import Dhall
-- >
-- > data Example0 = Example0 { foo :: Bool, bar :: Bool }
-- >     deriving (Generic, ToDhall)
-- >
-- > main = do
-- >     f <- input auto "\\(r : { foo : Bool, bar : Bool }) -> r.foo && r.bar"
-- >     print (f (Example0 { foo = True, bar = False }) :: Bool)
-- >     print (f (Example0 { foo = True, bar = True  }) :: Bool)
--
-- The above program prints:
--
-- > False
-- > True

-- $compiler
--
-- We can also test our @makeBools@ function directly from the command line.
-- This library comes with a command-line executable program named @dhall@ that
-- you can use to both type-check files and convert them to a normal form.  Our
-- compiler takes a program on standard input and then prints the program's type
-- to standard error followed by the program's normal form to standard output:
--
-- > $ dhall --annotate <<< './makeBools.dhall'
-- > (λ(n : Bool) → [ n, False, True, n ]) : ∀(n : Bool) → List Bool
--
-- The @dhall@ command emits Unicode output by default, but you can switch to
-- ASCII output using the @--ascii@ flag:
--
-- > $ dhall --annotate --ascii <<< './makeBools.dhall'
-- > (\(n : Bool) -> [ n, False, True, n ]) : forall (n : Bool) -> List Bool
--
-- The @--annotate@ flag adds a type signature to the output to let us know
-- what type the interpreter inferred for our expression.  The type signature
-- is @∀(n : Bool) → List Bool@ which says that @makeBools@ is a function of one
-- argument named @n@ that has type @Bool@ and the function returns a @List@ of
-- @Bool@s.  The @∀@ (U+2200) symbol is shorthand for the ASCII @forall@
-- keyword:
--
-- > ∀(x : a) → b         -- This type ...
-- >
-- > forall (x : a) -> b  -- ... is the same as this type
--
-- ... and Dhall's @forall@ keyword behaves the same way as Haskell's @forall@
-- keyword for input values that are @Type@s:
--
-- > forall (x : Type) -> b  -- This Dhall type ...
--
-- > forall x . b            -- ... is the same as this Haskell type
--
-- The part where Dhall differs from Haskell is that you can also use
-- @∀@/@forall@ to give names to non-@Type@ arguments (such as the first
-- argument to @makeBools@).
--
-- This expression is our program's normal form:
--
-- > λ(n : Bool) → [ n, False, True, n ]
--
-- ... and the interpreter was able to simplify our expression by noting that:
--
-- * @n && True  = n@
-- * @n && False = False@
-- * @n || True  = True@
-- * @n || False = n@
--
-- To apply a function to an argument you separate the function and argument by
-- whitespace (just like Haskell):
--
-- @f x@
--
-- You can read the above as \"apply the function @f@ to the argument @x@\".  This
-- means that we can \"apply\" our @./makeBools@ function to a @Bool@ argument
-- like this:
--
-- > $ dhall <<< './makeBools.dhall True'
-- > [True, False, True, True]
--
-- Remember that file paths are synonymous with their contents, so the above
-- code is exactly equivalent to:
--
-- > $ dhall <<< '(\(n : Bool) -> [n && True, n && False, n || True, n || False]) True'
-- > [True, False, True, True]
--
-- When you apply an anonymous function to an argument, you substitute the
-- \"bound variable" with the function's argument:
--
-- >    Bound variable
-- >    ⇩
-- > (\(n : Bool) -> ...) True
-- >                      ⇧
-- >                      Function argument
--
-- So in our above example, we would replace all occurrences of @n@ with @True@,
-- like this:
--
-- > -- If we replace all of these `n`s with `True` ...
-- > [n && True, n && False, n || True, n || False]
-- >
-- > -- ... then we get this:
-- > [True && True, True && False, True || True, True || False]
-- >
-- > -- ... which reduces to the following normal form:
-- > [True, False, True, True]
--
-- Now that we've verified that our function type checks and works, we can use
-- the same function within Haskell:
--
-- >>> input auto "./makeBools.dhall True" :: IO (Vector Bool)
-- [True,False,True,True]
--
-- __Exercise__: Create a file named @getFoo@ that is a function of the following
-- type:
--
-- > forall (r : { foo : Bool, bar : Text }) -> Bool
--
-- This function should take a single input argument named @r@ that is a record
-- with two fields.  The function should return the value of the @foo@ field.
--
-- __Exercise__: Use the @dhall@ command to infer the type of the function you
-- just created and verify that your function has the correct type
--
-- __Exercise__: Use the @dhall@ command to apply your function to a sample
-- record

-- $strings
-- Dhall supports ordinary string literals with Haskell-style escaping rules:
--
-- > $ dhall
-- > "Hello, \"world\"!"
-- > <Ctrl-D>
-- > "Hello, \"world\"!"
--
-- ... and Dhall also supports Nix-style multi-line string literals:
--
-- > $ dhall
-- > ''
-- >     #!/bin/bash
-- >
-- >     echo "Hi!"
-- > ''
-- > <Ctrl-D>
-- > "\n#!/bin/bash\n\necho \"Hi!\"\n"
--
-- These \"double single quote strings\" ignore all special characters, with one
-- exception: if you want to include a @''@ in the string, you will need to
-- escape it with a preceding @'@ (i.e. use @'''@ to insert @''@ into the final
-- string).
--
-- These strings also strip leading whitespace using the same rules as Nix.
-- Specifically: \"it strips from each line a number of spaces equal to the
-- minimal indentation of the string as a whole (disregarding the indentation
-- of empty lines).\"
--
-- You can also interpolate expressions into strings using @${...}@ syntax.  For
-- example:
--
-- > $ dhall
-- > let name = "John Doe"
-- > let age  = 21
-- > in  "My name is ${name} and my age is ${Natural/show age}"
-- > <Ctrl-D>
-- > "My name is John Doe and my age is 21"
--
-- Note that you can only interpolate expressions of type @Text@
--
-- If you need to insert a @"${"@ into a string without interpolation then use
-- @"''${"@ (same as Nix)
--
-- > ''
-- >     for file in *; do
-- >       echo "Found ''${file}"
-- >     done
-- > ''

-- $combine
--
-- You can combine two records, using either the @(//)@ operator or the
-- @(/\\)@ operator.
--
-- The @(//)@ operator (or @(⫽)@ U+2AFD) combines the fields of both records,
-- preferring fields from the right record if they share fields in common:
--
-- > $ dhall
-- > { foo = 1, bar = "ABC" } // { baz = True }
-- > <Ctrl-D>
-- > { bar = "ABC", baz = True, foo = 1 }
-- > $ dhall
-- > { foo = 1, bar = "ABC" } ⫽ { bar = True }  -- Fancy unicode
-- > <Ctrl-D>
-- > { bar = True, foo = 1 }
--
-- Note that the order of record fields does not matter.  The compiler
-- automatically sorts the fields.
--
-- If you need to set or add a deeply nested field you can use the @with@
-- keyword, like this:
--
-- > $ dhall <<< '{ x.y = 1 } with x.z = True'
-- > { x = { y = 1, z = True } }
--
-- > $ dhall <<< '{ x.y = 1 } with x.y = 2'
-- > { x.y = 2 }
--
-- The @with@ keyword is syntactic sugar for the @//@ operator which follows
-- these rules:
--
-- > -- Nested case
-- > record with k.ks… = value  ⇒  record // { k = record.k with ks… = value }
-- >
-- > -- Base case
-- > record with k = value      ⇒  record // { k = value }
--
-- The @(/\\)@ operator (or @(∧)@ U+2227) also lets you combine records, but
-- behaves differently if the records share fields in common.  The operator
-- combines shared fields recursively if they are both records:
--
-- > $ dhall
-- > { foo = { bar = True }, baz = "ABC" } /\ { foo = { qux = 1.0 } }
-- > <Ctrl-D>
-- > { baz = "ABC", foo = { bar = True, qux = 1.0 } }
--
-- ... but fails with a type error if either shared field is not a record:
--
-- > $ dhall
-- > { foo = 1, bar = "ABC" } /\ { foo = True }
-- > <Ctrl-D>
-- > Use "dhall --explain" for detailed errors
-- >
-- > Error: Field collision
-- >
-- > { foo = 1, bar = "ABC" } ∧ { foo = True }
-- >
-- > (input):1:1
--
-- __Exercise__: Combine any record with the empty record.  What do you expect
-- to happen?
--
-- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53):
--
-- > $ dhall
-- > { foo : Natural } //\\ { bar : Text }
-- > <Ctrl-D>
-- > { foo : Natural, bar : Text }
--
-- ... which behaves the exact same, except at the type level, meaning that the
-- operator descends recursively into record types:
--
-- > $ dhall
-- > { foo : { bar : Text } } //\\ { foo : { baz : Bool }, qux : Natural }
-- > <Ctrl-D>
-- > { foo : { bar : Text, baz : Bool }, qux : Natural }

-- $let
--
-- Dhall also supports @let@ expressions, which you can use to define
-- intermediate values in the course of a computation, like this:
--
-- > $ dhall
-- > let x = "ha" in x ++ x
-- > <Ctrl-D>
-- > "haha"
--
-- You can also annotate the types of values defined within a @let@ expression,
-- like this:
--
-- > $ dhall
-- > let x : Text = "ha" in x ++ x
-- > <Ctrl-D>
-- > "haha"
--
-- You need to nest @let@ expressions if you want to define more than one value
-- in this way:
--
-- > $ dhall
-- > let x = "Hello, "
-- > let y = "world!"
-- > in  x ++ y
-- > <Ctrl-D>
-- > "Hello, world!"
--
-- Dhall is whitespace-insensitive, so feel free to format things over multiple
-- lines or indent in any way that you please.
--
-- If you want to define a named function, just give a name to an anonymous
-- function:
--
-- > $ dhall
-- > let twice = \(x : Text) -> x ++ x in twice "ha"
-- > <Ctrl-D>
-- > "haha"
--
-- Unlike Haskell, Dhall does not support function arguments on the left-hand
-- side of the equals sign, so this will not work:
--
-- > $ dhall
-- > let twice (x : Text) = x ++ x in twice "ha"
-- > <Ctrl-D>
-- > Error: Invalid input
-- >
-- > (input):1:11:
-- >   |
-- > 1 | let twice (x : Text) = x ++ x in twice "ha"
-- >   |           ^
-- > unexpected '('
-- > expecting ':', '=', or the rest of label
--
-- The error message says that Dhall expected either a @(:)@ (i.e. the beginning
-- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a
-- function argument.
--
-- You can also use @let@ expressions to rename imports, like this:
--
-- > $ dhall
-- > let not = https://prelude.dhall-lang.org/Bool/not
-- > in  not True
-- > <Ctrl-D>
-- > False
--
-- ... or to define synonyms for types:
--
-- > $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name'
-- > List Text
-- >
-- > [ "John", "Mary" ]
--
-- __Exercise:__ What do you think the following code will normalize to?
--
-- > let x = 1
-- > let x = 2
-- > in  x
--
-- Test your guess using the @dhall@ compiler
--
-- __Exercise:__ Now try to guess what this code will normalize to:
--
-- > let x = "ha"
-- > let x = x ++ "ha"
-- > in  x
--
-- __Exercise:__ What about this code?
--
-- > let x = x ++ "ha"
-- > in  x

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

-- $unions
--
-- A union is a value that can be one of many alternative types of values.  For
-- example, the following union type:
--
-- > < Left : Natural | Right : Bool >
--
-- ... represents a value that can be either a @Natural@ or a @Bool@ value.  If
-- you are familiar with Haskell these are exactly analogous to Haskell's
-- \"sum types\" and the above type is equivalent to @Either Natural Bool@.
--
-- Each alternative is associated with a tag that distinguishes that alternative
-- from other alternatives.  In the above example, the @Left@ tag is used for
-- the @Natural@ alternative and the @Right@ tag is used for the @Bool@
-- alternative.
--
-- You can specify the value of a union constructor like this:
--
-- > let Union = < Left : Natural | Right : Bool>
-- >
-- > in  [ Union.Left 0, Union.Right True ]
--
-- In other words, you can access a union constructor as a field of a union
-- type and use that constructor to wrap a value of a type appropriate for
-- that alternative.  In the above example, the @Left@ constructor can wrap
-- a @Natural@ value and the @Right@ constructor can wrap a @Bool@ value.  We
-- can also confirm that by inspecting their type:
--
-- > $ echo '< Left : Natural | Right : Bool>' > ./Union
--
-- > $ dhall --annotate <<< '(./Union).Left'
-- >   < Left : Natural | Right : Bool >.Left
-- > : ∀(Left : Natural) → < Left : Natural | Right : Bool >
--
-- > $ dhall --annotate <<< '(./Union).Right'
-- >   < Left : Natural | Right : Bool >.Right
-- > : ∀(Right : Bool) → < Left : Natural | Right : Bool >
--
-- In other words, the @Left@ constructor is a function from a @Natural@ to a
-- value of our @Union@ type and the @Right@ constructor is a separate function
-- from a @Bool@ to that same @Union@ type.
--
-- You can consume a union using the built-in @merge@ function.  For example,
-- suppose we want to convert our union to a @Bool@ but we want to behave
-- differently depending on whether or not the union is a @Natural@ wrapped in
-- the @Left@ constructor or a @Bool@ wrapped in the @Right@ constructor .  We
-- would write:
--
-- > $ cat > process <<EOF
-- >   \(union : < Left : Natural | Right : Bool >) ->
-- >     let handlers =
-- >             { Left  = Natural/even  -- Natural/even is a built-in function
-- >             , Right = \(b : Bool) -> b
-- >             }
-- > in  merge handlers union
-- > EOF
--
-- Now our @./process@ function can handle both alternatives:
--
-- > $ dhall <<< './process ((./Union).Left 3)'
-- > False
--
-- > $ dhall <<< './process ((./Union).Right True)'
-- > True
--
-- Every @merge@ has the following form:
--
-- > merge handlers union [ : type ]
--
-- ... where:
--
-- * @union@ is the union you want to consume
-- * @handlers@ is a record with one function per alternative of the union
-- * @type@ is an optional declared result type of the @merge@
--
-- The @merge@ function selects which function to apply from the record based on
-- which alternative the union selects:
--
-- > merge { Foo = f, ... } (< … >.Foo x) = f x
--
-- So, for example:
--
-- > merge { Left = Natural/even, Right = \(b : Bool) -> b } (< Left : Natural | Right : Bool >.Left 3)
-- >     = Natural/even 3
-- >     = False
--
-- ... and similarly:
--
-- > merge { Left = Natural/even, Right = \(b : Bool) -> b } (< Left : Natural | Right : Bool >.Right True)
-- >     = (\(b : Bool) -> b) True
-- >     = True
--
-- Notice that each handler has to return the same type of result (@Bool@ in
-- this case).
--
-- You can also store more than one value within alternatives using Dhall's
-- support for anonymous records.  You can nest an anonymous record within a
-- union such as in this type:
--
-- > < Empty : {} | Person : { name : Text, age : Natural } >
--
-- You can even go a step further and omit the type of an alternative if it
-- stores no data, like this:
--
-- > < Empty | Person : { name : Text, age : Natural } >
--
-- The above Dhall type resembles the following equivalent Haskell data type:
--
-- > data Example = Empty | Person { name :: Text, age :: Text }
--
-- Empty alternatives like @Empty@ require no argument:
--
-- > let Example = < Empty | Person : { name : Text, age : Natural } >
-- >
-- > in  [ Example.Empty  -- Note the absence of any argument to `Empty`
-- >     , Example.Person { name = "John", age = 23 }
-- >     , Example.Person { name = "Amy" , age = 25 }
-- >     ]
--
-- ... and when you @merge@ an empty alternative the correspond handler takes no
-- argument:
--
-- > \(x : < Empty | Person : { name : Text, age : Natural } >) ->
-- >   merge
-- >     { Empty = "Unknown"  -- Note the absence of an anonymous function
-- >
-- >     , Person =
-- >         \(person : { name : Text, age : Natural }) ->
-- >           "Name: ${person.name}, Age: ${Natural/show person.age}"
-- >     }
-- >     x
--
-- __Exercise__: Create a list of the following type with at least one element
-- per alternative:
--
-- > List < Left : Natural | Right : Double >

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

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

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

-- $headers
--
-- Sometimes you would like to provide additional request headers when importing
-- Dhall expressions from URLs.  For example, you might want to provide an
-- authorization header or specify the expected content type.
--
-- Dhall URL imports let you add or modify request headers with the @using@
-- keyword:
--
-- > https://example.com/example.dhall using ./headers
--
-- ... where you can replace @./headers@ with any import that points to a Dhall
-- expression of the following type:
--
-- > List { header : Text, value : Text }
--
-- For example, if you needed to specify the content type correctly in order to
-- download the file, then your @./headers@ file might look like this:
--
-- > $ cat headers
-- > [ { header = "Accept", value = "application/dhall" } ]
--
-- ... or if you needed to provide an authorization token to access a private
-- GitHub repository, then your headers could look like this:
--
-- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN as Text}" } ]
--
-- This would read your GitHub API token from the @GITHUB_TOKEN@ environment
-- variable and supply that token in the authorization header.
--
-- You cannot inline the headers within the same file as the URL.  You must
-- provide them as a separate import.  That means that this is /not/ legal code:
--
-- > http://example.com/example.dhall using [ { header = "Accept", value = "application/dhall" } ]  -- NOT legal
--
-- Dhall will forward imports if you import an expression from a URL that
-- contains a relative import.  For example, if you import an expression like
-- this:
--
-- > http://example.com/example.dhall using ./headers
--
-- ... and @http:\/\/example.com/example.dhall@ contains a relative import of @./foo@
-- then Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file.

-- $integrity
--
-- Sometimes you want to use share code while still ensuring that the imported
-- value never changes and can't be corrupted by a malicious attacker.  Dhall
-- provides built-in support for hashing imported values to verify that their
-- value never changes
--
-- For example, suppose you save the following two files:
--
-- > $ cat ./foo
-- > ./bar sha256:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
--
-- > $ cat ./bar
-- > ./baz
--
-- > $ cat ./baz
-- > 1
--
-- The first file named @./foo@ contains an example of an integrity check.  You
-- can add @sha256:XXX@ after any import (such as after @./bar@), where @XXX@ is
-- an expected 64-character @sha256@ hash of the Dhall value.  To be precise,
-- the hash represents a @sha256@ hash of the UTF-8 encoding of a canonical text
-- representation of the fully resolved and normalized abstract syntax tree of
-- the imported expression.
--
-- Dhall will verify that the expected hash matches the actual hash of the
-- imported Dhall value and reject the import if there is a hash mismatch:
--
-- > $ dhall <<< './foo'
-- > Natural
-- >
-- > 1
--
-- Any import protected by a semantic integrity check is automatically cached
-- locally underneath either @~\/.cache\/dhall\/1220${HASH}@ or
-- @${XDG_CACHE_HOME}\/dhall/1220${HASH}@ if you define the @XDG_CACHE_HOME@
-- environment variable.
--
-- For example, after you import @./foo@ the contents of `./bar` are locally
-- cached in a fully-evaluated and binary-encoded form which you can inspect by
-- running:
--
-- > $ dhall decode < ~/.cache/dhall/1220d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
-- > 1
--
-- Subsequent attempts to resolve the same import will automatically retrieve
-- the import from the cache.  This matters less for local imports, but comes in
-- handy for remote imports to avoid redownloading them.
--
-- The local cache takes precedence when resolving imports, so changing the
-- original import afterwards will have no affect until you update the hash.
-- From Dhall's point of view, the hash is the true address and the file path
-- is just a suggestion for how to obtain the import if it's not already cached.
--
-- You can disable the cache by setting @XDG_CACHE_HOME@ to `/var/empty` (an
-- empty and unwritable directory), like this:
--
-- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo'
-- > Natural
-- >
-- > 1
--
-- We'll use this trick to test changes to the protected import in the following
-- examples.
--
-- Now, suppose you add a comment to the @./bar@ file:
--
-- > $ cat ./bar
-- > -- This comment does not change the hash
-- > ./baz
--
-- ... then @./foo@ will still successfully import @./bar@ because the hash
-- only depends on the normalized value and does not depend on meaningless
-- changes to whitespace or comments:
--
-- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo'  # This still succeeds
-- > Natural
-- >
-- > 1
--
-- You can compute the Hash for any import by using the hash subcommand
-- of this package.  For example:
--
-- > $ dhall hash <<< './bar'
-- > sha256:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
--
-- Now suppose that you actually change the value of the @./baz@ file:
--
-- > $ cat ./baz
-- > 2
--
-- ... then the @./foo@ file will fail to import @./bar@, even though the
-- text of the @./bar@ file technically never changed:
--
-- > XDG_CACHE_HOME=/var/empty dhall <<< './foo'
-- >
-- > Error: Import integrity check failed
-- >
-- > Expected hash:
-- >
-- > ↳ d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15
-- >
-- > Actual hash:
-- >
-- > ↳ 4caf97e8c445d4d4b5c5b992973e098ed4ae88a355915f5a59db640a589bc9cb
--
-- This is because the @./bar@ file now represents a new value (@2@ instead of
-- @1@), even though the text of the @./bar@ file is still the same.  Since the
-- value changed the hash must change as well.  However, we could change @./baz@
-- to:
--
-- > $ cat baz
-- > if True then 1 else 2
--
-- ... and the import would now succeed again because the final result is @1@.
--
-- The integrity hash ensures that your import's final meaning can never change,
-- so an attacker can never compromise an imported value protected by a hash
-- unless they can break SHA-256 encryption.  The hash not only protects the
-- file that you immediately import, but also protects every transitive import
-- as well.
--
-- You can also safely refactor your imported dependencies knowing that the
-- refactor will not change your hash so long as your refactor is
-- behavior-preserving.  This provides an easy way to detect refactoring errors
-- that you might accidentally introduce.  The hash not only protects you
-- from attackers, but also protects against human error, too!
--
-- If you have a file which either doesn't already use hashed imports,
-- or you changed some of the imports and want to update the hashes you can use the
-- freeze command to either add or update hashes:
--
-- > $ cat foo.dhall
-- > let replicate = https://prelude.dhall-lang.org/List/replicate
-- > in  replicate 5
-- > $
-- > $ dhall freeze ./foo.dhall
-- > $ cat ./foo.dhall
-- > let replicate =
-- >       https://prelude.dhall-lang.org/List/replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347
-- >
-- > in  replicate 5

-- $rawText
--
-- Sometimes you want to import the contents of a raw text file as a Dhall
-- value of type `Dhall.Syntax.Text`.  For example, one of the fields of a
-- record might be the contents of a software license:
--
-- > { package = "dhall"
-- > , author  = "Gabriel Gonzalez"
-- > , license = ./LICENSE
-- > }
--
-- Normally if you wanted to import a text file you would need to wrap the
-- contents of the file in double single-quotes, like this:
--
-- > $ cat LICENSE
-- > ''
-- > Copyright (c) 2017 Gabriel Gonzalez
-- > All rights reserved.
-- >
-- > ...
-- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-- > ''
--
-- ... which does not work well if you need to reuse the same text file for
-- other programs
--
-- However, Dhall supports importing a raw text file by adding @as Text@ to the
-- end of the import, like this:
--
-- > { package = "dhall"
-- > , author  = "Gabriel Gonzalez"
-- > , license = ./LICENSE as Text
-- > }
--
-- ... and then you can use the original text file unmodified:
--
-- > $ cat LICENSE
-- > Copyright (c) 2017 Gabriel Gonzalez
-- > All rights reserved.
-- >
-- > ...
-- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

-- $format
--
-- A format subcommand is also available that you can use to
-- automatically format Dhall expressions.  For example, we can take the
-- following unformatted Dhall expression:
--
-- > $ cat ./unformatted
-- > λ(a : Type) → λ(kvss : List (List { index : Natural, value : a })) →
-- > List/build { index : Natural, value : a } (λ(list : Type) → λ(cons : {
-- > index : Natural, value : a } → list → list) → λ(nil : list) →
-- > (List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff :
-- > Natural → list } (λ(kvs : List { index : Natural, value : a }) → λ(y : {
-- > count : Natural, diff : Natural → list }) → { count = y.count + List/length
-- > { index : Natural, value : a } kvs, diff = λ(n : Natural) → List/fold {
-- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a
-- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value }
-- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count =
-- > 0, diff = λ(_ : Natural) → nil }).diff 0)
--
-- ... and run the expression through the formatter:
--
-- > $ dhall format < ./unformatted
-- > λ(a : Type) →
-- > λ(kvss : List (List { index : Natural, value : a })) →
-- >   List/build
-- >     { index : Natural, value : a }
-- >     ( λ(list : Type) →
-- >       λ(cons : { index : Natural, value : a } → list → list) →
-- >       λ(nil : list) →
-- >         ( List/fold
-- >             (List { index : Natural, value : a })
-- >             kvss
-- >             { count : Natural, diff : Natural → list }
-- >             ( λ(kvs : List { index : Natural, value : a }) →
-- >               λ(y : { count : Natural, diff : Natural → list }) →
-- >                 { count =
-- >                     y.count + List/length { index : Natural, value : a } kvs
-- >                 , diff =
-- >                     λ(n : Natural) →
-- >                       List/fold
-- >                         { index : Natural, value : a }
-- >                         kvs
-- >                         list
-- >                         ( λ(kvOld : { index : Natural, value : a }) →
-- >                           λ(z : list) →
-- >                             cons
-- >                               { index = kvOld.index + n, value = kvOld.value }
-- >                               z
-- >                         )
-- >                         ( y.diff
-- >                             (n + List/length { index : Natural, value : a } kvs)
-- >                         )
-- >                 }
-- >             )
-- >             { count = 0, diff = λ(_ : Natural) → nil }
-- >         ).diff
-- >           0
-- >     )
--
-- The executable formats expressions without resolving, type-checking, or
-- normalizing them:
--
-- > $ dhall format
-- > let replicate = https://prelude.dhall-lang.org/List/replicate
-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
-- > <Ctrl-D>
-- > let replicate = https://prelude.dhall-lang.org/List/replicate
-- >
-- > in  replicate
-- >       5
-- >       (List (List Natural))
-- >       (replicate 5 (List Natural) (replicate 5 Natural 1))
--
-- You can also use the formatter to modify files in place:
--
-- > $ dhall format ./unformatted
--
-- Carefully note that the code formatter does not preserve all comments.
-- Currently, the formatter only preserves two types of comments:
--
-- * Leading comments at the beginning of the file
-- * Comments within a @let@ binding
--
-- For example:
--
-- > $ dhall format
-- > {- This comment will be preserved by the formatter -}
-- > -- ... and this comment will be preserved, too
-- > {- This comment will *NOT* be preserved -} 1
-- > -- ... and this comment will also *NOT* be preserved
-- > <Ctrl-D>
-- > {- This comment will be preserved by the formatter -}
-- > -- ... and this comment will be preserved, too
-- > 1
--
-- Also:
--
-- > let {- This comment will be preserved -}
-- >     x {- This comment will also be preserved-} =
-- >     {- ... and this one will be preserved, too -}
-- >       1
-- >
-- > in  x
--
-- Note that you do not need to format the output of the
-- @dhall@ interpreter.  The interpreter already automatically formats
-- multi-line expressions, too:
--
-- > $ dhall
-- > let replicate = https://prelude.dhall-lang.org/List/replicate
-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
-- > <Ctrl-D>
-- > [ [ [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   ]
-- > , [ [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   ]
-- > , [ [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   ]
-- > , [ [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   ]
-- > , [ [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   , [ 1, 1, 1, 1, 1 ]
-- >   ]
-- > ]

-- $builtins
--
-- Dhall is a restricted programming language that only supports simple built-in
-- functions and operators.  If you want to do anything fancier you will need to
-- load your data into Haskell for further processing
--
-- This section covers types, functions, and operators that are built into the
-- language, meaning that you do not need to import any code to use them.
-- Additionally, Dhall also comes with a Prelude (covered in the next section)
-- hosted online that contains functions derived from these base utilities.  The
-- Prelude also re-exports all built-in functions for people who prefer
-- consistency.
--
-- The language provides built-in support for the following primitive types:
--
-- * @Bool@ values
-- * @Natural@ values
-- * @Integer@ values
-- * @Double@ values
-- * @Text@ values
--
-- ... as well as support for the following derived types:
--
-- * @List@s of values
-- * @Optional@ values
-- * Anonymous records
-- * Anonymous unions
--
-- You can find an up-to-date list of available built-in functions and operators
-- here:
--
-- <https://github.com/dhall-lang/dhall-lang/wiki/Built-in-types%2C-functions%2C-and-operators Built-in types, functions, and operators>

-- $caveats
--
-- Dhall differs in a few important ways from other programming languages, so
-- you should keep the following caveats in mind:
--
-- First, Dhall only supports addition and multiplication on @Natural@ numbers
-- (i.e. non-negative integers), which are not the same type of number as
-- @Integer@s (which can be negative).  An @Integer@ number is a number prefixed
-- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading
-- sign.  If you try to add or multiply two @Integer@s you will get a type
-- error:
--
-- > $ dhall
-- > +2 + +2
-- > <Ctrl-D>
-- > Use "dhall --explain" for detailed errors
-- >
-- > Error: ❰+❱ only works on ❰Natural❱s
-- >
-- > +2 + +2
-- >
-- > (input):1:1
--
-- In fact, there are no built-in functions for @Integer@s (or @Double@s) other
-- than @Integer/show@ and @Double/show@.  As far as the language is concerned
-- they are opaque values that can only be shuffled around but not used in any
-- meaningful way until they have been loaded into Haskell.
--
-- Second, the equality @(==)@ and inequality @(!=)@ operators only work on
-- @Bool@s.  You cannot test any other types of values for equality.
--
-- However, you can extend the language with your own built-ins using the
-- Haskell API, as described in the next section.

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

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

-- $prelude
--
-- There is also a Prelude available at:
--
-- <https://prelude.dhall-lang.org>
--
-- If you visit the above link you can browse the Prelude, which has a few
-- subdirectories.  For example, the @Bool@ subdirectory has a @not@ file, which
-- you can reference using this URL:
--
-- <https://prelude.dhall-lang.org/Bool/not>
--
-- The @not@ function is just a UTF8-encoded text file hosted online with the
-- following contents
--
-- > $ dhall <<< 'https://prelude.dhall-lang.org/Bool/not as Text'
-- > ''
-- > {-
-- > Flip the value of a Bool
-- > -}
-- > let not : Bool → Bool = λ(b : Bool) → b == False
-- >
-- > let example0 = assert : not True ≡ False
-- >
-- > let example1 = assert : not False ≡ True
-- >
-- > in  not
-- > ''
--
-- The file could have been much shorter, like this:
--
-- > λ(b : Bool) → b == False
--
-- ... but all the functions exported from the Prelude try to be as
-- self-documenting as possible by including:
--
-- * the name of the function
-- * the type of the function
-- * documentation
-- * tests
--
-- The performance penalty for adding these helpful features is negligible,
-- especially if you protect the import with a semantic integrity check because
-- then the import would be cached compactly as @λ(_ : Bool) → _ == False@.
--
-- You can use this @not@ function either directly:
--
-- > $ dhall
-- > https://prelude.dhall-lang.org/Bool/not True
-- > <Ctrl-D>
-- > False
--
-- ... or assign the URL to a shorter name:
--
-- > $ dhall
-- > let Bool/not = https://prelude.dhall-lang.org/Bool/not
-- > in  Bool/not True
-- > <Ctrl-D>
-- > False
--
-- Some functions in the Prelude just re-export built-in functions for
-- consistency and documentation, such as @Prelude\/Natural\/even@, which
-- re-exports the built-in @Natural/even@ function:
--
-- > $ dhall <<< 'https://prelude.dhall-lang.org/Natural/even as Text'
-- > ''
-- > {-
-- > Returns `True` if a number if even and returns `False` otherwise
-- > -}
-- > let even : Natural → Bool = Natural/even
-- >
-- > let example0 = assert : even 3 ≡ False
-- >
-- > let example1 = assert : even 0 ≡ True
-- >
-- > in  even
-- > ''
--
-- You can also clone the Prelude locally to your filesystem if you prefer
-- using `git clone`, like this:
--
-- > $ git clone https://github.com/dhall-lang/dhall-lang.git
-- > $ tree dhall-lang/Prelude
-- > dhall-lang/Prelude
-- > ├── Bool
-- > │   ├── and
-- > │   ├── build
-- > │   ├── even
-- > │   ├── fold
-- > │   ├── not
-- > │   ├── odd
-- > │   ├── or
-- > │   ├── package.dhall
-- > │   └── show
-- > ├── Double
-- > │   ├── package.dhall
-- > │   └── show
-- > ├── Function
-- > │   ├── compose
-- > │   └── package.dhall
-- > ├── Integer
-- > │   ├── package.dhall
-- > │   ├── show
-- > │   └── toDouble
-- > ├── JSON
-- > │   ├── Nesting
-- > │   ├── Tagged
-- > │   ├── Type
-- > │   ├── array
-- > │   ├── bool
-- > │   ├── keyText
-- > │   ├── keyValue
-- > │   ├── null
-- > │   ├── number
-- > │   ├── object
-- > │   ├── package.dhall
-- > │   ├── render
-- > │   └── string
-- > ├── List
-- > │   ├── all
-- > │   ├── any
-- > │   ├── build
-- > │   ├── concat
-- > │   ├── concatMap
-- > │   ├── default
-- > │   ├── empty
-- > │   ├── filter
-- > │   ├── fold
-- > │   ├── generate
-- > │   ├── head
-- > │   ├── indexed
-- > │   ├── iterate
-- > │   ├── last
-- > │   ├── length
-- > │   ├── map
-- > │   ├── null
-- > │   ├── package.dhall
-- > │   ├── replicate
-- > │   ├── reverse
-- > │   ├── shifted
-- > │   └── unzip
-- > ├── Location
-- > │   ├── Type
-- > │   └── package.dhall
-- > ├── Map
-- > │   ├── Entry
-- > │   ├── Type
-- > │   ├── empty
-- > │   ├── keyText
-- > │   ├── keyValue
-- > │   ├── keys
-- > │   ├── map
-- > │   ├── package.dhall
-- > │   └── values
-- > ├── Monoid
-- > ├── Natural
-- > │   ├── build
-- > │   ├── enumerate
-- > │   ├── equal
-- > │   ├── even
-- > │   ├── fold
-- > │   ├── greaterThan
-- > │   ├── greaterThanEqual
-- > │   ├── isZero
-- > │   ├── lessThan
-- > │   ├── lessThanEqual
-- > │   ├── odd
-- > │   ├── package.dhall
-- > │   ├── product
-- > │   ├── show
-- > │   ├── subtract
-- > │   ├── sum
-- > │   ├── toDouble
-- > │   └── toInteger
-- > ├── Optional
-- > │   ├── all
-- > │   ├── any
-- > │   ├── build
-- > │   ├── concat
-- > │   ├── default
-- > │   ├── filter
-- > │   ├── fold
-- > │   ├── head
-- > │   ├── last
-- > │   ├── length
-- > │   ├── map
-- > │   ├── null
-- > │   ├── package.dhall
-- > │   ├── toList
-- > │   └── unzip
-- > ├── Text
-- > │   ├── concat
-- > │   ├── concatMap
-- > │   ├── concatMapSep
-- > │   ├── concatSep
-- > │   ├── default
-- > │   ├── defaultMap
-- > │   ├── package.dhall
-- > │   └── show
-- > ├── XML
-- > │   ├── Type
-- > │   ├── attribute
-- > │   ├── element
-- > │   ├── emptyAttributes
-- > │   ├── leaf
-- > │   ├── package.dhall
-- > │   ├── render
-- > │   └── text
-- > └── package.dhall
--
-- Browse the Prelude online to learn more by seeing what functions are
-- available and reading their inline documentation:
--
-- <https://prelude.dhall-lang.org>
--
-- __Exercise__: Try to use a new Prelude function that has not been covered
-- previously in this tutorial
--
-- You can also import the entire Prelude as a single large record for
-- convenience:
--
-- > $ dhall
-- > let Prelude = https://prelude.dhall-lang.org/package.dhall
-- >
-- > in  \(x : Text) ->
-- >       Prelude.List.length Text (Prelude.List.replicate 10 Text x)
-- > <Ctrl-D>
-- > ∀(x : Text) → Natural
-- >
-- > λ(x : Text) → 10
--
-- The organization of the package mirrors the layout of the Prelude, meaning
-- that every directory is stored as a record whose children are the fields of
-- that record.
--
-- __Exercise__: Browse the Prelude by running:
--
-- > $ dhall <<< 'https://prelude.dhall-lang.org/package.dhall'

-- $limitations
-- #limitations#
--
-- `FromDhall` has a limitiation: It won't work for recursive types.
-- If you instantiate these using their Generic instance you end up with one of
-- the following two cases:
--
-- If the type appears in it's own definition like
--
-- > data Foo = Foo Foo
-- >     deriving Generic
-- >
-- > instance FromDhall Foo
--
-- the resulting Decoder will throw an exception /ON USAGE/.
-- However, if the recursion is indirect like
--
-- > data Foo = Foo Bar
-- >     deriving Generic
-- >
-- > instance FromDhall Foo
-- >
-- > data Bar = Bar Foo
-- >     deriving Generic
-- >
-- > instance FromDhall Bar
--
-- the resulting Decoder will __NOT TERMINATE__ /ON USAGE/.

-- $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>
--
-- Also, you might want to check out the
-- <https://docs.dhall-lang.org/tutorials/Language-Tour.html Language Tour>, a
-- more comprehensive tour of Dhall which may cover features missing from this
-- Haskell tutorial.
--
-- You can also request features, support, or documentation improvements on the
-- above issue tracker.
--
-- If you would like to contribute to the Dhall project you can try to port
-- Dhall to languages that do not yet have Dhall integrations so that Dhall configuration files
-- can be read into those languages, too.

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