{-# 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 -- * 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" -- -- Every @let@ expression of the form: -- -- > let x : t = y in e -- -- ... is exactly equivalent to: -- -- > (λ(x : t) → e) y -- -- So for example, this @let@ expression: -- -- > let x : Text = "ha" in x ++ x -- -- ... is equivalent to: -- -- > (λ(x : Text) → x ++ x) "ha" -- -- ... which in turn reduces to: -- -- > "ha" ++ "ha" -- -- ... which in turn reduces to: -- -- > "haha" -- -- You need to nest @let@ expressions if you want to define more than one value -- in this way: -- -- > $ dhall -- > let x = "Hello, " -- > in let y = "world!" -- > in x ++ y -- > <Ctrl-D> -- > Text -- > -- > "Hello, world!" -- -- Dhall is whitespace-insensitive, so feel free to format things over multiple -- lines or indent in any way that you please. -- -- If you want to define a named function, just give a name to an anonymous -- function: -- -- > $ dhall -- > let twice = λ(x : Text) → x ++ x in twice "ha" -- > <Ctrl-D> -- > Text -- > -- > "haha" -- -- Unlike Haskell, Dhall does not support function arguments on the left-hand -- side of the equals sign, so this will not work: -- -- > $ dhall -- > let twice (x : Text) = x ++ x in twice "ha" -- > <Ctrl-D> -- > (stdin):1:11: error: expected: ":", -- > "=" -- > let twice (x : Text) = x ++ x in twice "ha" -- > ^ -- -- The error message says that Dhall expected either a @(:)@ (i.e. the beginning -- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a -- function argument. -- -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall -- > let not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not -- > in not True -- > <Ctrl-D> -- > Bool -- > -- > False -- -- __Exercise:__ What do you think the following code will normalize to? -- -- > let x = 1 -- > in let x = 2 -- > in x -- -- Test your guess using the @dhall@ compiler -- -- __Exercise:__ Now try to guess what this code will normalize to: -- -- > let x = "ha" -- > in let x = x ++ "ha" -- > in x -- -- __Exercise:__ What about this code? -- -- > let x = x ++ "ha" -- > in x -- $unions -- -- A union is a value that can be one of many alternative types of values. For -- example, the following union type: -- -- > < Left : Natural | Right : Bool > -- -- ... represents a value that can be either a @Natural@ or a @Bool@ value. If -- you are familiar with Haskell these are exactly analogous to Haskell's -- \"sum types\". -- -- Each alternative is associated with a tag that distinguishes that alternative -- from other alternatives. In the above example, the @Left@ tag is used for -- the @Natural@ alternative and the @Right@ tag is used for the @Bool@ -- alternative. -- -- A union literal specifies the value of one alternative and the types of the -- remaining alternatives. For example, both of the following union literals -- have the same type, which is the above union type: -- -- > < Left = +0 | Right : Bool > -- -- > < Right = True | Left : Natural > -- -- You can consume a union using the built-in @merge@ function. For example, -- suppose we want to convert our union to a @Bool@ but we want to behave -- differently depending on whether or not the union is a @Natural@ wrapped in -- the @Left@ alternative or a @Bool@ wrapped in the @Right@ alternative. We -- would write: -- -- > $ cat > process <<EOF -- > λ(union : < Left : Natural | Right : Bool >) -- > → let handlers = -- > { Left = Natural/even -- Natural/even is a built-in function -- > , Right = λ(b : Bool) → b -- > } -- > in merge handlers union : Bool -- > EOF -- -- Now our @./process@ function can handle both alternatives: -- -- > $ dhall -- > ./process < Left = +3 | Right : Bool > -- > <Ctrl-D> -- > Bool -- > -- > False -- -- > $ dhall -- > ./process < Right = True | Left : Natural > -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Every @merge@ has the following form: -- -- > merge handlers union : type -- -- ... where: -- -- * @union@ is the union you want to consume -- * @handlers@ is a record with one function per alternative of the union -- * @type@ is the declared result type of the @merge@ -- -- The @merge@ function selects which function to apply from the record based on -- which alternative the union selects: -- -- > merge { Foo = f, ... } < Foo = x | ... > : t = f x : t -- -- So, for example: -- -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool -- > = Natural/even +3 : Bool -- > = False -- -- ... and similarly: -- -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > : Bool -- > = (λ(b : Bool) → b) True : Bool -- > = True -- -- Notice that each handler has to return the same type of result (@Bool@ in -- this case) which must also match the declared result type of the @merge@. -- -- 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 > -- -- __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 List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map -- > in λ(f : Integer → Integer) → 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}" } ] -- -- 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. -- $builtins -- -- Dhall is a restricted programming language that only supports simple built-in -- functions and operators. If you want to do anything fancier you will need to -- load your data into Haskell for further processing -- -- This section covers types, functions, and operators that are built into the -- language, meaning that you do not need to import any code to use them. -- Additionally, Dhall also comes with a Prelude (covered in the next section) -- hosted online that contains functions derived from these base utilities. The -- Prelude also re-exports all built-in functions for people who prefer -- consistency. -- -- The following documentation on built-ins is provided primarily as a reference. -- You don't need to read about every single built-in and you may want to skip to -- the following Prelude section. -- The language provides built-in support for the following primitive types: -- -- * @Bool@ values -- * @Natural@ values -- * @Integer@ values -- * @Double@ values -- * @Text@ values -- -- ... as well as support for the following derived types: -- -- * @List@s of values -- * @Optional@ values -- * Anonymous records -- * Anonymous unions -- $caveats -- -- Dhall differs in a few important ways from other programming languages, so -- you should keep the following caveats in mind: -- -- First, Dhall only supports addition and multiplication on @Natural@ numbers -- (i.e. non-negative integers), which are not the same type of number as -- @Integer@s (which can be negative). A @Natural@ number is a number prefixed -- with the @+@ symbol. If you try to add or multiply two @Integer@s (without -- the @+@ prefix) you will get a type error: -- -- > $ dhall -- > 2 + 2 -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: ❰+❱ only works on ❰Natural❱s -- > -- > 2 + 2 -- > -- > (stdin):1:1 -- -- In fact, there are no built-in functions for @Integer@s (or @Double@s). As -- far as the language is concerned they are opaque values that can only be -- shuffled around but not used in any meaningful way until they have been -- loaded into Haskell. -- -- Second, the equality @(==)@ and inequality @(!=)@ operators only work on -- @Bool@s. You cannot test any other types of values for equality. -- $builtinOverview -- -- Each of the following sections provides an overview of builtin functions and -- operators for each type. For each function you get: -- -- * An example use of that function -- -- * A \"type judgement\" explaining when that function or operator is well -- typed -- -- For example, for the following judgement: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x && y : Bool -- -- ... you can read that as saying: "if @x@ has type @Bool@ and @y@ has type -- @Bool@, then @x && y@ has type @Bool@" -- -- Similarly, for the following judgement: -- -- > ───────────────────────────────── -- > Γ ⊢ Natural/even : Natural → Bool -- -- ... you can read that as saying: "@Natural/even@ always has type -- @Natural → Bool@" -- -- * Rules for how that function or operator behaves -- -- These rules are just equalities that come in handy when reasoning about code. -- For example, the section on @(&&)@ has the following rules: -- -- > (x && y) && z = x && (y && z) -- > -- > x && True = x -- > -- > True && x = x -- -- These rules are also a contract for how the compiler should behave. If you -- ever observe code that does not obey these rules you should file a bug -- report. -- $bool -- -- There are two values that have type @Bool@ named @True@ and @False@: -- -- > ─────────────── -- > Γ ⊢ True : Bool -- -- > ──────────────── -- > Γ ⊢ False : Bool -- -- The built-in operations for values of type @Bool@ are: -- -- $or -- -- Example: -- -- > $ dhall -- > True || False -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x || y : Bool -- -- Rules: -- -- > (x || y) || z = x || (y || z) -- > -- > x || False = x -- > -- > False || x = x -- > -- > x || (y && z) = (x || y) && (x || z) -- > -- > x || True = True -- > -- > True || x = True -- $and -- -- Example: -- -- > $ dhall -- > True && False -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x && y : Bool -- -- Rules: -- -- > (x && y) && z = x && (y && z) -- > -- > x && True = x -- > -- > True && x = x -- > -- > x && (y || z) = (x && y) || (x && z) -- > -- > x && False = False -- > -- > False && x = False -- $equal -- -- Example: -- -- > $ dhall -- > True == False -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x == y : Bool -- -- Rules: -- -- > (x == y) == z = x == (y == z) -- > -- > x == True = x -- > -- > True == x = x -- > -- > x == x = True -- $unequal -- -- Example: -- -- > $ dhall -- > True != False -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x != y : Bool -- -- Rules: -- -- > (x != y) != z = x != (y != z) -- > -- > x != False = x -- > -- > False != x = x -- > -- > x != x = False -- $ifthenelse -- -- Example: -- -- > $ dhall -- > if True then 3 else 5 -- > <Ctrl-D> -- > Integer -- > -- > 3 -- -- Type: -- -- > Γ ⊢ t : Type -- > ───────────────────── -- > Γ ⊢ b : Bool Γ ⊢ l : t Γ ⊢ r : t -- > ──────────────────────────────────── -- > Γ ⊢ if b then l else r -- -- Rules: -- -- > if b then True else False = b -- > -- > if True then l else r = l -- > -- > if False then l else r = r -- $natural -- -- @Natural@ literals are numbers prefixed by a @+@ sign, like this: -- -- > +4 : Natural -- -- If you omit the @+@ sign then you get an @Integer@ literal, which is a -- different type of value -- $plus -- -- Example: -- -- > $ dhall -- > +2 + +3 -- > <Ctrl-D> -- > Natural -- > -- > +5 -- -- Type: -- -- > Γ ⊢ x : Natural Γ ⊢ y : Natural -- > ───────────────────────────────── -- > Γ ⊢ x + y : Natural -- -- Rules: -- -- > (x + y) + z = x + (y + z) -- > -- > x + +0 = x -- > -- > +0 + x = x -- $times -- -- Example: -- -- > $ dhall -- > +2 * +3 -- > <Ctrl-D> -- > Natural -- > -- > +6 -- -- Type: -- -- > Γ ⊢ x : Natural Γ ⊢ y : Natural -- > ───────────────────────────────── -- > Γ ⊢ x * y : Natural -- -- Rules: -- -- > (x * y) * z = x * (y * z) -- > -- > x * +1 = x -- > -- > +1 * x = x -- > -- > (x + y) * z = (x * z) + (y * z) -- > -- > x * (y + z) = (x * y) + (x * z) -- > -- > x * +0 = +0 -- > -- > +0 * x = +0 -- $even -- -- Example: -- -- > $ dhall -- > Natural/even +6 -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > ───────────────────────────────── -- > Γ ⊢ Natural/even : Natural → Bool -- -- Rules: -- -- > Natural/even (x + y) = Natural/even x == Natural/even y -- > -- > Natural/even +0 = True -- > -- > Natural/even (x * y) = Natural/even x || Natural/even y -- > -- > Natural/even +1 = False -- $odd -- -- Example: -- -- > $ dhall -- > Natural/odd +6 -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > ──────────────────────────────── -- > Γ ⊢ Natural/odd : Natural → Bool -- -- Rules: -- -- > Natural/odd (x + y) = Natural/odd x != Natural/odd y -- > -- > Natural/odd +0 = False -- > -- > Natural/odd (x * y) = Natural/odd x && Natural/odd y -- > -- > Natural/odd +1 = True -- $isZero -- -- Example: -- -- > $ dhall -- > Natural/isZero +6 -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > ─────────────────────────────────── -- > Γ ⊢ Natural/isZero : Natural → Bool -- -- Rules: -- -- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y -- > -- > Natural/isZero +0 = True -- > -- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y -- > -- > Natural/isZero +1 = False -- $naturalFold -- -- Example: -- -- > $ dhall -- > Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome" -- > <Ctrl-D> -- > Text -- > -- > "You're welcome!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!" -- -- Type: -- -- > ────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ Natural/fold : Natural → ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural -- -- Rules: -- -- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z) -- > -- > Natural/fold +0 n s z = z -- > -- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s) -- > -- > Natural/fold 1 n s = s -- $naturalBuild -- -- Example: -- -- > $ dhall -- > Natural/build (λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ zero)) -- > <Ctrl-D> -- > Natural -- > -- > +2 -- -- Type: -- -- > ───────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ Natural/build : (∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural) → Natural -- -- Rules: -- -- > Natural/fold (Natural/build x) = x -- > -- > Natural/build (Natural/fold x) = x -- $integer -- -- @Integer@ literals are either prefixed with a @-@ sign (if they are negative) -- or no sign (if they are positive), like this: -- -- > 3 : Integer -- > -2 : Integer -- -- If you prefix them with a @+@ sign then they are @Natural@ literals and not -- @Integer@s -- -- There are no built-in operations on @Integer@s. For all practical purposes -- they are opaque values within the Dhall language -- $double -- -- A @Double@ literal is a floating point value with at least one decimal -- place, such as: -- -- > -2.0 : Double -- > 3.14159 : Double -- -- There are no built-in operations on @Double@s. For all practical purposes -- they are opaque values within the Dhall language -- $text -- -- A @Text@ literal is just a sequence of characters enclosed in double quotes, -- like: -- -- > "ABC" : Text -- -- The only thing you can do with @Text@ values is concatenate them -- $textAppend -- -- Example: -- -- > $ dhall -- > "Hello, " ++ "world!" -- > <Ctrl-D> -- > Text -- > -- > "Hello, world!" -- -- Type: -- -- > Γ ⊢ x : Text Γ ⊢ y : Text -- > ─────────────────────────── -- > Γ ⊢ x && y : Text -- -- Rules: -- -- > (x ++ y) ++ z = x ++ (y ++ z) -- > -- > x ++ "" = x -- > -- > "" ++ x = x -- $list -- -- Dhall @List@ literals are a sequence of values inside of brackets separated by -- commas: -- -- > Γ ⊢ t : Type Γ ⊢ x : t Γ ⊢ y : t ... -- > ────────────────────────────────────────── -- > Γ ⊢ [x, y, ... ] : List t -- -- Also, every @List@ must end with a mandatory type annotation -- -- The built-in operations on @List@s are: -- $listAppend -- -- Example: -- -- > $ dhall -- > [1, 2, 3] # [5, 6, 7] -- > <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 List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat -- > -- > List/fold a (List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) -- > -- > List/fold a ([] : List a) b c n = n -- > -- > List/fold a ([x] : List a) b c = c x -- $listBuild -- -- Example: -- -- > $ dhall -- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil))) -- > <Ctrl-D> -- > List Integer -- > -- > [1, 2, 3] : List Integer -- -- Type: -- -- > ─────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ List/build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a -- -- Rules: -- -- > List/build t (List/fold t x) = x -- > -- > List/fold t (List/build t x) = x -- $listLength -- -- Example: -- -- > $ dhall -- > List/length Integer [1, 2, 3] -- > <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 Optional/head = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/head -- > let List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat -- > let List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap -- > let List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map -- > -- > List/head a (List/concat a xss) = -- > Optional/head a (List/map (List a) (Optional a) (List/head a) xss) -- > -- > List/head a ([x] : List a) = [x] : Optional a -- > -- > List/head b (List/concatMap a b f m) -- > = Optional/concatMap a b (λ(x : a) → List/head b (f x)) (List/head a m) -- $listLast -- -- Example: -- -- > $ dhall -- > List/last Integer [1, 2, 3] -- > <Ctrl-D> -- > Optional Integer -- > -- > [1] : Optional Integer -- -- Type: -- -- > ───────────────────────────────────── -- > Γ ⊢ List/last : ∀(a : Type) → List a → Optional a -- -- Rules: -- -- > let Optional/last = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/last -- > let List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat -- > let List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap -- > let List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map -- > -- > List/last a (List/concat a xss) = -- > Optional/last a (List/map (List a) (Optional a) (List/last a) xss) -- > -- > List/last a ([x] : List a) = [x] : Optional a -- > -- > List/last b (List/concatMap a b f m) -- > = Optional/concatMap a b (λ(x : a) → List/last b (f x)) (List/last a m) -- $listIndexed -- -- Example -- -- > $ dhall -- > List/indexed Text ["ABC", "DEF", "GHI"] -- > <Ctrl-D> -- > List { index : Natural, value : Text } -- > -- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text } -- -- Type: -- -- > ───────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a } -- -- Rules: -- -- > let List/shifted = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/shifted -- > let List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat -- > let List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map -- > -- > List/indexed a (List/concat a xss) = -- > List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) -- $listReverse -- -- Example: -- -- > $ dhall -- > List/reverse Integer [1, 2, 3] -- > <Ctrl-D> -- > List Integer -- > -- > [3, 2, 1] : List Integer -- -- Type: -- -- > ───────────────────────────────────────────────── -- > Γ ⊢ List/reverse : ∀(a : Type) → List a → List a -- -- Rules: -- -- > let List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map -- > let List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat -- > let List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap -- > -- > List/reverse a (List/concat a xss) -- > = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss)) -- > -- > List/reverse a ([x] : List a) = [x] : List a -- > -- > List/reverse b (List/concatMap a b f xs) -- > = List/concatMap a b (λ(x : a) → List/reverse b (f x)) (List/reverse a xs) -- > -- > List/reverse a ([x, y] : List a) = [y, x] : List a -- $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: -- -- <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/Gabriel439/Haskell-Dhall-Library/issues> -- -- You can also request features, support, or documentation improvements on the -- above issue tracker. -- -- If you would like to contribute to the Dhall project you can try to port Dhall -- to other languages besides Haskell so that Dhall configuration files can be -- read into those languages, too. -- $faq -- -- * Why do 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.