{-# OPTIONS_GHC -fno-warn-unused-imports #-} {-| Dhall is a programming language specialized for configuration files. This module contains a tutorial explaining how to author configuration files using this language -} module Dhall.Tutorial ( -- * Introduction -- $introduction -- * Types -- $types -- * Imports -- $imports -- * Lists -- $lists -- * Optional values -- $optional0 -- * Records -- $records -- * Functions -- $functions -- * Compiler -- $compiler -- * Strings -- $strings -- * Combine -- $combine -- * Let expressions -- $let -- * Defaults -- $defaults -- * Unions -- $unions -- * Polymorphic functions -- $polymorphic -- * Total -- $total -- * Assertions -- $assertions -- * Headers -- $headers -- * Import integrity -- $integrity -- * Raw text -- $rawText -- * Formatting code -- $format -- * Built-in functions -- $builtins -- ** Caveats -- $caveats -- ** Extending the language -- $extending -- * 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: -- -- > -- ./config.dhall -- > { foo = 1 -- > , bar = [3.0, 4.0, 5.0] -- > } -- -- You can read the above configuration file into Haskell using the following -- code: -- -- > -- example.hs -- > -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Dhall -- > -- > data Example = Example { foo :: Natural, bar :: Vector Double } -- > deriving (Generic, Show) -- > -- > instance FromDhall Example -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config.dhall" -- > print (x :: Example) -- -- If you compile and run the above example, the program prints the corresponding -- Haskell record: -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]} -- -- You can also load some types directly into Haskell without having to define a -- record, like this: -- -- >>> import Dhall -- >>> :set -XOverloadedStrings -- >>> input auto "True" :: IO Bool -- True -- -- The `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 :: FromDhall a => Type a -- > -- > input auto :: FromDhall a => Text -> IO a -- -- >>> input auto "True" :: IO Bool -- True -- -- You can see what types `auto` supports \"out-of-the-box\" by browsing the -- instances for the `FromDhall` class. For example, the following instance -- says that we can directly decode any Dhall expression that evaluates to a -- @Bool@ into a Haskell `Bool`: -- -- > instance FromDhall Bool -- -- ... which is why we could directly decode the string @\"True\"@ into the -- value `True`. -- -- There is also another instance that says that if we can decode a value of -- type @a@, then we can also decode a @List@ of values as a `Vector` of @a@s: -- -- > instance FromDhall a => FromDhall (Vector a) -- -- Therefore, since we can decode a @Bool@, we must also be able to decode a -- @List@ of @Bool@s, like this: -- -- >>> input auto "[True, False]" :: IO (Vector Bool) -- [True,False] -- -- We could also specify what type to decode by providing an explicit `Type` -- instead of using `auto` with a type annotation: -- -- >>> input (vector bool) "[True, False]" -- [True,False] -- -- __Exercise:__ Create a @./config.dhall@ file that the following program can -- decode: -- -- > {-# LANGUAGE DeriveAnyClass #-} -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Dhall -- > -- > data Person = Person { age :: Natural, name :: Text } -- > deriving (Generic, FromDhall, Show) -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config.dhall" -- > print (x :: Person) -- -- __Exercise:__ Create a @./config.dhall@ file that the following program can -- decode: -- -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > import Data.Functor.Identity -- > import Dhall -- > -- > instance FromDhall a => FromDhall (Identity a) -- > -- > main :: IO () -- > main = do -- > x <- input auto "./config.dhall" -- > print (x :: Identity Double) -- $types -- -- Suppose that we try to decode a value of the wrong type, like this: -- -- >>> input auto "1" :: IO Bool -- *** Exception: -- ...Error...: Expression doesn't match annotation -- ... -- - Bool -- + Natural -- ... -- 1│ 1 : Bool -- ... -- (input):1:1 -- ... -- -- The interpreter complains because the string @\"1\"@ cannot be decoded into a -- Haskell value of type `Bool`. This part of the type error: -- -- > - Bool -- > + Natural -- -- ... means that the expected type was @Bool@ but the inferred type of the -- expression @1@ was @Natural@. -- -- The code excerpt from the above error message has two components: -- -- * the expression being type checked (i.e. @1@) -- * the expression's expected type (i.e. @Bool@) -- -- > Expression -- > ⇩ -- > 1 : Bool -- > ⇧ -- > Expected type -- -- The @(:)@ symbol is how Dhall annotates values with their expected types. -- This notation is equivalent to type annotations in Haskell using the @(::)@ -- symbol. Whenever you see: -- -- > x : t -- -- ... you should read that as \"we expect the expression @x@ to have type -- @t@\". However, we might be wrong and if our expected type does not match the -- expression's actual type then the type checker will complain. -- -- In this case, the expression @1@ does not have type @Bool@ so type checking -- fails with an exception. -- -- __Exercise:__ Load the Dhall library into @ghci@ and run these commands to get -- get a more detailed error message: -- -- > >>> import Dhall -- > >>> :set -XOverloadedStrings -- > >>> detailed (input auto "1") :: IO Bool -- > ... -- -- ... then read the entire error message -- -- __Exercise:__ Fix the type error, either by changing the value to decode or -- changing the expected type -- $imports -- -- You might wonder why in some cases we can decode a configuration file: -- -- >>> writeFile "bool" "True" -- >>> input auto "./bool" :: IO Bool -- True -- -- ... and in other cases we can decode a value directly: -- -- >>> input auto "True" :: IO Bool -- True -- -- This is because importing a configuration from a file is a special case of a -- more general language feature: Dhall expressions can reference other -- expressions by their file path. -- -- To illustrate this, let's create three files: -- -- > $ echo "True" > bool1 -- > $ echo "False" > bool2 -- > $ echo "./bool1 && ./bool2" > both -- -- ... and read in all three files in a single expression: -- -- >>> input auto "[ ./bool1 , ./bool2 , ./both ]" :: IO (Vector Bool) -- [True,False,False] -- -- Each file path is replaced with the Dhall expression contained within that -- file. If that file contains references to other files then those references -- are transitively resolved. -- -- In other words: configuration files can reference other configuration files, -- either by their relative or absolute paths. This means that we can split a -- configuration file into multiple files, like this: -- -- > -- ./config.dhall -- > { foo = 1 -- > , bar = ./bar.dhall -- > } -- -- > -- ./bar.dhall -- > [3.0, 4.0, 5.0] -- -- ... which is equivalent to our original configuration: -- -- > -- ./config.dhall -- > { foo = 1 -- > , bar = [3.0, 4.0, 5.0] -- > } -- -- However, the Dhall language will forbid cycles in these file references. For -- example, if we create the following cycle: -- -- > $ echo './file1' > file2 -- > $ echo './file2' > file1 -- -- ... then the interpreter will reject the import: -- -- >>> input auto "./file1" :: IO Natural -- *** Exception: -- ↳ ./file1 -- ↳ ./file2 -- ... -- Cyclic import: ./file1 -- ... -- -- You can also import expressions by URL. For example, you can find a Dhall -- expression hosted at this GitHub URL: -- -- <https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True> -- -- > $ curl https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True -- > True -- -- ... and you can reference that expression either directly: -- -- >>> input auto "https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- True -- -- ... or inside of a larger expression: -- -- >>> input auto "False == https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- False -- -- You're not limited to hosting Dhall expressions on GitHub. You can host a -- Dhall expression anywhere that you can host UTF8-encoded text on the web, -- such as a pastebin, or your own web server. -- -- You can also import Dhall expressions from environment variables, too: -- -- >>> System.Environment.setEnv "FOO" "1" -- >>> input auto "env:FOO" :: IO Natural -- 1 -- -- You can import types, too. For example, we can change our @./bar@ file to: -- -- > -- ./bar.dhall -- > [3.0, 4.0, 5.0] : List ./type.dhall -- -- ... then specify the type in a separate file: -- -- > -- ./type.dhall -- > Double -- -- ... and everything still type checks: -- -- > $ ./example -- > Example {foo = 1, bar = [3.0,4.0,5.0]} -- -- Note that imports should be terminated by whitespace or parentheses otherwise -- you will get either an import error or a parse error, like this: -- -- >>> writeFile "baz" "2.0" -- >>> input auto "./baz: Double" :: IO Double -- *** Exception: -- ↳ ./baz: -- ... -- ...Error...: Missing file ...baz: -- ... -- -- This is because the parser thinks that @./baz:@ is a single token due to -- the missing whitespace before the colon and tries to import a file named -- @./baz:@, which does not exist. To fix the problem we have to add a space -- after @./baz@: -- -- >>> input auto "./baz : Double" :: IO Double -- 2.0 -- -- __Exercise:__ There is a @not@ function hosted online here: -- -- <https://prelude.dhall-lang.org/Bool/not> -- -- Visit that link and read the documentation. Then try to guess what this -- code returns: -- -- > >>> input auto "https://prelude.dhall-lang.org/Bool/not https://raw.githubusercontent.com/dhall-lang/dhall-haskell/18e4e9a18dc53271146df3ccf5b4177c3552236b/examples/True" :: IO Bool -- > ??? -- -- Run the code to test your guess -- $lists -- -- You can store 0 or more values of the same type in a list, like this: -- -- > [1, 2, 3] -- -- Every list can be followed by the type of the list. The type annotation is -- required for empty lists but optional for non-empty lists. You will get a -- 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:__ Replace the @\"???\"@ with an expression that successfully -- decodes to the specified type: -- -- > >>> input auto "???" :: IO (Vector (Vector Natural)) -- $optional0 -- -- @Optional@ values are either of the form @Some value@ or @None type@. -- -- For example, these are valid @Optional@ values: -- -- > Some 1 -- > -- > None Natural -- -- ... which both have type @Optional Natural@ -- -- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes: -- -- >>> input auto "Some 1" :: IO (Maybe Natural) -- Just 1 -- >>> input auto "None Natural" :: IO (Maybe Natural) -- Nothing -- -- __Exercise:__ Replace the @\"???\"@ with an expression that successfully -- decodes to the specified type: -- -- > >>> input auto "???" :: IO (Maybe (Maybe (Maybe Natural))) -- $records -- -- Record literals are delimited by curly braces and their fields are separated -- by commas. For example, this is a valid record literal: -- -- > { foo = True -- > , bar = 2 -- > , baz = 4.2 -- > } -- -- A record type is like a record literal except instead of specifying each -- field's value we specify each field's type. For example, the preceding -- record literal has the following record type: -- -- > { foo : Bool -- > , bar : Natural -- > , baz : Double -- > } -- -- If you want to specify an empty record literal, you must use @{=}@, which is -- special syntax reserved for empty records. If you want to specify the empty -- record type, then you use @{}@. If you forget which is which you can always -- ask the @dhall@ compiler to remind you of the type for each one: -- -- > $ dhall type <<< '{=}' -- > {} -- -- > $ dhall type <<< '{}' -- > Type -- -- This is our first use of the @dhall@ command-line tool (provided by this -- package), which provides a @type@ subcommand for inferring an expression's -- type. By default the tool reads the expression on standard input and outputs -- the type to standard output. -- -- Note that @<<<@ is a feature specific to the Bash shell to feed a string to -- a command's standard input. If you are using another shell, then you can -- instead do this: -- -- > $ echo '{=}' | dhall type -- > {} -- -- __Exercise__: Use the @dhall type@ command to infer the type of this record: -- -- > -- ./nested.dhall -- > { foo = 1 -- > , bar = -- > { baz = 2.0 -- > , qux = True -- > } -- > } -- -- You can access a field of a record using the following syntax: -- -- > record.fieldName -- -- ... which means to access the value of the field named @fieldName@ from the -- @record@. For example: -- -- >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double -- 4.2 -- -- ... and you can project out multiple fields into a new record using this -- syntax: -- -- > someRecord.{ field₀, field₁, … } -- -- For example: -- -- > $ dhall <<< '{ x = 1, y = True, z = "ABC" }.{ x, y }' -- > { x = 1, y = True } -- -- This is our first example of using the @dhall@ command-line tool with no -- subcommand (like @type@), which evaluates the provided expression. By -- default, this reads the expression on standard input and outputs the -- evaluated result on standard output. -- -- __Exercise__: Save the above @./nested.dhall@ file and then try to access the -- value of the @baz@ field. Test that this works by interpreting your code -- using the @dhall@ command. -- -- You can convert a record to a list of key-value pairs (a.k.a. a \"Map\") by -- using the `toMap` keyword. For example: -- -- > $ dhall <<< 'toMap { foo = 1, bar = 2 }' -- > [ { mapKey = "bar", mapValue = 2 }, { mapKey = "foo", mapValue = 1 } ] -- -- This conversion only works if all field of the record have the same type. -- This comes in handy when you need to convert a Dhall record to the Dhall -- equivalent of a homogeneous map (i.e. Haskell's @"Data.Map"@). -- $functions -- -- The Dhall programming language also supports user-defined anonymous -- functions. For example, we can save the following anonymous function to a -- file: -- -- > -- ./makeBools.dhall -- > \(n : Bool) -> -- > [ n && True, n && False, n || True, n || False ] -- -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB) -- instead of @\\@ and @→@ (U+2192) instead of @->@ (for people who are into that -- sort of thing): -- -- > $ -- ./makeBools.dhall -- > λ(n : Bool) → -- > [ n && True, n && False, n || True, n || False ] -- > <Ctrl-D> -- -- You can read this as a function of one argument named @n@ that has type -- @Bool@. This function returns a @List@ of @Bool@s. Each element of the -- @List@ depends on the input argument named @n@. -- -- The (ASCII) syntax for anonymous functions resembles the syntax for anonymous -- functions in Haskell. The only difference is that Dhall requires you to -- annotate the type of the function's input. -- -- You can import this function into Haskell, too: -- -- >>> makeBools <- input auto "./makeBools.dhall" :: IO (Bool -> Vector Bool) -- >>> makeBools True -- [True,False,True,True] -- -- The reason this works is that there is an `FromDhall` instance for simple -- functions: -- -- > instance (ToDhall a, FromDhall b) => FromDhall (a -> b) -- -- Thanks to currying, this instance works for functions of multiple simple -- arguments: -- -- >>> dhallAnd <- input auto "λ(x : Bool) → λ(y : Bool) → x && y" :: IO (Bool -> Bool -> Bool) -- >>> dhallAnd True False -- False -- -- However, you can't convert anything more complex than that (like a polymorphic -- or higher-order function). You will need to apply those functions to their -- arguments within Dhall before converting their result to a Haskell value. -- -- Just like `FromDhall`, you can derive `ToDhall` for user-defined data types: -- -- > {-# LANGUAGE DeriveAnyClass #-} -- > {-# LANGUAGE DeriveGeneric #-} -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > module Main where -- > -- > import Dhall -- > -- > data Example0 = Example0 { foo :: Bool, bar :: Bool } -- > deriving (Generic, ToDhall) -- > -- > main = do -- > f <- input auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar" -- > print (f (Example0 { foo = True, bar = False }) :: Bool) -- > print (f (Example0 { foo = True, bar = True }) :: Bool) -- -- The above program prints: -- -- > False -- > True -- $compiler -- -- We can also test our @makeBools@ function directly from the command line. -- This library comes with a command-line executable program named @dhall@ that -- you can use to both type-check files and convert them to a normal form. Our -- compiler takes a program on standard input and then prints the program's type -- to standard error followed by the program's normal form to standard output: -- -- > $ dhall --annotate <<< './makeBools.dhall' -- > (λ(n : Bool) → [ n, False, True, n ]) : ∀(n : Bool) → List Bool -- -- The @--annotate@ flag adds a type signature to the output to let us know -- what type the interpreter inferred for our expression. The type signature -- is @∀(n : Bool) → List Bool@ which says that @makeBools@ is a function of one -- argument named @n@ that has type @Bool@ and the function returns a @List@ of -- @Bool@s. The @∀@ (U+2200) symbol is shorthand for the ASCII @forall@ -- keyword: -- -- > ∀(x : a) → b -- This type ... -- > -- > forall (x : a) → b -- ... is the same as this type -- -- ... and Dhall's @forall@ keyword behaves the same way as Haskell's @forall@ -- keyword for input values that are @Type@s: -- -- > forall (x : Type) → b -- This Dhall type ... -- -- > forall x . b -- ... is the same as this Haskell type -- -- The part where Dhall differs from Haskell is that you can also use -- @∀@/@forall@ to give names to non-@Type@ arguments (such as the first -- argument to @makeBools@). -- -- This expression is our program's normal form: -- -- > λ(n : Bool) → [ n, False, True, n ] -- -- ... and the interpreter was able to simplify our expression by noting that: -- -- * @n && True = n@ -- * @n && False = False@ -- * @n || True = True@ -- * @n || False = n@ -- -- To apply a function to an argument you separate the function and argument by -- whitespace (just like Haskell): -- -- @f x@ -- -- You can read the above as \"apply the function @f@ to the argument @x@\". This -- means that we can \"apply\" our @./makeBools@ function to a @Bool@ argument -- like this: -- -- > $ dhall <<< './makeBools.dhall True' -- > [True, False, True, True] -- -- Remember that file paths are synonymous with their contents, so the above -- code is exactly equivalent to: -- -- > $ dhall <<< '(λ(n : Bool) → [n && True, n && False, n || True, n || False]) True' -- > [True, False, True, True] -- -- When you apply an anonymous function to an argument, you substitute the -- \"bound variable" with the function's argument: -- -- > Bound variable -- > ⇩ -- > (λ(n : Bool) → ...) True -- > ⇧ -- > Function argument -- -- So in our above example, we would replace all occurrences of @n@ with @True@, -- like this: -- -- > -- If we replace all of these `n`s with `True` ... -- > [n && True, n && False, n || True, n || False] -- > -- > -- ... then we get this: -- > [True && True, True && False, True || True, True || False] -- > -- > -- ... which reduces to the following normal form: -- > [True, False, True, True] -- -- Now that we've verified that our function type checks and works, we can use -- the same function within Haskell: -- -- >>> input auto "./makeBools.dhall True" :: IO (Vector Bool) -- [True,False,True,True] -- -- __Exercise__: Create a file named @getFoo@ that is a function of the following -- type: -- -- > ∀(r : { foo : Bool, bar : Text }) → Bool -- -- This function should take a single input argument named @r@ that is a record -- with two fields. The function should return the value of the @foo@ field. -- -- __Exercise__: Use the @dhall@ command to infer the type of the function you -- just created and verify that your function has the correct type -- -- __Exercise__: Use the @dhall@ command to apply your function to a sample -- record -- $strings -- Dhall supports ordinary string literals with Haskell-style escaping rules: -- -- > $ dhall -- > "Hello, \"world\"!" -- > <Ctrl-D> -- > "Hello, \"world\"!" -- -- ... and Dhall also supports Nix-style multi-line string literals: -- -- > $ dhall -- > '' -- > #!/bin/bash -- > -- > echo "Hi!" -- > '' -- > <Ctrl-D> -- > "\n#!/bin/bash\n\necho \"Hi!\"\n" -- -- These \"double single quote strings\" ignore all special characters, with one -- exception: if you want to include a @''@ in the string, you will need to -- escape it with a preceding @'@ (i.e. use @'''@ to insert @''@ into the final -- string). -- -- These strings also strip leading whitespace using the same rules as Nix. -- Specifically: \"it strips from each line a number of spaces equal to the -- minimal indentation of the string as a whole (disregarding the indentation -- of empty lines).\" -- -- You can also interpolate expressions into strings using @${...}@ syntax. For -- example: -- -- > $ dhall -- > let name = "John Doe" -- > let age = 21 -- > in "My name is ${name} and my age is ${Natural/show age}" -- > <Ctrl-D> -- > "My name is John Doe and my age is 21" -- -- Note that you can only interpolate expressions of type @Text@ -- -- If you need to insert a @"${"@ into a string without interpolation then use -- @"''${"@ (same as Nix) -- -- > '' -- > for file in *; do -- > echo "Found ''${file}" -- > done -- > '' -- $combine -- -- You can combine two records, using either the @(//)@ operator or the -- @(/\\)@ operator. -- -- The @(//)@ operator (or @(⫽)@ U+2AFD) combines the fields of both records, -- preferring fields from the right record if they share fields in common: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } // { baz = True } -- > <Ctrl-D> -- > { bar = "ABC", baz = True, foo = 1 } -- > $ dhall -- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode -- > <Ctrl-D> -- > { bar = True, foo = 1 } -- -- Note that the order of record fields does not matter. The compiler -- automatically sorts the fields. -- -- The @(/\\)@ operator (or @(∧)@ U+2227) also lets you combine records, but -- behaves differently if the records share fields in common. The operator -- combines shared fields recursively if they are both records: -- -- > $ dhall -- > { foo = { bar = True }, baz = "ABC" } /\ { foo = { qux = 1.0 } } -- > <Ctrl-D> -- > { baz = "ABC", foo = { bar = True, qux = 1.0 } } -- -- ... but fails with a type error if either shared field is not a record: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } ∧ { foo = True } -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: Field collision -- > -- > { foo = 1, bar = "ABC" } ∧ { foo = True } -- > -- > (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> -- > "haha" -- -- You can also annotate the types of values defined within a @let@ expression, -- like this: -- -- > $ dhall -- > let x : Text = "ha" in x ++ x -- > <Ctrl-D> -- > "haha" -- -- You need to nest @let@ expressions if you want to define more than one value -- in this way: -- -- > $ dhall -- > let x = "Hello, " -- > let y = "world!" -- > in x ++ y -- > <Ctrl-D> -- > "Hello, world!" -- -- Dhall is whitespace-insensitive, so feel free to format things over multiple -- lines or indent in any way that you please. -- -- If you want to define a named function, just give a name to an anonymous -- function: -- -- > $ dhall -- > let twice = λ(x : Text) → x ++ x in twice "ha" -- > <Ctrl-D> -- > "haha" -- -- Unlike Haskell, Dhall does not support function arguments on the left-hand -- side of the equals sign, so this will not work: -- -- > $ dhall -- > let twice (x : Text) = x ++ x in twice "ha" -- > <Ctrl-D> -- > Error: Invalid input -- > -- > (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://prelude.dhall-lang.org/Bool/not -- > in not True -- > <Ctrl-D> -- > False -- -- ... or to define synonyms for types: -- -- > $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name' -- > List Text -- > -- > [ "John", "Mary" ] -- -- __Exercise:__ What do you think the following code will normalize to? -- -- > let x = 1 -- > let x = 2 -- > in x -- -- Test your guess using the @dhall@ compiler -- -- __Exercise:__ Now try to guess what this code will normalize to: -- -- > let x = "ha" -- > let x = x ++ "ha" -- > in x -- -- __Exercise:__ What about this code? -- -- > let x = x ++ "ha" -- > in x -- $defaults -- -- For records with a large number of defaultable fields you can use the -- @::@ operator to auto-complete a record. For example: -- -- > let greet = -- > \(args : { greeting : Text, name : Text }) -- > -> "${args.greeting}, ${args.name}!" -- > -- > let Greeting = -- > { Type = { greeting : Text, name : Text } -- > , default = { greeting = "Hello", name = "John" } -- > } -- > -- > in '' -- > ${greet Greeting::{=}} -- > ${greet Greeting::{ greeting = "Hola" }} -- > ${greet Greeting::{ name = "Jane" }} -- > ${greet Greeting::{ greeting = "Hola", name = "Jane" }} -- > '' -- -- This operator is syntactic sugar. Specifically an expression of the form: -- -- > T::r -- -- ... is equivalent to: -- -- > (T.default // r) : T.Type -- -- So, for example: -- -- > Greeting::{ greeting = "Hola" } -- -- ... is the same thing as: -- -- > (Greeting.default // { greeting = "Hola" }) : Greeting.Type -- -- ... which is the same thing as: -- -- > ({ greeting = "Hello", name = "John" } // { greeting = "Hola" }) : { greeting : Text, name : Text } -- -- ... which is the same thing as: -- -- > { greeting = "Hola", name = "John" } -- $unions -- -- A union is a value that can be one of many alternative types of values. For -- example, the following union type: -- -- > < Left : Natural | Right : Bool > -- -- ... represents a value that can be either a @Natural@ or a @Bool@ value. If -- you are familiar with Haskell these are exactly analogous to Haskell's -- \"sum types\" and the above type is equivalent to @Either Natural Bool@. -- -- Each alternative is associated with a tag that distinguishes that alternative -- from other alternatives. In the above example, the @Left@ tag is used for -- the @Natural@ alternative and the @Right@ tag is used for the @Bool@ -- alternative. -- -- You can specify the value of a union constructor like this: -- -- > let Union = < Left : Natural | Right : Bool> -- > -- > in [ Union.Left 0, Union.Right True ] -- -- In other words, you can access a union constructor as a field of a union -- type and use that constructor to wrap a value of a type appropriate for -- that alternative. In the above example, the @Left@ constructor can wrap -- a @Natural@ value and the @Right@ constructor can wrap a @Bool@ value. We -- can also confirm that by inspecting their type: -- -- > $ echo '< Left : Natural | Right : Bool>' > ./Union -- -- > $ dhall --annotate <<< '(./Union).Left' -- > < Left : Natural | Right : Bool >.Left -- > : ∀(Left : Natural) → < Left : Natural | Right : Bool > -- -- > $ dhall --annotate <<< '(./Union).Right' -- > < Left : Natural | Right : Bool >.Right -- > : ∀(Right : Bool) → < Left : Natural | Right : Bool > -- -- In other words, the @Left@ constructor is a function from a @Natural@ to a -- value of our @Union@ type and the @Right@ constructor is a separate function -- from a @Bool@ to that same @Union@ type. -- -- You can consume a union using the built-in @merge@ function. For example, -- suppose we want to convert our union to a @Bool@ but we want to behave -- differently depending on whether or not the union is a @Natural@ wrapped in -- the @Left@ constructor or a @Bool@ wrapped in the @Right@ constructor . We -- would write: -- -- > $ cat > process <<EOF -- > λ(union : < Left : Natural | Right : Bool >) -- > → let handlers = -- > { Left = Natural/even -- Natural/even is a built-in function -- > , Right = λ(b : Bool) → b -- > } -- > in merge handlers union -- > EOF -- -- Now our @./process@ function can handle both alternatives: -- -- > $ dhall <<< './process ((./Union).Left 3)' -- > False -- -- > $ dhall <<< './process ((./Union).Right True)' -- > True -- -- Every @merge@ has the following form: -- -- > merge handlers union [ : type ] -- -- ... where: -- -- * @union@ is the union you want to consume -- * @handlers@ is a record with one function per alternative of the union -- * @type@ is an optional declared result type of the @merge@ -- -- The @merge@ function selects which function to apply from the record based on -- which alternative the union selects: -- -- > merge { Foo = f, ... } (< … >.Foo x) = f x -- -- So, for example: -- -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Left 3) -- > = Natural/even 3 -- > = False -- -- ... and similarly: -- -- > merge { Left = Natural/even, Right = λ(b : Bool) → b } (< Left : Natural | Right : Bool >.Right True) -- > = (λ(b : Bool) → b) True -- > = True -- -- Notice that each handler has to return the same type of result (@Bool@ in -- this case). -- -- You can also store more than one value within alternatives using Dhall's -- support for anonymous records. You can nest an anonymous record within a -- union such as in this type: -- -- > < Empty : {} | Person : { name : Text, age : Natural } > -- -- You can even go a step further and omit the type of an alternative if it -- stores no data, like this: -- -- > < Empty | Person : { name : Text, age : Natural } > -- -- The above Dhall type resembles the following equivalent Haskell data type: -- -- > data Example = Empty | Person { name :: Text, age :: Text } -- -- Empty alternatives like @Empty@ require no argument: -- -- > let Example = < Empty | Person : { name : Text, age : Natural } > -- > -- > in [ Example.Empty -- Note the absence of any argument to `Empty` -- > , Example.Person { name = "John", age = 23 } -- > , Example.Person { name = "Amy" , age = 25 } -- > ] -- -- ... and when you @merge@ an empty alternative the correspond handler takes no -- argument: -- -- > λ(x : < Empty | Person : { name : Text, age : Natural } >) -- > → merge -- > { Empty = "Unknown" -- Note the absence of 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 -- -- Let's ask the interpreter for the type of this function: -- the first line: -- -- > $ dhall type <<< './id' -- > ∀(a : Type) → ∀(x : a) → a -- -- You can read the type @(∀(a : Type) → ∀(x : a) → a)@ as saying: \"This is the -- type of a function whose first argument is named @a@ and is a @Type@. The -- second argument is named @x@ and has type @a@ (i.e. the value of the first -- argument). The result also has type @a@.\" -- -- This means that the type of the second argument changes depending on what -- type we provide for the first argument. When we apply @./id@ to @Natural@, -- we create a function that expects an @Natural@ argument: -- -- > $ dhall type <<< './id Natural' -- > ∀(x : Natural) → Natural -- -- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a -- @Bool@ argument: -- -- > $ dhall type <<< './id Bool' -- > ∀(x : Bool) → Bool -- -- We can then supply the final argument to each of those functions to show -- that they both work on their respective types: -- -- > $ dhall <<< './id Natural 4' -- > 4 -- -- > $ dhall <<< './id Bool True' -- > True -- -- Built-in functions can also be polymorphic, too. For example, we can ask -- the compiler for the type of @List/reverse@, the function that reverses a -- list: -- -- > $ dhall --annotate -- > List/reverse -- > <Ctrl-D> -- > List/reverse : ∀(a : Type) → List a → List a -- -- The first argument to @List/reverse@ is the type of the list to reverse: -- -- > $ dhall -- > List/reverse Bool -- > <Ctrl-D> -- > List/reverse Bool : List Bool → List Bool -- -- ... and the second argument is the list to reverse: -- -- > $ dhall -- > List/reverse Bool [True, False] -- > <Ctrl-D> -- > [False, True] -- -- Note that the second argument has no name. This type: -- -- > ∀(a : Type) → List a → List a -- -- ... is equivalent to this type: -- -- > ∀(a : Type) → ∀(_ : List a) → List a -- -- In other words, if you don't see the @∀@ symbol surrounding a function -- argument type then that means that the name of the argument is @"_"@. This -- is true even for user-defined functions: -- -- > $ dhall type <<< 'λ(_ : Text) → 1' -- > Text → Natural -- -- The type @Text → Natural@ is the same as @∀(_ : Text) → Natural@ -- -- __Exercise__ : Translate Haskell's `flip` function to Dhall -- $total -- -- Dhall is a total programming language, which means that Dhall is not -- Turing-complete and evaluation of every Dhall program is guaranteed to -- eventually halt. There is no upper bound on how long the program might take -- to evaluate, but the program is guaranteed to terminate in a finite amount of -- time and not hang forever. -- -- This guarantees that all Dhall programs can be safely reduced to a normal -- form where as many functions have been evaluated as possible. In fact, Dhall -- expressions can be evaluated even if all function arguments haven't been fully -- applied. For example, the following program is an anonymous function: -- -- > $ dhall -- > \(n : Bool) -> 10 * 10 -- > <Ctrl-D> -- > λ(n : Bool) → 100 -- -- ... and even though the function is still missing the first argument named -- @n@ the compiler is smart enough to evaluate the body of the anonymous -- function ahead of time before the function has even been invoked. -- -- We can use the @map@ function from the Prelude to illustrate an even more -- complex example: -- -- > $ dhall -- > let List/map = https://prelude.dhall-lang.org/List/map -- > in λ(f : Natural → Natural) → List/map Natural Natural f [1, 2, 3] -- > <Ctrl-D> -- > λ(f : Natural → Natural) → [f 1, f 2, f 3] -- -- Dhall can apply our function to each element of the list even before we specify -- which function to apply. -- -- The language will also never crash or throw any exceptions. Every -- computation will succeed and produce something, even if the result might be -- an @Optional@ value: -- -- > $ dhall <<< 'List/head Natural ([] : List Natural)' -- > None Natural -- -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: -- -- <https://prelude.dhall-lang.org/List/replicate> -- -- Test what the following Dhall expression normalizes to: -- -- > let replicate = https://prelude.dhall-lang.org/List/replicate -- > in replicate 10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" -- by finding an input expression that crashes or loops forever (and file a bug -- report if you succeed). -- $assertions -- -- You can add compile-time assertions which you can use to add tests to your -- code. For example, we can add some tests to our @not@ function like this: -- -- > let not -- > : Bool → Bool -- > = λ(b : Bool) → b == False -- > -- > let example0 = assert : not False === True -- > -- > let example1 = assert : not True === False -- > -- > in not -- -- The expression @assert : not False == True@ is a type-checking assertion -- that two expressions have the same normal form. If the two expressions differ -- then type-checking rejects the code. -- -- For example, suppose that we change the example to add an incorrect assertion: -- -- > -- ./test.dhall -- > -- > let not -- > : Bool → Bool -- > = λ(b : Bool) → b == False -- > -- > let example0 = assert : not False === True -- > -- > let example1 = assert : not True === True -- Oops! -- > -- > in not -- -- The type-checker then rejects the assertion with the following error message: -- -- > $ dhall <<< './test.dhall' -- > -- > ↳ ./test.dhall -- > -- > Error: Assertion failed -- > -- > - False -- > + True -- > -- > 7│ assert : not True === True -- Oops! -- > 8│ -- > -- > ./test.dhall:7:16 -- > -- > 1│ ./test.dhall -- > -- > (stdin):1:1 -- -- You can compare expressions that contain variables, too, which is equivalent -- to symbolic reasoning: -- -- > $ dhall <<< '\(n : Natural) -> assert : n === (n + 0)' -- > λ(n : Natural) → assert : n ≡ n -- -- Dhall accepts this because the language has built-in support for normalizing -- @n + 0@ to @n@, so both sides of the comparison normalize to the same value: -- @n@. -- -- Note that this sort of symbolic reasoning is limited and can only detect -- equality of normal forms. Some equivalent expressions will be rejected -- if they don't share the same normal form, such as these: -- -- > $ dhall <<< '\(n : Natural) -> assert : Natural/even (n + n) === True' -- > -- > Use "dhall --explain" for detailed errors -- > -- > n : Natural -- > -- > Error: Assertion failed -- > -- > - … … -- > + True -- > -- > 1│ assert : Natural/even (n + n) === True -- > -- > (stdin):1:19 -- -- Here the interpreter is not smart enough to simplify @Natural/even (n + n)@ -- to @True@ so the assertion fails. -- -- If you prefer to use Unicode, then the Unicode equivalent of @===@ is @≡@ -- (U+2261). -- $headers -- -- Sometimes you would like to provide additional request headers when importing -- Dhall expressions from URLs. For example, you might want to provide an -- authorization header or specify the expected content type. -- -- Dhall URL imports let you add or modify request headers with the @using@ -- keyword: -- -- > https://example.com/example.dhall using ./headers -- -- ... where you can replace @./headers@ with any import that points to a Dhall -- expression of the following type: -- -- > List { header : Text, value : Text } -- -- For example, if you needed to specify the content type correctly in order to -- download the file, then your @./headers@ file might look like this: -- -- > $ cat headers -- > [ { header = "Accept", value = "application/dhall" } ] -- -- ... or if you needed to provide an authorization token to access a private -- GitHub repository, then your headers could look like this: -- -- > [ { header = "Authorization", value = "token ${env:GITHUB_TOKEN as Text}" } ] -- -- This would read your GitHub API token from the @GITHUB_TOKEN@ environment -- variable and supply that token in the authorization header. -- -- You cannot inline the headers within the same file as the URL. You must -- provide them as a separate import. That means that this is /not/ legal code: -- -- > http://example.com/example.dhall using [ { header = "Accept", value = "application/dhall" } ] -- NOT legal -- -- Dhall will forward imports if you import an expression from a URL that -- contains a relative import. For example, if you import an expression like -- this: -- -- > http://example.com/example.dhall using ./headers -- -- ... and @http:\/\/example.com/example.dhall@ contains a relative import of @./foo@ -- then Dhall will import @http:\/\/example.com/foo@ using the same @./headers@ file. -- $integrity -- -- Sometimes you want to use share code while still ensuring that the imported -- value never changes and can't be corrupted by a malicious attacker. Dhall -- provides built-in support for hashing imported values to verify that their -- value never changes -- -- For example, suppose you save the following two files: -- -- > $ cat ./foo -- > ./bar sha256:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15 -- -- > $ cat ./bar -- > ./baz -- -- > $ cat ./baz -- > 1 -- -- The first file named @./foo@ contains an example of an integrity check. You -- can add @sha256:XXX@ after any import (such as after @./bar@), where @XXX@ is -- an expected 64-character @sha256@ hash of the Dhall value. To be precise, -- the hash represents a @sha256@ hash of the UTF-8 encoding of a canonical text -- representation of the fully resolved and normalized abstract syntax tree of -- the imported expression. -- -- Dhall will verify that the expected hash matches the actual hash of the -- imported Dhall value and reject the import if there is a hash mismatch: -- -- > $ dhall <<< './foo' -- > Natural -- > -- > 1 -- -- Any import protected by a semantic integrity check is automatically cached -- locally underneath either @~\/.cache\/dhall\/1220${HASH}@ or -- @${XDG_CACHE_HOME}\/dhall/1220${HASH}@ if you define the @XDG_CACHE_HOME@ -- environment variable. -- -- For example, after you import @./foo@ the contents of `./bar` are locally -- cached in a fully-evaluated and binary-encoded form which you can inspect by -- running: -- -- > $ dhall decode < ~/.cache/dhall/1220d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15 -- > 1 -- -- Subsequent attempts to resolve the same import will automatically retrieve -- the import from the cache. This matters less for local imports, but comes in -- handy for remote imports to avoid redownloading them. -- -- The local cache takes precedence when resolving imports, so changing the -- original import afterwards will have no affect until you update the hash. -- From Dhall's point of view, the hash is the true address and the file path -- is just a suggestion for how to obtain the import if it's not already cached. -- -- You can disable the cache by setting `XDG_CACHE_HOME` to `/var/empty` (an -- empty and unwritable directory), like this: -- -- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo' -- > Natural -- > -- > 1 -- -- We'll use this trick to test changes to the protected import in the following -- examples. -- -- Now, suppose you add a comment to the @./bar@ file: -- -- > $ cat ./bar -- > -- This comment does not change the hash -- > ./baz -- -- ... then @./foo@ will still successfully import @./bar@ because the hash -- only depends on the normalized value and does not depend on meaningless -- changes to whitespace or comments: -- -- > $ XDG_CACHE_HOME=/var/empty dhall <<< './foo' # This still succeeds -- > Natural -- > -- > 1 -- -- You can compute the Hash for any import by using the hash subcommand -- of this package. For example: -- -- > $ dhall hash <<< './bar' -- > sha256:d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15 -- -- Now suppose that you actually change the value of the @./baz@ file: -- -- > $ cat ./baz -- > 2 -- -- ... then the @./foo@ file will fail to import @./bar@, even though the -- text of the @./bar@ file technically never changed: -- -- > XDG_CACHE_HOME=/var/empty dhall <<< './foo' -- > -- > Error: Import integrity check failed -- > -- > Expected hash: -- > -- > ↳ d60d8415e36e86dae7f42933d3b0c4fe3ca238f057fba206c7e9fbf5d784fe15 -- > -- > Actual hash: -- > -- > ↳ 4caf97e8c445d4d4b5c5b992973e098ed4ae88a355915f5a59db640a589bc9cb -- -- This is because the @./bar@ file now represents a new value (@2@ instead of -- @1@), even though the text of the @./bar@ file is still the same. Since the -- value changed the hash must change as well. However, we could change @./baz@ -- to: -- -- > $ cat baz -- > if True then 1 else 2 -- -- ... and the import would now succeed again because the final result is @1@. -- -- The integrity hash ensures that your import's final meaning can never change, -- so an attacker can never compromise an imported value protected by a hash -- unless they can break SHA-256 encryption. The hash not only protects the -- file that you immediately import, but also protects every transitive import -- as well. -- -- You can also safely refactor your imported dependencies knowing that the -- refactor will not change your hash so long as your refactor is -- behavior-preserving. This provides an easy way to detect refactoring errors -- that you might accidentally introduce. The hash not only protects you -- from attackers, but also protects against human error, too! -- -- If you have a file which either doesn't already use hashed imports, -- or you changed some of the imports and want to update the hashes you can use the -- freeze command to either add or update hashes: -- -- > $ cat foo.dhall -- > let replicate = https://prelude.dhall-lang.org/List/replicate -- > in replicate 5 -- > $ -- > $ dhall freeze --inplace ./foo.dhall -- > $ cat ./foo.dhall -- > let replicate = -- > https://prelude.dhall-lang.org/List/replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347 -- > -- > in replicate 5 -- $rawText -- -- Sometimes you want to import the contents of a raw text file as a Dhall -- value of type `Text`. For example, one of the fields of a record might be -- the contents of a software license: -- -- > { package = "dhall" -- > , author = "Gabriel Gonzalez" -- > , license = ./LICENSE -- > } -- -- Normally if you wanted to import a text file you would need to wrap the -- contents of the file in double single-quotes, like this: -- -- > $ cat LICENSE -- > '' -- > Copyright (c) 2017 Gabriel Gonzalez -- > All rights reserved. -- > -- > ... -- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- > '' -- -- ... which does not work well if you need to reuse the same text file for -- other programs -- -- However, Dhall supports importing a raw text file by adding @as Text@ to the -- end of the import, like this: -- -- > { package = "dhall" -- > , author = "Gabriel Gonzalez" -- > , license = ./LICENSE as Text -- > } -- -- ... and then you can use the original text file unmodified: -- -- > $ cat LICENSE -- > Copyright (c) 2017 Gabriel Gonzalez -- > All rights reserved. -- > -- > ... -- > (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -- > SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- $format -- -- A format subcommand is also available that you can use to -- automatically format Dhall expressions. For example, we can take the -- following unformatted Dhall expression: -- -- > $ cat ./unformatted -- > λ(a : Type) → λ(kvss : List (List { index : Natural, value : a })) → -- > List/build { index : Natural, value : a } (λ(list : Type) → λ(cons : { -- > index : Natural, value : a } → list → list) → λ(nil : list) → -- > (List/fold (List { index : Natural, value : a }) kvss { count : Natural, diff : -- > Natural → list } (λ(kvs : List { index : Natural, value : a }) → λ(y : { -- > count : Natural, diff : Natural → list }) → { count = y.count + List/length -- > { index : Natural, value : a } kvs, diff = λ(n : Natural) → List/fold { -- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a -- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value } -- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count = -- > 0, diff = λ(_ : Natural) → nil }).diff 0) -- -- ... and run the expression through the formatter: -- -- > $ dhall format < ./unformatted -- > λ(a : Type) -- > → λ(kvss : List (List { index : Natural, value : a })) -- > → List/build -- > { index : Natural, value : a } -- > ( λ(list : Type) -- > → λ(cons : { index : Natural, value : a } → list → list) -- > → λ(nil : list) -- > → ( List/fold -- > (List { index : Natural, value : a }) -- > kvss -- > { count : Natural, diff : Natural → list } -- > ( λ(kvs : List { index : Natural, value : a }) -- > → λ(y : { count : Natural, diff : Natural → list }) -- > → { count = -- > y.count + List/length { index : Natural, value : a } kvs -- > , diff = -- > λ(n : Natural) -- > → List/fold -- > { index : Natural, value : a } -- > kvs -- > list -- > ( λ(kvOld : { index : Natural, value : a }) -- > → λ(z : list) -- > → cons -- > { index = kvOld.index + n, value = kvOld.value } -- > z -- > ) -- > ( y.diff -- > (n + List/length { index : Natural, value : a } kvs) -- > ) -- > } -- > ) -- > { count = 0, diff = λ(_ : Natural) → nil } -- > ).diff -- > 0 -- > ) -- -- The executable formats expressions without resolving, type-checking, or -- normalizing them: -- -- > $ dhall format -- > let replicate = https://prelude.dhall-lang.org/List/replicate -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D> -- > let replicate = https://prelude.dhall-lang.org/List/replicate -- > -- > in replicate -- > 5 -- > (List (List Natural)) -- > (replicate 5 (List Natural) (replicate 5 Natural 1)) -- -- You can also use the formatter to modify files in place using the -- @--inplace@ flag (i.e. for formatting source code): -- -- > $ dhall format --inplace ./unformatted -- -- Carefully note that the code formatter does not preserve all comments. -- Currently, the formatter only preserves two types of comments: -- -- * Leading comments at the beginning of the file -- * Comments within a @let@ binding -- -- For example: -- -- > $ dhall format -- > {- This comment will be preserved by the formatter -} -- > -- ... and this comment will be preserved, too -- > {- This comment will *NOT* be preserved -} 1 -- > -- ... and this comment will also *NOT* be preserved -- > <Ctrl-D> -- > {- This comment will be preserved by the formatter -} -- > -- ... and this comment will be preserved, too -- > 1 -- -- Also: -- -- > let {- This comment will be preserved -} -- > x {- This comment will also be preserved-} = -- > {- ... and this one will be preserved, too -} -- > 1 -- > -- > in x -- -- Note that you do not need to format the output of the -- @dhall@ interpreter. The interpreter already automatically formats -- multi-line expressions, too: -- -- > $ dhall -- > let replicate = https://prelude.dhall-lang.org/List/replicate -- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1)) -- > <Ctrl-D> -- > [ [ [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > ] -- > , [ [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > ] -- > , [ [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > ] -- > , [ [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > ] -- > , [ [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > , [ 1, 1, 1, 1, 1 ] -- > ] -- > ] -- $builtins -- -- Dhall is a restricted programming language that only supports simple built-in -- functions and operators. If you want to do anything fancier you will need to -- load your data into Haskell for further processing -- -- This section covers types, functions, and operators that are built into the -- language, meaning that you do not need to import any code to use them. -- Additionally, Dhall also comes with a Prelude (covered in the next section) -- hosted online that contains functions derived from these base utilities. The -- Prelude also re-exports all built-in functions for people who prefer -- consistency. -- -- The language provides built-in support for the following primitive types: -- -- * @Bool@ values -- * @Natural@ values -- * @Integer@ values -- * @Double@ values -- * @Text@ values -- -- ... as well as support for the following derived types: -- -- * @List@s of values -- * @Optional@ values -- * Anonymous records -- * Anonymous unions -- -- You can find an up-to-date list of available built-in functions and operators -- here: -- -- <https://github.com/dhall-lang/dhall-lang/wiki/Built-in-types%2C-functions%2C-and-operators Built-in types, functions, and operators> -- $caveats -- -- Dhall differs in a few important ways from other programming languages, so -- you should keep the following caveats in mind: -- -- First, Dhall only supports addition and multiplication on @Natural@ numbers -- (i.e. non-negative integers), which are not the same type of number as -- @Integer@s (which can be negative). An @Integer@ number is a number prefixed -- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading -- sign. If you try to add or multiply two @Integer@s you will get a type -- error: -- -- > $ dhall -- > +2 + +2 -- > <Ctrl-D> -- > Use "dhall --explain" for detailed errors -- > -- > Error: ❰+❱ only works on ❰Natural❱s -- > -- > +2 + +2 -- > -- > (stdin):1:1 -- -- In fact, there are no built-in functions for @Integer@s (or @Double@s) other -- than @Integer/show@ and @Double/show@. As far as the language is concerned -- they are opaque values that can only be shuffled around but not used in any -- meaningful way until they have been loaded into Haskell. -- -- Second, the equality @(==)@ and inequality @(!=)@ operators only work on -- @Bool@s. You cannot test any other types of values for equality. -- -- However, you can extend the language with your own built-ins using the -- Haskell API, as described in the next section. -- $extending -- -- You can use the Haskell API to extend the Dhall configuration language with -- new built-in functions. This section contains a simple Haskell recipe to add -- a new @Natural/equal@ built-in function of type: -- -- > Natural/equal : Natural → Natural → Bool -- -- To do so, we: -- -- * extend the type-checking context to include the type of @Natural/equal@ -- * extend the normalizer to evaluate all occurrences of @Natural/equal@ -- -- ... like this: -- -- > -- example.hs -- > -- > {-# LANGUAGE OverloadedStrings #-} -- > -- > module Main where -- > -- > import Dhall.Core (Expr(..), ReifiedNormalizer(..)) -- > -- > import qualified Data.Text.IO -- > import qualified Dhall -- > import qualified Dhall.Context -- > import qualified Lens.Family as Lens -- > -- > main :: IO () -- > main = do -- > text <- Data.Text.IO.getContents -- > -- > let startingContext = transform Dhall.Context.empty -- > where -- > transform = Dhall.Context.insert "Natural/equal" naturalEqualType -- > -- > naturalEqualType = -- > Pi "_" Natural (Pi "_" Natural Bool) -- > -- > let normalizer (App (App (Var "Natural/equal") (NaturalLit x)) (NaturalLit y)) = -- > Just (BoolLit (x == y)) -- > normalizer _ = -- > Nothing -- > -- > let inputSettings = transform Dhall.defaultInputSettings -- > where -- > transform = -- > Lens.set Dhall.normalizer (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) -- $prelude -- -- There is also a Prelude available at: -- -- <https://prelude.dhall-lang.org> -- -- If you visit the above link you can browse the Prelude, which has a few -- subdirectories. For example, the @Bool@ subdirectory has a @not@ file, which -- you can reference using this URL: -- -- <https://prelude.dhall-lang.org/Bool/not> -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents -- -- > $ $ dhall <<< 'https://prelude.dhall-lang.org/Bool/not as Text' -- > '' -- > {- -- > Flip the value of a `Bool` -- > -} -- > let not : Bool → Bool = λ(b : Bool) → b == False -- > -- > let example0 = assert : not True ≡ False -- > -- > let example1 = assert : not False ≡ True -- > -- > in not -- > '' -- -- The file could have been much shorter, like this: -- -- > λ(b : Bool) → b == False -- -- ... but all the functions exported from the Prelude try to be as -- self-documenting as possible by including: -- -- * the name of the function -- * the type of the function -- * documentation -- * tests -- -- The performance penalty for adding these helpful features is negligible, -- especially if you protect the import with a semantic integrity check because -- then the import would be cached compactly as @λ(_ : Bool) → _ == False@. -- -- You can use this @not@ function either directly: -- -- > $ dhall -- > https://prelude.dhall-lang.org/Bool/not True -- > <Ctrl-D> -- > False -- -- ... or assign the URL to a shorter name: -- -- > $ dhall -- > let Bool/not = https://prelude.dhall-lang.org/Bool/not -- > in Bool/not True -- > <Ctrl-D> -- > False -- -- Some functions in the Prelude just re-export built-in functions for -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: -- -- > $ dhall <<< 'https://prelude.dhall-lang.org/Natural/even as Text' -- > '' -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > -} -- > let even : Natural → Bool = Natural/even -- > -- > let example0 = assert : even 3 ≡ False -- > -- > let example1 = assert : even 0 ≡ True -- > -- > in even -- > '' -- -- You can also clone the Prelude locally to your filesystem if you prefer -- using `git clone`, like this: -- -- > $ git clone https://github.com/dhall-lang/dhall-lang.git -- > $ tree dhall-lang/Prelude -- > dhall-lang/Prelude -- > ├── Bool -- > │ ├── and -- > │ ├── build -- > │ ├── even -- > │ ├── fold -- > │ ├── not -- > │ ├── odd -- > │ ├── or -- > │ ├── package.dhall -- > │ └── show -- > ├── Double -- > │ ├── package.dhall -- > │ └── show -- > ├── Function -- > │ ├── compose -- > │ └── package.dhall -- > ├── Integer -- > │ ├── package.dhall -- > │ ├── show -- > │ └── toDouble -- > ├── JSON -- > │ ├── Nesting -- > │ ├── Tagged -- > │ ├── Type -- > │ ├── array -- > │ ├── bool -- > │ ├── keyText -- > │ ├── keyValue -- > │ ├── null -- > │ ├── number -- > │ ├── object -- > │ ├── package.dhall -- > │ ├── render -- > │ └── string -- > ├── List -- > │ ├── all -- > │ ├── any -- > │ ├── build -- > │ ├── concat -- > │ ├── concatMap -- > │ ├── default -- > │ ├── empty -- > │ ├── filter -- > │ ├── fold -- > │ ├── generate -- > │ ├── head -- > │ ├── indexed -- > │ ├── iterate -- > │ ├── last -- > │ ├── length -- > │ ├── map -- > │ ├── null -- > │ ├── package.dhall -- > │ ├── replicate -- > │ ├── reverse -- > │ ├── shifted -- > │ └── unzip -- > ├── Location -- > │ ├── Type -- > │ └── package.dhall -- > ├── Map -- > │ ├── Entry -- > │ ├── Type -- > │ ├── empty -- > │ ├── keyText -- > │ ├── keyValue -- > │ ├── keys -- > │ ├── map -- > │ ├── package.dhall -- > │ └── values -- > ├── Monoid -- > ├── Natural -- > │ ├── build -- > │ ├── enumerate -- > │ ├── equal -- > │ ├── even -- > │ ├── fold -- > │ ├── greaterThan -- > │ ├── greaterThanEqual -- > │ ├── isZero -- > │ ├── lessThan -- > │ ├── lessThanEqual -- > │ ├── odd -- > │ ├── package.dhall -- > │ ├── product -- > │ ├── show -- > │ ├── subtract -- > │ ├── sum -- > │ ├── toDouble -- > │ └── toInteger -- > ├── Optional -- > │ ├── all -- > │ ├── any -- > │ ├── build -- > │ ├── concat -- > │ ├── default -- > │ ├── filter -- > │ ├── fold -- > │ ├── head -- > │ ├── last -- > │ ├── length -- > │ ├── map -- > │ ├── null -- > │ ├── package.dhall -- > │ ├── toList -- > │ └── unzip -- > ├── Text -- > │ ├── concat -- > │ ├── concatMap -- > │ ├── concatMapSep -- > │ ├── concatSep -- > │ ├── default -- > │ ├── defaultMap -- > │ ├── package.dhall -- > │ └── show -- > ├── XML -- > │ ├── Type -- > │ ├── attribute -- > │ ├── element -- > │ ├── emptyAttributes -- > │ ├── leaf -- > │ ├── package.dhall -- > │ ├── render -- > │ └── text -- > └── package.dhall -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: -- -- <https://prelude.dhall-lang.org> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial -- -- You can also import the entire Prelude as a single large record for -- convenience: -- -- > $ dhall -- > let Prelude = https://prelude.dhall-lang.org/package.dhall -- > -- > in λ(x : Text) -- > → Prelude.List.length Text (Prelude.List.replicate 10 Text x) -- > <Ctrl-D> -- > ∀(x : Text) → Natural -- > -- > λ(x : Text) → 10 -- -- The organization of the package mirrors the layout of the Prelude, meaning -- that every directory is stored as a record whose children are the fields of -- that record. -- -- __Exercise__: Browse the Prelude by running: -- -- > $ dhall <<< 'https://prelude.dhall-lang.org/package.dhall' -- $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 languages that do not yet have Dhall integrations so that Dhall configuration files -- can be read into those languages, too. -- $faq -- -- <https://github.com/dhall-lang/dhall-lang/wiki/Frequently-Asked-Questions-(FAQ) Frequently Asked Questions (FAQ)>