{-# OPTIONS_GHC -fno-warn-unused-imports #-} {-| Dhall is a programming language specialized for configuration files. This module contains a tutorial explaning how to author configuration files using this language -} module Dhall.Tutorial ( -- * Introduction -- $introduction -- * Types -- $types -- * Imports -- $imports -- * Lists -- $lists -- * Optional values -- $optional0 -- * Records -- $records -- * Functions -- $functions -- * Compiler -- $compiler -- * Strings -- $strings -- * Combine -- $combine -- * Let expressions -- $let -- * Unions -- $unions -- * Polymorphic functions -- $polymorphic -- * Total -- $total -- * Headers -- $headers -- * Import integrity -- $integrity -- * Raw text -- $rawText -- * Formatting code -- $format -- * Built-in functions -- $builtins -- ** Caveats -- $caveats -- ** Extending the language -- $extending -- ** Overview -- $builtinOverview -- ** @Bool@ -- $bool -- *** @(||)@ -- $or -- *** @(&&)@ -- $and -- *** @(==)@ -- $equal -- *** @(!=)@ -- $unequal -- *** @if@\/@then@\/@else@ -- $ifthenelse -- ** @Natural@ -- $natural -- *** @(+)@ -- $plus -- *** @(*)@ -- $times -- *** @Natural/even@ -- $even -- *** @Natural/odd@ -- $odd -- *** @Natural/isZero@ -- $isZero -- *** @Natural/fold@ -- $naturalFold -- *** @Natural/build@ -- $naturalBuild -- ** @Integer@ -- $integer -- ** @Double@ -- $double -- ** @Text@ -- $text -- *** @(++)@ -- $textAppend -- ** @List@ -- $list -- *** @(#)@ -- $listAppend -- *** @List/fold@ -- $listFold -- *** @List/build@ -- $listBuild -- *** @List/length@ -- $listLength -- *** @List/head@ -- $listHead -- *** @List/last@ -- $listLast -- *** @List/indexed@ -- $listIndexed -- *** @List/reverse@ -- $listReverse -- ** @Optional@ -- $optional1 -- *** @Optional/fold@ -- $optionalFold -- * Prelude -- $prelude -- * Conclusion -- $conclusion -- * Frequently Asked Questions (FAQ) -- $faq ) where import Data.Vector (Vector) import Dhall -- $setup -- -- >>> :set -XOverloadedStrings -- $introduction -- -- The simplest way to use Dhall is to ignore the programming language features -- and use it as a strongly typed configuration format. For example, suppose -- that you create the following configuration file: -- -- > $ cat ./config -- > { foo = 1 -- > , bar = [3.0, 4.0, 5.0] -- > } -- -- You can read the above configuration file into Haskell using the following -- code: -- -- > -- example.hs -- > -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Dhall -- > -- > data Example = Example { foo :: Natural, bar :: Vector Double } -- > deriving (Generic, Show) -- > -- > instance Interpret Example -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config" -- > print (x :: Example) -- -- If you compile and run the above example, the program prints the corresponding -- Haskell record: -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]} -- -- You can also load some types directly into Haskell without having to define a -- record, like this: -- -- >>> :set -XOverloadedStrings -- >>> input auto "True" :: IO Bool -- True -- -- The `input` function can decode any value if we specify the value's expected -- `Type`: -- -- > input -- > :: Type a -- Expected type -- > -> Text -- Dhall program -- > -> IO a -- Decoded expression -- -- ... and we can either specify an explicit type like `bool`: -- -- > bool :: Type Bool -- > -- > input bool :: Text -> IO Bool -- > -- > input bool "True" :: IO Bool -- -- >>> input bool "True" -- True -- -- ... or we can use `auto` to let the compiler infer what type to decode from -- the expected return type: -- -- > auto :: Interpret a => Type a -- > -- > input auto :: Interpret a => Text -> IO a -- -- >>> input auto "True" :: IO Bool -- True -- -- You can see what types `auto` supports \"out-of-the-box\" by browsing the -- instances for the `Interpret` class. For example, the following instance -- says that we can directly decode any Dhall expression that evaluates to a -- @Bool@ into a Haskell `Bool`: -- -- > instance Interpret Bool -- -- ... which is why we could directly decode the string @\"True\"@ into the -- value `True`. -- -- There is also another instance that says that if we can decode a value of -- type @a@, then we can also decode a @List@ of values as a `Vector` of @a@s: -- -- > instance Interpret a => Interpret (Vector a) -- -- Therefore, since we can decode a @Bool@, we must also be able to decode a -- @List@ of @Bool@s, like this: -- -- >>> input auto "[True, False]" :: IO (Vector Bool) -- [True,False] -- -- We could also specify what type to decode by providing an explicit `Type` -- instead of using `auto` with a type annotation: -- -- >>> input (vector bool) "[True, False]" -- [True,False] -- -- __Exercise:__ Create a @./config@ file that the following program can decode: -- -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Dhall -- > -- > data Person = Person { age :: Natural, name :: Text } -- > deriving (Generic, Show) -- > -- > instance Interpret Person -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config" -- > print (x :: Person) -- -- __Exercise:__ Create a @./config@ file that the following program can decode: -- -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Data.Functor.Identity -- > import Dhall -- > -- > instance Interpret a => Interpret (Identity a) -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config" -- > print (x :: Identity Double) -- $types -- -- Suppose that we try to decode a value of the wrong type, like this: -- -- >>> input auto "1" :: IO Bool -- *** Exception: -- ...Error...: Expression doesn't match annotation -- ... -- - Bool -- + Natural -- ... -- 1: 1 : Bool -- ... -- (input):1:1 -- ... -- -- The interpreter complains because the string @\"1\"@ cannot be decoded into a -- Haskell value of type `Bool`. This part of the type error: -- -- > - Bool -- > + Natural -- -- ... means that the expected type was @Bool@ but the inferred type of the -- expression @1@ was @Natural@. -- -- The code excerpt from the above error message has two components: -- -- * the expression being type checked (i.e. @1@) -- * the expression's expected type (i.e. @Bool@) -- -- > Expression -- > ⇩ -- > 1 : Bool -- > ⇧ -- > Expected type -- -- The @(:)@ symbol is how Dhall annotates values with their expected types. -- This notation is equivalent to type annotations in Haskell using the @(::)@ -- symbol. Whenever you see: -- -- > x : t -- -- ... you should read that as \"we expect the expression @x@ to have type -- @t@\". However, we might be wrong and if our expected type does not match the -- expression's actual type then the type checker will complain. -- -- In this case, the expression @1@ does not have type @Bool@ so type checking -- fails with an exception. -- -- __Exercise:__ Load the Dhall library into @ghci@ and run these commands to get -- get a more detailed error message: -- -- > >>> import Dhall -- > >>> :set -XOverloadedStrings -- > >>> detailed (input auto "1") :: IO Bool -- > ... -- -- ... then read the entire error message -- -- __Exercise:__ Fix the type error, either by changing the value to decode or -- changing the expected type -- $imports -- -- You might wonder why in some cases we can decode a configuration file: -- -- >>> writeFile "bool" "True" -- >>> input auto "./bool" :: IO Bool -- True -- -- ... and in other cases we can decode a value directly: -- -- >>> input auto "True" :: IO Bool -- True -- -- This is because importing a configuration from a file is a special case of a -- more general language feature: Dhall expressions can reference other -- expressions by their file path. -- -- To illustrate this, let's create three files: -- -- > $ echo "True" > bool1 -- > $ echo "False" > bool2 -- > $ echo "./bool1 && ./bool2" > both -- -- ... and read in all three files in a single expression: -- -- >>> input auto "[ ./bool1 , ./bool2 , ./both ]" :: IO (Vector Bool) -- [True,False,False] -- -- Each file path is replaced with the Dhall expression contained within that -- file. If that file contains references to other files then those references -- are transitively resolved. -- -- In other words: configuration files can reference other configuration files, -- either by their relative or absolute paths. This means that we can split a -- configuration file into multiple files, like this: -- -- > $ cat > ./config <<EOF -- > { foo = 1 -- > , bar = ./bar -- > } -- > EOF -- -- > $ echo "[3.0, 4.0, 5.0]" > ./bar -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]} -- -- However, the Dhall language will forbid cycles in these file references. For -- example, if we create the following cycle: -- -- > $ echo './file1' > file2 -- > $ echo './file2' > file1 -- -- ... then the interpreter will reject the import: -- -- >>> input auto "./file1" :: IO Natural -- *** Exception: -- ↳ ./file1 -- ↳ ./file2 -- ... -- Cyclic import: ./file1 -- ... -- -- You can also import expressions by URL. For example, you can find a Dhall -- expression hosted at this GitHub URL: -- -- <https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True> -- -- > $ curl https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True -- > True -- -- ... and you can reference that expression either directly: -- -- >>> input auto "https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- True -- -- ... or inside of a larger expression: -- -- >>> input auto "False == https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- False -- -- You're not limited to hosting Dhall expressions on GitHub. You can host a -- Dhall expression anywhere that you can host UTF8-encoded text on the web, -- as a pastebin, or your own web server. -- -- You can also import Dhall expressions from environment variables, too: -- -- >>> System.Environment.setEnv "FOO" "1" -- >>> input auto "env:FOO" :: IO Natural -- 1 -- -- You can import types, too. For example, we can change our @./bar@ file to: -- -- > $ echo "[3.0, 4.0, 5.0] : List ./type" > ./bar -- -- ... then specify the @./type@ in a separate file: -- -- > $ echo "Double" > ./type -- -- ... and everything still type checks: -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]} -- -- Note that all imports must be terminated by whitespace or you will get either -- an import error or a parse error, like this: -- -- >>> writeFile "baz" "2.0" -- >>> input auto "./baz: Double" :: IO Double -- *** Exception: -- ↳ ./baz: -- ... -- ...Error...: Missing file ...baz: -- ... -- -- This is because the parser thinks that @./baz:@ is a single token due to -- the missing whitespace before the colon and tries to import a file named -- @./baz:@, which does not exist. To fix the problem we have to add a space -- after @./baz@: -- -- >>> input auto "./baz : Double" :: IO Double -- 2.0 -- -- __Exercise:__ There is a @not@ function hosted online here: -- -- <https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not> -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- -- > >>> input auto "https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- > ??? -- -- Run the code to test your guess -- $lists -- -- You can store 0 or more values of the same type in a list, like this: -- -- > [1, 2, 3] -- -- Every list can be followed by the type of the list. The type annotation is -- required for empty lists but optional for non-empty lists. You will get a -- type error if you provide an empty list without a type annotation: -- -- >>> input auto "[]" :: IO (Vector Natural) -- *** Exception: -- ...Error...: An empty list requires a type annotation -- ... -- 1: [] -- ... -- (input):1:1 -- -- Also, list elements must all have the same type. You will get an error if -- you try to store elements of different types in a list: -- -- >>> input auto "[1, True, 3]" :: IO (Vector Natural) -- *** Exception: -- ...Error...: List elements should all have the same type -- ... -- - Natural -- + Bool -- ... -- 1: True -- ... -- (input):1:5 -- ... -- -- __Exercise:__ What is the shortest @./config@ file that you can decode using -- this command: -- -- > >>> input auto "./config" :: IO (Vector (Vector Natural)) -- $optional0 -- -- @Optional@ values are either of the form @Some aValue@ or @None aType@. -- -- For example, these are valid @Optional@ values: -- -- > Some 1 -- > -- > None Natural -- -- ... which both have type @Optional Natural@ -- -- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes: -- -- >>> input auto "Some 1" :: IO (Maybe Natural) -- Just 1 -- >>> input auto "None Natural" :: IO (Maybe Natural) -- Nothing -- -- __Exercise:__ Author a @./config@ file that you can decode like this: -- -- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Natural))) -- > ??? -- $records -- -- Record literals are delimited by curly braces and their fields are separated -- by commas. For example, this is a valid record literal: -- -- > { foo = True -- > , bar = 2 -- > , baz = 4.2 -- > } -- -- A record type is like a record literal except instead of specifying each -- field's value we specify each field's type. For example, the preceding -- record literal has the following record type: -- -- > { foo : Bool -- > , bar : Natural -- > , baz : Double -- > } -- -- If you want to specify an empty record literal, you must use @{=}@, which is -- special syntax reserved for empty records. If you want to specify the empty -- record type, then you use @{}@. If you forget which is which you can always -- ask the @dhall@ compiler to remind you of the type for each one: -- -- > $ dhall -- > {=} -- > <Ctrl-D> -- > {} -- > -- > {=} -- -- > $ dhall -- > {} -- > <Ctrl-D> -- > Type -- > -- > {} -- -- You can access a field of a record using the following syntax: -- -- > record.fieldName -- -- ... which means to access the value of the field named @fieldName@ from the -- @record@. For example: -- -- >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double -- 4.2 -- -- ... and you can project out multiple fields into a new record using this -- syntax: -- -- > someRecord.{ field₀, field₁, … } -- -- For example: -- -- > $ dhall -- > { x = 1, y = True, z = "ABC" }.{ x, y } -- > <Ctrl-D> -- > { x : Natural, y : Bool } -- > -- > { x = 1, y = True } -- -- __Exercise__: What is the type of this record: -- -- > { foo = 1 -- > , bar = -- > { baz = 2.0 -- > , qux = True -- > } -- > } -- -- __Exercise__: Save the above code to a file named @./record@ and then try to -- access the value of the @baz@ field -- $functions -- -- The Dhall programming language also supports user-defined anonymous -- functions. For example, we can save the following anonymous function to a -- file: -- -- > $ cat > makeBools -- > \(n : Bool) -> -- > [ n && True, n && False, n || True, n || False ] -- > <Ctrl-D> -- -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB) -- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into that -- sort of thing): -- -- > $ cat > makeBools -- > λ(n : Bool) → -- > [ n && True, n && False, n || True, n || False ] -- > <Ctrl-D> -- -- You can read this as a function of one argument named @n@ that has type -- @Bool@. This function returns a @List@ of @Bool@s. Each element of the -- @List@ depends on the input argument named @n@. -- -- The (ASCII) syntax for anonymous functions resembles the syntax for anonymous -- functions in Haskell. The only difference is that Dhall requires you to -- annotate the type of the function's input. -- -- You can import this function into Haskell, too: -- -- >>> makeBools <- input auto "./makeBools" :: IO (Bool -> Vector Bool) -- >>> makeBools True -- [True,False,True,True] -- -- The reason this works is that there is an `Interpret` instance for simple -- functions: -- -- > instance (Inject a, Interpret b) => Interpret (a -> b) -- -- Thanks to currying, this instance works for functions of multiple simple -- arguments: -- -- >>> dhallAnd <- input auto "λ(x : Bool) → λ(y : Bool) → x && y" :: IO (Bool -> Bool -> Bool) -- >>> dhallAnd True False -- False -- -- However, you can't convert anything more complex than that (like a polymorphic -- or higher-order function). You will need to apply those functions to their -- arguments within Dhall before converting their result to a Haskell value. -- -- Just like `Interpret`, you can derive `Inject` for user-defined data types: -- -- > {-# LANGUAGE DeriveAnyClass #-} -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > module Main where -- > -- > import Dhall -- > -- > data Example0 = Example0 { foo :: Bool, bar :: Bool } -- > deriving (Generic, Inject) -- > -- > main = do -- > f <- input auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" -- > print (f (Example0 { foo = True, bar = False }) :: Bool) -- > print (f (Example0 { foo = True, bar = True }) :: Bool) -- -- The above program prints: -- -- > False -- > True -- $compiler -- -- We can also test our @makeBools@ function directly from the command line. -- This library comes with a command-line executable program named @dhall@ that -- you can use to both type-check files and convert them to a normal form. Our -- compiler takes a program on standard input and then prints the program's type -- to standard error followed by the program's normal form to standard output: -- -- > $ dhall -- > ./makeBools -- > <Ctrl-D> -- > ∀(n : Bool) → List Bool -- > -- > λ(n : Bool) → [ n, False, True, n ] -- -- The first line says that @makeBools@ is a function of one argument named @n@ -- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@ -- (U+2200) symbol is shorthand for the ASCII @forall@ keyword: -- -- > ∀(x : a) → b -- This type ... -- > -- > forall (x : a) → b -- ... is the same as this type -- -- ... and Dhall's @forall@ keyword behaves the same way as Haskell's @forall@ -- keyword for input values that are @Type@s: -- -- > forall (x : Type) → b -- This Dhall type ... -- -- > forall x . b -- ... is the same as this Haskell type -- -- The part where Dhall differs from Haskell is that you can also use -- @∀@/@forall@ to give names to non-@Type@ arguments (such as the first -- argument to @makeBools@). -- -- The second line of Dhall's output is our program's normal form: -- -- > λ(n : Bool) → [ n, False, True, n ] -- -- ... and the interpreter was able to simplify our expression by noting that: -- -- * @n && True = n@ -- * @n && False = False@ -- * @n || True = True@ -- * @n || False = n@ -- -- To apply a function to an argument you separate the function and argument by -- whitespace (just like Haskell): -- -- @f x@ -- -- You can read the above as \"apply the function @f@ to the argument @x@\". This -- means that we can \"apply\" our @./makeBools@ function to a @Bool@ argument -- like this: -- -- > $ dhall -- > ./makeBools True -- > <Ctrl-D> -- > List Bool -- > -- > [True, False, True, True] -- -- Remember that file paths are synonymous with their contents, so the above -- code is exactly equivalent to: -- -- > $ dhall -- > (λ(n : Bool) → [n && True, n && False, n || True, n || False]) True -- > <Ctrl-D> -- > List Bool -- > -- > [True, False, True, True] -- -- When you apply an anonymous function to an argument, you substitute the -- \"bound variable" with the function's argument: -- -- > Bound variable -- > ⇩ -- > (λ(n : Bool) → ...) True -- > ⇧ -- > Function argument -- -- So in our above example, we would replace all occurrences of @n@ with @True@, -- like this: -- -- > -- If we replace all of these `n`s with `True` ... -- > [n && True, n && False, n || True, n || False] -- > -- > -- ... then we get this: -- > [True && True, True && False, True || True, True || False] -- > -- > -- ... which reduces to the following normal form: -- > [True, False, True, True] -- -- Now that we've verified that our function type checks and works, we can use -- the same function within Haskell: -- -- >>> input auto "./makeBools True" :: IO (Vector Bool) -- [True,False,True,True] -- -- __Exercise__: Create a file named @getFoo@ that is a function of the following -- type: -- -- > ∀(r : { foo : Bool, bar : Text }) → Bool -- -- This function should take a single input argument named @r@ that is a record -- with two fields. The function should return the value of the @foo@ field. -- -- __Exercise__: Use the @dhall@ compiler to infer the type of the function you -- just created and verify that your function has the correct type -- -- __Exercise__: Use the @dhall@ compiler to apply your function to a sample -- record -- $strings -- Dhall supports ordinary string literals with Haskell-style escaping rules: -- -- > dhall -- > "Hello, \"world\"!" -- > <Ctrl-D> -- > Text -- > -- > "Hello, \"world\"!" -- -- ... and Dhall also supports Nix-style multi-line string literals: -- -- > dhall -- > '' -- > #!/bin/bash -- > -- > echo "Hi!" -- > '' -- > <Ctrl-D> -- > Text -- > -- > "\n#!/bin/bash\n\necho \"Hi!\"\n" -- -- These \"double single quote strings\" ignore all special characters, with one -- exception: if you want to include a @''@ in the string, you will need to -- escape it with a preceding @'@ (i.e. use @'''@ to insert @''@ into the final -- string). -- -- These strings also strip leading whitespace using the same rules as Nix. -- Specifically: \"it strips from each line a number of spaces equal to the -- minimal indentation of the string as a whole (disregarding the indentation -- of empty lines).\" -- -- You can also interpolate expressions into strings using @${...}@ syntax. For -- example: -- -- > $ dhall -- > let name = "John Doe" -- > in let age = 21 -- > in "My name is ${name} and my age is ${Natural/show age}" -- > <Ctrl-D> -- > Text -- > -- > "My name is John Doe and my age is 21" -- -- Note that you can only interpolate expressions of type @Text@ -- -- If you need to insert a @"${"@ into a string without interpolation then use -- @"''${"@ (same as Nix) -- -- > '' -- > for file in *; do -- > echo "Found ''${file}" -- > done -- > '' -- $combine -- -- You can combine two records, using either the @(//)@ operator or the -- @(/\\)@ operator. -- -- The @(//)@ operator (or @(⫽)@ U+2AFD) combines the fields of both records, -- preferring fields from the right record if they share fields in common: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } // { baz = True } -- > <Ctrl-D> -- > { bar : Text, baz : Bool, foo : Natural } -- > -- > { bar = "ABC", baz = True, foo = 1 } -- > $ dhall -- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode -- > <Ctrl-D> -- > { bar : Bool, foo : Natural } -- > -- > { bar = True, foo = 1 } -- -- Note that the order of record fields does not matter. The compiler -- automatically sorts the fields. -- -- The @(/\\)@ operator (or @(∧)@ U+2227) also lets you combine records, but -- behaves differently if the records share fields in common. The operator -- combines shared fields recursively if they are both records: -- -- > $ dhall -- > { foo = { bar = True }, baz = "ABC" } /\ { foo = { qux = 1.0 } } -- > <Ctrl-D> -- > { baz : Text, foo : { bar : Bool, qux : Double } } -- > -- > { baz = "ABC", foo = { bar = True, qux = 1.0 } } -- -- ... but fails with a type error if either shared field is not a record: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } ∧ { foo = True } -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: Field collision -- > -- > { foo = 1, bar = "ABC" } ∧ { foo = True } -- > -- > (stdin):1:1 -- -- __Exercise__: Combine any record with the empty record. What do you expect -- to happen? -- -- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53): -- -- > $ dhall -- > { foo : Natural } ⩓ { bar : Text } -- > <Ctrl-D> -- > { foo : Natural, bar : Text } -- -- ... which behaves the exact same, except at the type level, meaning that the -- operator descends recursively into record types: -- -- > $ dhall -- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural } -- > <Ctrl-D> -- > { foo : { bar : Text, baz : Bool }, qux : Natural } -- $let -- -- Dhall also supports @let@ expressions, which you can use to define -- intermediate values in the course of a computation, like this: -- -- > $ dhall -- > let x = "ha" in x ++ x -- > <Ctrl-D> -- > Text -- > -- > "haha" -- -- You can also annotate the types of values defined within a @let@ expression, -- like this: -- -- > $ dhall -- > let x : Text = "ha" in x ++ x -- > <Ctrl-D> -- > Text -- > -- > "haha" -- -- You need to nest @let@ expressions if you want to define more than one value -- in this way: -- -- > $ dhall -- > let x = "Hello, " -- > in let y = "world!" -- > in x ++ y -- > <Ctrl-D> -- > Text -- > -- > "Hello, world!" -- -- Dhall is whitespace-insensitive, so feel free to format things over multiple -- lines or indent in any way that you please. -- -- If you want to define a named function, just give a name to an anonymous -- function: -- -- > $ dhall -- > let twice = λ(x : Text) → x ++ x in twice "ha" -- > <Ctrl-D> -- > Text -- > -- > "haha" -- -- Unlike Haskell, Dhall does not support function arguments on the left-hand -- side of the equals sign, so this will not work: -- -- > $ dhall -- > let twice (x : Text) = x ++ x in twice "ha" -- > <Ctrl-D> -- > Error: Invalid input -- > -- > (stdin):1:11: -- > | -- > 1 | let twice (x : Text) = x ++ x in twice "ha" -- > | ^ -- > unexpected '(' -- > expecting ':', '=', or the rest of label -- -- The error message says that Dhall expected either a @(:)@ (i.e. the beginning -- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a -- function argument. -- -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall -- > let not = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not -- > in not True -- > <Ctrl-D> -- > Bool -- > -- > False -- -- ... or to define synonyms for types: -- -- > $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name' -- > List Text -- > -- > [ "John", "Mary" ] -- -- __Exercise:__ What do you think the following code will normalize to? -- -- > let x = 1 -- > in let x = 2 -- > in x -- -- Test your guess using the @dhall@ compiler -- -- __Exercise:__ Now try to guess what this code will normalize to: -- -- > let x = "ha" -- > in let x = x ++ "ha" -- > in x -- -- __Exercise:__ What about this code? -- -- > let x = x ++ "ha" -- > in x -- $unions -- -- A union is a value that can be one of many alternative types of values. For -- example, the following union type: -- -- > < Left : Natural | Right : Bool > -- -- ... represents a value that can be either a @Natural@ or a @Bool@ value. If -- you are familiar with Haskell these are exactly analogous to Haskell's -- \"sum types\". -- -- Each alternative is associated with a tag that distinguishes that alternative -- from other alternatives. In the above example, the @Left@ tag is used for -- the @Natural@ alternative and the @Right@ tag is used for the @Bool@ -- alternative. -- -- You can specify the value of a union constructor like this: -- -- > let Union = < Left : Natural | Right : Bool> -- > -- > [ Union.Left 0, Union.Right True ] : List Union -- -- 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 : Bool -- > 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 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) = 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 } > -- -- -- This union of records resembles following equivalent Haskell data type: -- -- > data Example = Empty | Person { name :: Text, age :: Text } -- -- Empty alternatives like @Empty@ require no argument: -- -- > let MyType = < Empty | Person : { name : Text, age : Natural } > -- > -- > in [ MyType.Empty -- Note the absence of any argument to `Empty` -- > , MyType.Person { name = "John", age = 23 } -- > , MyType.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 a `λ` -- > -- > , Person = -- > λ(person : { name : Text, age : Natural }) -- > → "Name: ${person.name}, Age: ${Natural/show person.age}" -- > } -- > x -- -- __Exercise__: Create a list of the following type with at least one element -- per alternative: -- -- > List < Left : Natural | Right : Double > -- $polymorphic -- -- The Dhall language supports defining polymorphic functions (a.k.a. -- \"generic\" functions) that work on more than one type of value. However, -- Dhall differs from Haskell by not inferring the types of these polymorphic -- functions. Instead, you must be explicit about what type of value the -- function is specialized to. -- -- Take, for example, Haskell's identity function named @id@: -- -- > id :: a -> a -- > id = \x -> x -- -- The identity function is polymorphic, meaning that `id` works on values of -- different types: -- -- >>> id 4 -- 4 -- >>> id True -- True -- -- The equivalent function in Dhall is: -- -- > λ(a : Type) → λ(x : a) → x -- -- Notice how this function takes two arguments instead of one. The first -- argument is the type of the second argument. -- -- Let's illustrate how this works by actually using the above function: -- -- > $ echo "λ(a : Type) → λ(x : a) → x" > id -- -- If we supply the function alone to the compiler we get the inferred type as -- the first line: -- -- > $ dhall -- > ./id -- > <Ctrl-D> -- > ∀(a : Type) → ∀(x : a) → a -- > -- > λ(a : Type) → λ(x : a) → x -- -- You can read the type @(∀(a : Type) → ∀(x : a) → a)@ as saying: \"This is the -- type of a function whose first argument is named @a@ and is a @Type@. The -- second argument is named @x@ and has type @a@ (i.e. the value of the first -- argument). The result also has type @a@.\" -- -- This means that the type of the second argument changes depending on what -- type we provide for the first argument. When we apply @./id@ to @Natural@, -- we create a function that expects an @Natural@ argument: -- -- > $ dhall -- > ./id Natural -- > <Ctrl-D> -- > ∀(x : Natural) → Natural -- > -- > λ(x : Natural) → x -- -- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a -- @Bool@ argument: -- -- > $ dhall -- > ./id Bool -- > <Ctrl-D> -- > ∀(x : Bool) → Bool -- > -- > λ(x : Bool) → x -- -- We can then supply the final argument to each of those functions to show -- that they both work on their respective types: -- -- > $ dhall -- > ./id Natural 4 -- > <Ctrl-D> -- > Natural -- > -- > 4 -- -- > $ dhall -- > ./id Bool True -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Built-in functions can also be polymorphic, too. For example, we can ask -- the compiler for the type of @List/reverse@, the function that reverses a -- list: -- -- > $ dhall -- > List/reverse -- > <Ctrl-D> -- > ∀(a : Type) → List a → List a -- > -- > List/reverse -- -- The first argument to @List/reverse@ is the type of the list to reverse: -- -- > $ dhall -- > List/reverse Bool -- > <Ctrl-D> -- > List Bool → List Bool -- > -- > List/reverse Bool -- -- ... and the second argument is the list to reverse: -- -- > $ dhall -- > List/reverse Bool [True, False] -- > <Ctrl-D> -- > List Bool -- > -- > [False, True] : List Bool -- -- Note that the second argument has no name. This type: -- -- > ∀(a : Type) → List a → List a -- -- ... is equivalent to this type: -- -- > ∀(a : Type) → ∀(_ : List a) → List a -- -- In other words, if you don't see the @∀@ symbol surrounding a function -- argument type then that means that the name of the argument is @"_"@. This -- is true even for user-defined functions: -- -- > $ dhall -- > λ(_ : Text) → 1 -- > <Ctrl-D> -- > Text → Natural -- > -- > λ(_ : Text) → 1 -- -- The type @(Text → Natural)@ is the same as @(∀(_ : Text) → Natural)@ -- -- __Exercise__ : Translate Haskell's `flip` function to Dhall -- $total -- -- Dhall is a total programming language, which means that Dhall is not -- Turing-complete and evaluation of every Dhall program is guaranteed to -- eventually halt. There is no upper bound on how long the program might take -- to evaluate, but the program is guaranteed to terminate in a finite amount of -- time and not hang forever. -- -- This guarantees that all Dhall programs can be safely reduced to a normal -- form where as many functions have been evaluated as possible. In fact, Dhall -- expressions can be evaluated even if all function arguments haven't been fully -- applied. For example, the following program is an anonymous function: -- -- > $ dhall -- > \(n : Bool) -> 10 * 10 -- > <Ctrl-D> -- > ∀(n : Bool) → Natural -- > -- > λ(n : Bool) → 100 -- -- ... and even though the function is still missing the first argument named -- @n@ the compiler is smart enough to evaluate the body of the anonymous -- function ahead of time before the function has even been invoked. -- -- We can use the @map@ function from the Prelude to illustrate an even more -- complex example: -- -- > $ dhall -- > let Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map -- > in λ(f : Natural → Natural) → Prelude/List/map Natural Natural f [1, 2, 3] -- > <Ctrl-D> -- > ∀(f : Natural → Natural) → List Natural -- > -- > λ(f : Natural → Natural) → [f 1, f 2, f 3] : List Natural -- -- Dhall can apply our function to each element of the list even before we specify -- which function to apply. -- -- The language will also never crash or throw any exceptions. Every -- computation will succeed and produce something, even if the result might be -- an @Optional@ value: -- -- > $ dhall -- > List/head Natural ([] : List Natural) -- > <Ctrl-D> -- > Optional Natural -- > -- > None Natural -- -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- -- <https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate> -- -- Test what the following Dhall expression normalizes to: -- -- > let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate -- > in replicate 10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by -- finding an input expression that crashes or loops forever (and file a bug -- report if you succeed) -- $headers -- -- Sometimes you would like to provide additional request headers when importing -- Dhall expressions from URLs. For example, you might want to provide an -- authorization header or specify the expected content type. -- -- Dhall URL imports let you add or modify request headers with the @using@ -- keyword: -- -- > https://example.com/example.dhall using ./headers -- -- ... where you can replace @./headers@ with any import that points to a Dhall -- expression of the following type: -- -- > List { header : Text, value : Text } -- -- For example, if you needed to specify the content type correctly in order to -- download the file, then your @./headers@ file might look like this: -- -- > $ cat headers -- > [ { header = "Accept", value = "application/dhall" } ] -- -- ... or if you needed to provide an authorization token to access a private -- GitHub repository, then your headers could look like this: -- -- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN as Text}" } ] -- -- This would read your GitHub API token from the @GITHUB_TOKEN@ environment -- variable and supply that token in the authorization header. -- -- You cannot inline the headers within the same file as the URL. You must -- provide them as a separate import. That means that this is /not/ legal code: -- -- > http://example.com/example.dhall using [ { header = "Accept", value = "application/dhall" } ] -- NOT legal -- -- Dhall will forward imports if you import an expression from a URL that -- contains a relative import. For example, if you import an expression like -- this: -- -- > http://example.com/example.dhall using ./headers -- -- ... and @http:\/\/example.com/example.dhall@ contains a relative import of @./foo@ -- then Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. -- $integrity -- -- Sometimes you want to use share code while still ensuring that the imported -- value never changes and can't be corrupted by a malicious attacker. Dhall -- provides built-in support for hashing imported values to verify that their -- value never changes -- -- For example, suppose you save the following two files: -- -- > $ cat ./foo -- > ./bar sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b -- -- > $ cat ./bar -- > ./baz -- -- > $ cat ./baz -- > 1 -- -- The first file named @./foo@ contains an example of an integrity check. You -- can add @sha256:XXX@ after any import (such as after @./bar@), where @XXX@ is -- an expected 64-character @sha256@ hash of the Dhall value. To be precise, -- the hash represents a @sha256@ hash of the UTF-8 encoding of a canonical text -- representation of the fully resolved and normalized abstract syntax tree of -- the imported expression. -- -- Dhall will verify that the expected hash matches the actual hash of the -- imported Dhall value and reject the import if there is a hash mismatch: -- -- > $ dhall <<< './foo' -- > Natural -- > -- > 1 -- -- This implies that the hash only changes if the Dhall value changes. For -- example, if you add a comment to the @./bar@ file: -- -- > $ cat ./bar -- > -- This comment does not change the hash -- > ./baz -- -- ... then @./foo@ will still successfully import @./bar@ because the hash -- only depends on the normalized value and does not depend on meaningless -- changes to whitespace or comments: -- -- > $ dhall <<< './foo' # This still succeeds -- > Natural -- > -- > 1 -- -- You can compute the Hash for any import by using the hash subcommand -- of this package. For example: -- -- > dhall hash <<< './bar' -- > sha256:6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b -- -- Then you can paste that output into your code after the import -- -- Now suppose that you you change the value of the @./baz@ file: -- -- > $ cat ./baz -- > 2 -- -- ... then the @./foo@ file will fail to import @./bar@, even though the -- text of the @./bar@ file technically never changed: -- -- > dhall <<< './foo' -- > -- > Error: Import integrity check failed -- > -- > Expected hash: -- > -- > ↳ 6b86b273ff34fce19d6b804eff5a3f5747ada4eaa22f1d49c01e52ddb7875b4b -- > -- > Actual hash: -- > -- > ↳ d4735e3a265e16eee03f59718b9b5d03019c07d8b6c51f90da3a666eec13ab35 -- -- This is because the @./bar@ file now represents a new value (@2@ instead of -- @1@), even though the text of the @./bar@ is still the same. Since the value -- changed the hash must change as well. However, we could change @./baz@ to: -- -- > $ cat baz -- > if True then 1 else 2 -- -- ... and the import would succeed again because the final result is still @1@. -- -- The integrity hash ensures that your import's final meaning can never change, -- so an attacker can never compromise an imported value protected by a hash -- unless they can break SHA-256 encryption. The hash not only protects the -- file that you immediately import, but also protects every transitive import -- as well. -- -- You can also safely refactor your imported dependencies knowing that the -- refactor will not change your hash so long as your refactor is -- behavior-preserving. This provides an easy way to detect refactoring errors -- that you might accidentally introduce. The hash not only protects you -- from attackers, but also protects against human error, too! -- -- If you have a file which either doesn't already use hashed imports, -- or you changed some of the imports and want to update the hashes you can use the -- freeze command to either add or update hashes: -- -- > $ cat foo.dhall -- > let replicate = -- > https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate -- > in replicate 5 -- > $ -- > $ dhall freeze --inplace ./foo.dhall -- > $ cat ./foo.dhall -- > let replicate = -- > https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate sha256:b0e3ec1797b32c80c0bcb7e8254b08c7e9e35e75e6b410c7ac21477ab90167ad -- > in replicate 5 -- -- $rawText -- -- Sometimes you want to import the contents of a raw text file as a Dhall -- value of type `Text`. For example, one of the fields of a record might be -- the contents of a software license: -- -- > { package = "dhall" -- > , author = "Gabriel Gonzalez" -- > , license = ./LICENSE -- > } -- -- Normally if you wanted to import a text file you would need to wrap the -- contents of the file in double single-quotes, like this: -- -- > $ cat LICENSE -- > '' -- > Copyright (c) 2017 Gabriel Gonzalez -- > All rights reserved. -- > -- > ... -- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- > '' -- -- ... which does not work well if you need to reuse the same text file for -- other programs -- -- However, Dhall supports importing a raw text file by adding @as Text@ to the -- end of the import, like this: -- -- > { package = "dhall" -- > , author = "Gabriel Gonzalez" -- > , license = ./LICENSE as Text -- > } -- -- ... and then you can use the original text file unmodified: -- -- > $ cat LICENSE -- > Copyright (c) 2017 Gabriel Gonzalez -- > All rights reserved. -- > -- > ... -- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- $format -- -- A format subcommand is also available that you can use to -- automatically format Dhall expressions. For example, we can take the -- following unformatted Dhall expression: -- -- > $ cat ./unformatted -- > λ(a : Type) → λ(kvss : List (List { index : Natural, value : a })) → -- > List/build { index : Natural, value : a } (λ(list : Type) → λ(cons : { -- > index : Natural, value : a } → list → list) → λ(nil : list) → -- > (List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff : -- > Natural → list } (λ(kvs : List { index : Natural, value : a }) → λ(y : { -- > count : Natural, diff : Natural → list }) → { count = y.count + List/length -- > { index : Natural, value : a } kvs, diff = λ(n : Natural) → List/fold { -- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a -- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value } -- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count = -- > 0, diff = λ(_ : Natural) → nil }).diff 0) -- -- ... and run the expression through the formatter: -- -- > $ dhall format < ./unformatted -- > λ(a : Type) -- > → λ(kvss : List (List { index : Natural, value : a })) -- > → List/build -- > { index : Natural, value : a } -- > ( λ(list : Type) -- > → λ(cons : { index : Natural, value : a } → list → list) -- > → λ(nil : list) -- > → ( List/fold -- > (List { index : Natural, value : a }) -- > kvss -- > { count : Natural, diff : Natural → list } -- > ( λ(kvs : List { index : Natural, value : a }) -- > → λ(y : { count : Natural, diff : Natural → list }) -- > → { count = y.count + List/length { index : Natural, value : a } kvs -- > , diff = -- > λ(n : Natural) -- > → List/fold -- > { index : Natural, value : a } -- > kvs -- > list -- > ( λ(kvOld : { index : Natural, value : a }) -- > → λ(z : list) -- > → cons { index = kvOld.index + n, value = kvOld.value } z -- > ) -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > ) -- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff -- > 0 -- > ) -- -- The executable formats expressions without resolving, type-checking, or -- normalizing them: -- -- > $ dhall format -- > let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D> -- > let replicate = -- > https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate -- > -- > in replicate -- > 5 -- > (List (List Natural)) -- > (replicate 5 (List Natural) (replicate 5 Natural 1)) -- -- You can also use the formatter to modify files in place using the -- @--inplace@ flag (i.e. for formatting source code): -- -- > $ dhall format --inplace ./unformatted -- > $ cat ./unformatted -- > λ(a : Type) -- > → λ(kvss : List (List { index : Natural, value : a })) -- > → List/build -- > { index : Natural, value : a } -- > ( λ(list : Type) -- > → λ(cons : { index : Natural, value : a } → list → list) -- > → λ(nil : list) -- > → ( List/fold -- > (List { index : Natural, value : a }) -- > kvss -- > { count : Natural, diff : Natural → list } -- > ( λ(kvs : List { index : Natural, value : a }) -- > → λ(y : { count : Natural, diff : Natural → list }) -- > → { count = y.count + List/length { index : Natural, value : a } kvs -- > , diff = -- > λ(n : Natural) -- > → List/fold -- > { index : Natural, value : a } -- > kvs -- > list -- > ( λ(kvOld : { index : Natural, value : a }) -- > → λ(z : list) -- > → cons { index = kvOld.index + n, value = kvOld.value } z -- > ) -- > (y.diff (n + List/length { index : Natural, value : a } kvs)) -- > } -- > ) -- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff -- > 0 -- > ) -- -- Carefully note that the code formatter does not preserve all comments. -- Currently, the formatter only preserves leading comments and whitespace -- up until the last newline preceding the code. In other words: -- -- > $ dhall format -- > {- This comment will be preserved by the formatter -} -- > -- ... and this comment will be preserved, too -- > {- This comment will *NOT* be preserved -} 1 -- > -- ... and this comment will also *NOT* be preserved -- > <Ctrl-D> -- > {- This comment will be preserved by the formatter -} -- > -- ... and this comment will be preserved, too -- > 1 -- -- Note that you do not need to format the output of the -- @dhall@ interpreter. The interpreter already automatically formats -- multi-line expressions, too: -- -- > $ dhall -- > let replicate = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/replicate -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D> -- > List (List (List Natural)) -- > -- > [ [ [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] -- > : List (List Natural) -- > , [ [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] -- > : List (List Natural) -- > , [ [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] -- > : List (List Natural) -- > , [ [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] -- > : List (List Natural) -- > , [ [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > , [ 1, 1, 1, 1, 1 ] : List Natural -- > ] -- > : List (List Natural) -- > ] -- > : List (List (List Natural)) -- $builtins -- -- Dhall is a restricted programming language that only supports simple built-in -- functions and operators. If you want to do anything fancier you will need to -- load your data into Haskell for further processing -- -- This section covers types, functions, and operators that are built into the -- language, meaning that you do not need to import any code to use them. -- Additionally, Dhall also comes with a Prelude (covered in the next section) -- hosted online that contains functions derived from these base utilities. The -- Prelude also re-exports all built-in functions for people who prefer -- consistency. -- -- The following documentation on built-ins is provided primarily as a reference. -- You don't need to read about every single built-in and you may want to skip to -- the following Prelude section. -- The language provides built-in support for the following primitive types: -- -- * @Bool@ values -- * @Natural@ values -- * @Integer@ values -- * @Double@ values -- * @Text@ values -- -- ... as well as support for the following derived types: -- -- * @List@s of values -- * @Optional@ values -- * Anonymous records -- * Anonymous unions -- $caveats -- -- Dhall differs in a few important ways from other programming languages, so -- you should keep the following caveats in mind: -- -- First, Dhall only supports addition and multiplication on @Natural@ numbers -- (i.e. non-negative integers), which are not the same type of number as -- @Integer@s (which can be negative). An @Integer@ number is a number prefixed -- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading -- sign. If you try to add or multiply two @Integer@s you will get a type -- error: -- -- > $ dhall -- > +2 + +2 -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: ❰+❱ only works on ❰Natural❱s -- > -- > +2 + +2 -- > -- > (stdin):1:1 -- -- In fact, there are no built-in functions for @Integer@s (or @Double@s). As -- far as the language is concerned they are opaque values that can only be -- shuffled around but not used in any meaningful way until they have been -- loaded into Haskell. -- -- Second, the equality @(==)@ and inequality @(!=)@ operators only work on -- @Bool@s. You cannot test any other types of values for equality. -- -- 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 (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 -- > -- > (stdin):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) -- $builtinOverview -- -- Each of the following sections provides an overview of builtin functions and -- operators for each type. For each function you get: -- -- * An example use of that function -- -- * A \"type judgement\" explaining when that function or operator is well -- typed -- -- For example, for the following judgement: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x && y : Bool -- -- ... you can read that as saying: "if @x@ has type @Bool@ and @y@ has type -- @Bool@, then @x && y@ has type @Bool@" -- -- Similarly, for the following judgement: -- -- > ───────────────────────────────── -- > Γ ⊢ Natural/even : Natural → Bool -- -- ... you can read that as saying: "@Natural/even@ always has type -- @Natural → Bool@" -- -- * Rules for how that function or operator behaves -- -- These rules are just equalities that come in handy when reasoning about code. -- For example, the section on @(&&)@ has the following rules: -- -- > (x && y) && z = x && (y && z) -- > -- > x && True = x -- > -- > True && x = x -- -- These rules are also a contract for how the compiler should behave. If you -- ever observe code that does not obey these rules you should file a bug -- report. -- $bool -- -- There are two values that have type @Bool@ named @True@ and @False@: -- -- > ─────────────── -- > Γ ⊢ True : Bool -- -- > ──────────────── -- > Γ ⊢ False : Bool -- -- The built-in operations for values of type @Bool@ are: -- -- $or -- -- Example: -- -- > $ dhall -- > True || False -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x || y : Bool -- -- Rules: -- -- > (x || y) || z = x || (y || z) -- > -- > x || False = x -- > -- > False || x = x -- > -- > x || (y && z) = (x || y) && (x || z) -- > -- > x || True = True -- > -- > True || x = True -- $and -- -- Example: -- -- > $ dhall -- > True && False -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x && y : Bool -- -- Rules: -- -- > (x && y) && z = x && (y && z) -- > -- > x && True = x -- > -- > True && x = x -- > -- > x && (y || z) = (x && y) || (x && z) -- > -- > x && False = False -- > -- > False && x = False -- $equal -- -- Example: -- -- > $ dhall -- > True == False -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x == y : Bool -- -- Rules: -- -- > (x == y) == z = x == (y == z) -- > -- > x == True = x -- > -- > True == x = x -- > -- > x == x = True -- $unequal -- -- Example: -- -- > $ dhall -- > True != False -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > Γ ⊢ x : Bool Γ ⊢ y : Bool -- > ─────────────────────────── -- > Γ ⊢ x != y : Bool -- -- Rules: -- -- > (x != y) != z = x != (y != z) -- > -- > x != False = x -- > -- > False != x = x -- > -- > x != x = False -- $ifthenelse -- -- Example: -- -- > $ dhall -- > if True then 3 else 5 -- > <Ctrl-D> -- > Natural -- > -- > 3 -- -- Type: -- -- > Γ ⊢ t : Type -- > ───────────────────── -- > Γ ⊢ b : Bool Γ ⊢ l : t Γ ⊢ r : t -- > ──────────────────────────────────── -- > Γ ⊢ if b then l else r : t -- -- Rules: -- -- > if b then True else False = b -- > -- > if True then l else r = l -- > -- > if False then l else r = r -- $natural -- -- @Natural@ literals are non-negative numbers without any leading sign, like -- this: -- -- > 4 : Natural -- -- If you add a @+@ or @-@ sign then you get an @Integer@ literal, which is a -- different type of value -- $plus -- -- Example: -- -- > $ dhall -- > 2 + 3 -- > <Ctrl-D> -- > Natural -- > -- > 5 -- -- Type: -- -- > Γ ⊢ x : Natural Γ ⊢ y : Natural -- > ───────────────────────────────── -- > Γ ⊢ x + y : Natural -- -- Rules: -- -- > (x + y) + z = x + (y + z) -- > -- > x + 0 = x -- > -- > 0 + x = x -- $times -- -- Example: -- -- > $ dhall -- > 2 * 3 -- > <Ctrl-D> -- > Natural -- > -- > 6 -- -- Type: -- -- > Γ ⊢ x : Natural Γ ⊢ y : Natural -- > ───────────────────────────────── -- > Γ ⊢ x * y : Natural -- -- Rules: -- -- > (x * y) * z = x * (y * z) -- > -- > x * 1 = x -- > -- > 1 * x = x -- > -- > (x + y) * z = (x * z) + (y * z) -- > -- > x * (y + z) = (x * y) + (x * z) -- > -- > x * 0 = 0 -- > -- > 0 * x = 0 -- $even -- -- Example: -- -- > $ dhall -- > Natural/even 6 -- > <Ctrl-D> -- > Bool -- > -- > True -- -- Type: -- -- > ───────────────────────────────── -- > Γ ⊢ Natural/even : Natural → Bool -- -- Rules: -- -- > Natural/even (x + y) = Natural/even x == Natural/even y -- > -- > Natural/even 0 = True -- > -- > Natural/even (x * y) = Natural/even x || Natural/even y -- > -- > Natural/even 1 = False -- $odd -- -- Example: -- -- > $ dhall -- > Natural/odd 6 -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > ──────────────────────────────── -- > Γ ⊢ Natural/odd : Natural → Bool -- -- Rules: -- -- > Natural/odd (x + y) = Natural/odd x != Natural/odd y -- > -- > Natural/odd 0 = False -- > -- > Natural/odd (x * y) = Natural/odd x && Natural/odd y -- > -- > Natural/odd 1 = True -- $isZero -- -- Example: -- -- > $ dhall -- > Natural/isZero 6 -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > ─────────────────────────────────── -- > Γ ⊢ Natural/isZero : Natural → Bool -- -- Rules: -- -- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y -- > -- > Natural/isZero 0 = True -- > -- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y -- > -- > Natural/isZero 1 = False -- $naturalFold -- -- Example: -- -- > $ dhall -- > Natural/fold 40 Text (λ(t : Text) → t ++ "!") "You're welcome" -- > <Ctrl-D> -- > Text -- > -- > "You're welcome!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!" -- -- Type: -- -- > ────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ Natural/fold : Natural → ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural -- -- Rules: -- -- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z) -- > -- > Natural/fold 0 n s z = z -- > -- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s) -- > -- > Natural/fold 1 n s = s -- $naturalBuild -- -- Example: -- -- > $ dhall -- > Natural/build (λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ zero)) -- > <Ctrl-D> -- > Natural -- > -- > 2 -- -- Type: -- -- > ───────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ Natural/build : (∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural) → Natural -- -- Rules: -- -- > Natural/fold (Natural/build x) = x -- > -- > Natural/build (Natural/fold x) = x -- $integer -- -- @Integer@ literals are prefixed with a @+@ (if they are non-negative) or a -- @-@ sign (if they are negative), like this: -- -- > +3 : Integer -- > -2 : Integer -- -- If you omit the sign then they are @Natural@ literals and not @Integer@s -- -- There are no built-in operations on @Integer@s. For all practical purposes -- they are opaque values within the Dhall language -- $double -- -- A @Double@ literal is a floating point value with at least one decimal -- place, such as: -- -- > -2.0 : Double -- > 3.14159 : Double -- -- There are no built-in operations on @Double@s. For all practical purposes -- they are opaque values within the Dhall language -- $text -- -- A @Text@ literal is just a sequence of characters enclosed in double quotes, -- like: -- -- > "ABC" : Text -- -- The only thing you can do with @Text@ values is concatenate them -- $textAppend -- -- Example: -- -- > $ dhall -- > "Hello, " ++ "world!" -- > <Ctrl-D> -- > Text -- > -- > "Hello, world!" -- -- Type: -- -- > Γ ⊢ x : Text Γ ⊢ y : Text -- > ─────────────────────────── -- > Γ ⊢ x && y : Text -- -- Rules: -- -- > (x ++ y) ++ z = x ++ (y ++ z) -- > -- > x ++ "" = x -- > -- > "" ++ x = x -- $list -- -- Dhall @List@ literals are a sequence of values inside of brackets separated by -- commas: -- -- > Γ ⊢ t : Type Γ ⊢ x : t Γ ⊢ y : t ... -- > ────────────────────────────────────────── -- > Γ ⊢ [x, y, ... ] : List t -- -- Also, every empty @List@ must end with a mandatory type annotation, for example: -- -- > [] : List Natural -- -- The built-in operations on @List@s are: -- $listAppend -- -- Example: -- -- > $ dhall -- > [1, 2, 3] # [4, 5, 6] -- > <Ctrl-D> -- > List Natural -- > -- > [1, 2, 3, 4, 5, 6] -- -- Type: -- -- > Γ ⊢ x : List a Γ ⊢ y : List a -- > ───────────────────────────────── -- > Γ ⊢ x # y : List a -- -- Rules: -- -- > ([] : List a) # xs = xs -- > -- > xs # ([] : List a) = xs -- > -- > (xs # ys) # zs = xs # (ys # zs) -- $listFold -- -- Example: -- -- > $ dhall -- > List/fold Bool [True, False, True] Bool (λ(x : Bool) → λ(y : Bool) → x && y) True -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Type: -- -- > ──────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ List/fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list -- -- Rules: -- -- > let Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat -- > -- > List/fold a (Prelude/List/concat a xss) b c -- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c) -- > -- > List/fold a ([] : List a) b c n = n -- > -- > List/fold a ([x] : List a) b c = c x -- $listBuild -- -- Example: -- -- > $ dhall -- > List/build Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil))) -- > <Ctrl-D> -- > List Natural -- > -- > [1, 2, 3] : List Natural -- -- Type: -- -- > ─────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ List/build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a -- -- Rules: -- -- > List/build t (List/fold t x) = x -- > -- > List/fold t (List/build t x) = x -- $listLength -- -- Example: -- -- > $ dhall -- > List/length Natural [1, 2, 3] -- > <Ctrl-D> -- > Natural -- > -- > 3 -- -- Type: -- -- > ──────────────────────────────────────────────── -- > Γ ⊢ List/length : ∀(a : Type) → List a → Natural -- -- Rules: -- -- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + 1) 0 -- $listHead -- -- Example: -- -- > $ dhall -- > List/head Natural [1, 2, 3] -- > <Ctrl-D> -- > Optional Natural -- > -- > Some 1 -- -- Type: -- -- > ─────────────────────────────────────────────── -- > Γ ⊢ List/head ∀(a : Type) → List a → Optional a -- -- Rules: -- -- > let Prelude/Optional/head = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Optional/head -- > let Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat -- > let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap -- > let Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map -- > -- > List/head a (Prelude/List/concat a xss) = -- > Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss) -- > -- > List/head a ([x] : List a) = Some x -- > -- > List/head b (Prelude/List/concatMap a b f m) -- > = Prelude/Optional/concatMap a b (λ(x : a) → List/head b (f x)) (List/head a m) -- $listLast -- -- Example: -- -- > $ dhall -- > List/last Natural [1, 2, 3] -- > <Ctrl-D> -- > Optional Natural -- > -- > Some 1 -- -- Type: -- -- > ───────────────────────────────────────────────── -- > Γ ⊢ List/last : ∀(a : Type) → List a → Optional a -- -- Rules: -- -- > let Prelude/Optional/last = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Optional/last -- > let Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat -- > let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap -- > let Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map -- > -- > List/last a (Prelude/List/concat a xss) = -- > Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss) -- > -- > List/last a ([x] : List a) = Some x -- > -- > List/last b (Prelude/List/concatMap a b f m) -- > = Prelude/Optional/concatMap a b (λ(x : a) → List/last b (f x)) (List/last a m) -- $listIndexed -- -- Example -- -- > $ dhall -- > List/indexed Text ["ABC", "DEF", "GHI"] -- > <Ctrl-D> -- > List { index : Natural, value : Text } -- > -- > [{ index = 0, value = "ABC" }, { index = 1, value = "DEF" }, { index = 2, value = "GHI" }] : List { index : Natural, value : Text } -- -- Type: -- -- > ───────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a } -- -- Rules: -- -- > let Prelude/List/shifted = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/shifted -- > let Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat -- > let Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map -- > -- > List/indexed a (Prelude/List/concat a xss) = -- > Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss) -- $listReverse -- -- Example: -- -- > $ dhall -- > List/reverse Natural [1, 2, 3] -- > <Ctrl-D> -- > List Natural -- > -- > [3, 2, 1] : List Natural -- -- Type: -- -- > ───────────────────────────────────────────────── -- > Γ ⊢ List/reverse : ∀(a : Type) → List a → List a -- -- Rules: -- -- > let Prelude/List/map = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/map -- > let Prelude/List/concat = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concat -- > let Prelude/List/concatMap = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/List/concatMap -- > -- > List/reverse a (Prelude/List/concat a xss) -- > = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss)) -- > -- > List/reverse a ([x] : List a) = [x] : List a -- > -- > List/reverse b (Prelude/List/concatMap a b f xs) -- > = Prelude/List/concatMap a b (λ(x : a) → List/reverse b (f x)) (List/reverse a xs) -- > -- > List/reverse a ([x, y] : List a) = [y, x] : List a -- $optional1 -- -- Dhall @Optional@ literals are either @Some@ followed by a value: -- -- > Γ ⊢ x : t Γ ⊢ t : Type -- > ──────────────────────── -- > Γ ⊢ Some x : Optional t -- -- ... or @None@ followed by a type: -- -- > ─────────────────────────────────── -- > Γ ⊢ None : ∀(t : Type) → Optional t -- -- Note that `None` is a valid standalone function -- -- The built-in operations on @Optional@ values are: -- $optionalFold -- -- Example: -- -- > $ dhall -- > Optional/fold Text (Some "ABC") Text (λ(t : Text) → t) "" -- > <Ctrl-D> -- > Text -- > -- > "ABC" -- -- Type: -- -- > ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── -- > Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(some : a → optional) → ∀(none : optional) → optional -- -- Rules: -- -- > Optional/fold a (None a) o j n = n -- > -- > Optional/fold a (Some x) o j n = j x -- $prelude -- -- There is also a Prelude available at: -- -- <http://prelude.dhall-lang.org> -- -- ... which currenty redirects to: -- -- <https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75> -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a -- set of convenient utilities which didn't quite make the cut to be built into -- the language. Feel free to host your own custom Prelude if you want! -- -- If you visit the above link you can browse the Prelude, which has a few -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file -- located here: -- -- <https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not> -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- -- > $ curl https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not -- > {- -- > Flip the value of a `Bool` -- > -- > Examples: -- > -- > ``` -- > ./not True = False -- > -- > ./not False = True -- > ``` -- > -} -- > let not : Bool → Bool -- > = λ(b : Bool) → b == False -- > -- > in not -- -- The file could have been much shorter, like this: -- -- > λ(b : Bool) → b == False -- -- ... but all the functions exported from the Prelude try to be as -- self-documenting as possible by including: -- -- * the name of the function -- * the type of the function -- * documentation (including a few examples) -- -- The performance penalty for adding these helpful features is negligible. -- -- You can use this @not@ function either directly: -- -- > $ dhall -- > https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not True -- > <Ctrl-D> -- > Bool -- > -- > False -- -- ... or assign the URL to a shorter name: -- -- > $ dhall -- > let Bool/not = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Bool/not -- > in Bool/not True -- > <Ctrl-D> -- > Bool -- > -- > False -- -- Some functions in the Prelude just re-export built-in functions for -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- -- > $ curl https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > -- > Examples: -- > -- > ``` -- > ./even 3 = False -- > -- > ./even 0 = True -- > ``` -- > -} -- > let even : Natural → Bool -- > = Natural/even -- > -- > in even -- -- You can also clone the Prelude locally to your filesystem if you prefer -- using `git clone`, like this: -- -- > $ git clone https://github.com/dhall-lang/Prelude.git -- > $ tree Prelude -- > Prelude -- > ├── Bool -- > │ ├── and -- > │ ├── build -- > │ ├── even -- > │ ├── fold -- > │ ├── not -- > │ ├── odd -- > │ ├── or -- > │ ├── package.dhall -- > │ └── show -- > ├── Double -- > │ ├── package.dhall -- > │ └── show -- > ├── Integer -- > │ ├── package.dhall -- > │ └── show -- > ├── List -- > │ ├── all -- > │ ├── any -- > │ ├── build -- > │ ├── concat -- > │ ├── concatMap -- > │ ├── filter -- > │ ├── fold -- > │ ├── generate -- > │ ├── head -- > │ ├── indexed -- > │ ├── iterate -- > │ ├── last -- > │ ├── length -- > │ ├── map -- > │ ├── null -- > │ ├── package.dhall -- > │ ├── replicate -- > │ ├── reverse -- > │ ├── shifted -- > │ └── unzip -- > ├── Monoid -- > ├── Natural -- > │ ├── build -- > │ ├── enumerate -- > │ ├── even -- > │ ├── fold -- > │ ├── isZero -- > │ ├── odd -- > │ ├── package.dhall -- > │ ├── product -- > │ ├── show -- > │ ├── sum -- > │ └── toInteger -- > ├── Optional -- > │ ├── None -- > │ ├── Some -- > │ ├── all -- > │ ├── any -- > │ ├── build -- > │ ├── concat -- > │ ├── filter -- > │ ├── fold -- > │ ├── head -- > │ ├── last -- > │ ├── length -- > │ ├── map -- > │ ├── null -- > │ ├── package.dhall -- > │ ├── toList -- > │ └── unzip -- > ├── Record -- > │ ├── keyText -- > │ ├── keyValue -- > │ └── package.dhall -- > ├── Text -- > │ ├── concat -- > │ ├── concatMap -- > │ ├── concatMapSep -- > │ ├── concatSep -- > │ └── package.dhall -- > └── package.dhall -- > -- > 8 directories, 70 files -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- -- <https://github.com/dhall-lang/Prelude> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial -- -- You can also import the entire Prelude as a single large record for -- convenience: -- -- > $ dhall -- > let Prelude = https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/package.dhall -- > -- > in λ(x : Text) -- > → Prelude.`List`.length Text (Prelude.`List`.replicate 10 Text x) -- > <Ctrl-D> -- > ∀(x : Text) → Natural -- > -- > λ(x : Text) → 10 -- -- The organization of the package mirrors the layout of the Prelude, meaning -- that every directory is stored as a record whose children are the fields of -- that record. -- -- __Exercise__: Browse the Prelude by running: -- -- > $ dhall <<< 'https://raw.githubusercontent.com/dhall-lang/Prelude/35deff0d41f2bf86c42089c6ca16665537f54d75/package.dhall' -- $conclusion -- -- By this point you should be able to use the Dhall configuration language to -- author, import, and program configuration files. If you run into any issues -- you can report them at: -- -- <https://github.com/dhall-lang/dhall-haskell/issues> -- -- You can also request features, support, or documentation improvements on the -- above issue tracker. -- -- If you would like to contribute to the Dhall project you can try to port Dhall -- to other languages besides Haskell so that Dhall configuration files can be -- read into those languages, too. -- $faq -- -- * Why do empty lists require a type annotation? -- -- Unlike Haskell, Dhall cannot infer a polymorphic type for the empty list -- because Dhall represents polymorphic values as functions of types, like this: -- -- > λ(a : Type) → [] : List a -- -- If the compiler treated an empty list literal as syntactic short-hand for -- the above polymorphic function then you'd get the unexpected behavior where -- a list literal is a function if the list has 0 elements but not a function -- otherwise. -- -- * Does Dhall support user-defined recursive types? -- -- No, but you can translate recursive code to non-recursive code by following -- this guide: -- -- <https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall How to translate recursive code to Dhall>