dhall 1.0.0 → 1.0.1
raw patch · 9 files changed
+2644/−624 lines, 9 filesdep ~base
Dependency ranges changed: base
Files
- dhall.cabal +3/−10
- exec/Main.hs +1/−2
- src/Dhall.hs +182/−300
- src/Dhall/Context.hs +3/−3
- src/Dhall/Core.hs +190/−170
- src/Dhall/Import.hs +72/−60
- src/Dhall/Parser.hs +67/−55
- src/Dhall/Tutorial.hs +2090/−0
- src/Dhall/TypeCheck.hs +36/−24
dhall.cabal view
@@ -1,8 +1,8 @@ Name: dhall-Version: 1.0.0+Version: 1.0.1 Cabal-Version: >=1.8.0.2 Build-Type: Simple-Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2, GHC == 8.0.1+Tested-With: GHC == 7.10.2, GHC == 8.0.1 License: BSD3 License-File: LICENSE Copyright: 2016 Gabriel Gonzalez@@ -20,14 +20,6 @@ type-checks a Dhall file and reduces the file to a fully evaluated normal form. .- "Dhall.Core" contains the core syntax tree and evaluator- .- "Dhall.Import" contains logic for resolving remote file and URL references- .- "Dhall.TypeChecker" contains the type-checker- .- "Dhall.Parser" contains the parser- . Read "Dhall.Tutorial" to learn how to use this library Category: Compiler Source-Repository head@@ -61,6 +53,7 @@ Dhall.Core, Dhall.Import, Dhall.Parser,+ Dhall.Tutorial, Dhall.TypeCheck Executable dhall
exec/Main.hs view
@@ -62,7 +62,6 @@ handler2 e = do let _ = e :: SomeException- System.IO.hPutStrLn stderr "" System.IO.hPrint stderr e System.Exit.exitFailure @@ -73,7 +72,7 @@ Left err -> Control.Exception.throwIO err Right expr -> return expr - expr' <- load Nothing expr+ expr' <- load expr typeExpr <- case Dhall.TypeCheck.typeOf expr' of Left err -> Control.Exception.throwIO err
src/Dhall.hs view
@@ -7,296 +7,15 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} --- | Dhall is a programming language specialized for configuration files.------ The simplest possible 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 have the following configuration file:--- --- > $ cat config--- > < Example =--- > { foo = 1--- > , bar = [3.0, 4.0, 5.0] : List Double--- > }--- > >--- --- You can read the above configuration file into Haskell using the following--- code:--- --- > $ cat example.hs--- > {-# LANGUAGE DeriveGeneric #-}--- > {-# LANGUAGE OverloadedStrings #-}--- > --- > import Dhall--- > --- > data Example = Example { foo :: Integer , bar :: Vector Double }--- > deriving (Generic, Show)--- > --- > instance Interpret Example--- > --- > main :: IO ()--- > main = do--- > x <- input auto "./config"--- > print (x :: Example)--- --- If you compile and run the above program, the program prints the--- corresponding Haskell record:--- --- > $ ./example--- > Example {foo = 1, bar = [3.0,4.0,5.0]}------ In the above code, the @Example@ Haskell type represents the schema for our--- configuration file. Suppose that we modify our configuration file to no--- longer match the schema, like this:------ > $ echo "1" > config------ This then throws an exception when we try to load the configuration file:------ > $ ./example--- > example: --- > Expression: 1 : { bar : List Double, foo : Integer }--- > --- > Error: Expression's inferred type does not match annotated type--- > --- > Explanation: You can annotate the type or kind of an expression like this:--- > --- > x : t -- `x` is the expression and `t` is the annotated type or kind of `x`--- > --- > Annotations are introduced in one of two ways:--- > --- > * You can manually annotate expressions to declare the type or kind you expect--- > * The interpreter also implicitly inserts a top-level type annotation--- > --- > Annotations are optional because the compiler can infer the type of all--- > expressions. However, if you or the interpreter inserts an annotation and the--- > inferred type or kind does not match the annotation then type-checking fails.--- > --- > You or the interpreter annotated this expression:--- > ↳ 1--- > ... with this type or kind:--- > ↳ { bar : List Double, foo : Integer }--- > ... but the inferred type of the expression is actually this type or kind:--- > ↳ Integer------ The Dhall programming language is a statically typed language and the--- above error message is the output of the language's type-checker. Every--- expression we read into Haskell is type-checked against the expected schema.------ The above error message says that the type-checker expected a record with--- two fields: a field named @bar@ that is a `Vector` of `Double`s, and a--- field named @foo@ that is an `Integer`. However, the type-checker found an--- expression whose inferred type was an `Integer`. Since an `Integer` is not--- the same thing as a record the type-checking step fails and Dhall does not--- bother to marshal the configuration into Haskell.------ Dhall is also a heavily restricted programming language. For example, we can--- define a configuration file that is an anonymous function:------ > $ cat > makeBools--- > \(n : Bool) ->--- > [ n && True, n && False, n || True, n || False ] : List Bool--- > <Ctrl-D>------ You can read this as a function of one argument named @n@ of type `Bool`--- that returns a `Vector` of `Bool`s. Each element of the `Vector` depends--- on the input argument.------ This library comes with a command-line compiler named @dhall@ that you can--- use to type-check configuration files and convert them to a normal form. For--- example, we can ask the compiler what the type of our @makeBools@ file--- is:------ > $ dhall typecheck < makeBools--- > ∀(n : Bool) → List Bool------ This says that @makeBools@ is a function of one argument named @n@ of type--- `Bool` that returns a `Vector` of `Bool`s.------ We can apply our file to a `Bool` argument as if it were an ordinary--- function, like this:------ > {-# LANGUAGE OverloadedStrings #-}--- >--- > import Dhall--- >--- > main :: IO ()--- > main = do--- > x <- input auto "./makeBools True"--- > print (x :: Vector Bool)------ This produces the following output:------ > $ ./example--- > [True,False,True,True]------ Notice how we can decode into some types \"out-of-the-box\" without declaring--- a Haskell record to store the output. In the above example we marshalled--- the result directly into a `Vector` of `Bool`s. The instances for the--- `Interpret` class list all types that are automatically supported.------ We can also test functions directly on the command line using the @dhall@--- compiler. For example:------ > $ dhall--- > ./makeBools False--- > <Ctrl-D>--- > List Bool--- > --- > [False, False, True, False] : List Bool------ The @dhall@ compiler with no arguments produces two output lines:------ * The first output line is the type of the result--- * The second output line is the normal form of the expression that we input------ In the above example the type of the result is a `Vector` of `Bool`s and the--- normal form of the expression just evaluates all functions.------ You can also use the Dhall compiler to evaluate expressions which have no--- file references. For example:------ > $ dhall--- > "Hello, " <> "world!"--- > <Ctrl-D>--- > Text--- > --- > "Hello, world!"------ > $ dhall--- > +10 * +10--- > Natural--- > --- > +100------ Dhall is a very restricted programming language that only supports simple--- operations. For example, Dhall only support addition and subtraction on--- `Natural` numbers (i.e. non-negative numbers), which are not the same type of--- number as `Integer`s (which can be negative). A `Natural` number is a number--- prefixed with the @+@ symbol. If you try to add or multiply two `Integer`s--- (without the @+@ prefix) you will get a type error:------ > $ dhall--- > 2 + 2--- > <Ctrl-D>--- > dhall: --- > Expression: 2 + 2--- > --- > Error: Cannot use `(+)` on a value that's not a `Natural`--- > --- > Explanation: The `(+)` operator expects two arguments of type `Natural`--- > --- > You provided this argument:--- > --- > 2 + ...--- > --- > ... whose type is not `Natural`. The type is actually:--- > ↳ Integer--- > --- > An `Integer` is not the same thing as a `Natural` number. They are distinct--- > types: `Integer`s can be negative, but `Natural` numbers must be non-negative--- > --- > You can prefix an `Integer` literal with a `+` to create a `Natural` literal--- > --- > Example:--- > --- > +2 + ...------ The Dhall language doesn't just type-check the final schema; the language--- also ensures that every expression is internally consistent. For example,--- suppose that we call @./makeBools@ on a non-`Bool` argument:--------- > $ dhall--- > ./makeBools "ABC"--- > dhall: --- > Expression: (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) "ABC"--- > --- > Error: Function applied to the wrong type or kind of argument--- > --- > Explanation: Every function declares what type or kind of argument to accept--- > --- > λ(x : Bool) → x -- Anonymous function which only accepts `Bool` arguments--- > --- > let f (x : Bool) = x -- Named function which only accepts `Bool` arguments--- > in f True--- > --- > λ(a : Type) → a -- Anonymous function which only accepts `Type` arguments--- > --- > You *cannot* apply a function to the wrong type or kind of argument:--- > --- > (λ(x : Bool) → x) "A" -- "A" is `Text`, but the function expects a `Bool`--- > --- > You tried to invoke a function which expects an argument of type or kind:--- > ↳ Bool--- > ... on an argument of type or kind:--- > ↳ Text------ We get a type error saying that our function expects a `Bool` argument, but--- we supplied an argument of type `Text` instead.------ Our `input` function also doesn't need to reference any files at all:------ >>> input auto "True && False" :: IO Bool--- False------ Reading from an external configuration file is just a special case of Dhall's--- support for embedding files as expressions. There's no limit to how many--- files-as-expressions that you can nest this way. For example, we can define--- one file that is a Dhall expression that in turn depends on another file--- which is also a Dhall expression:------ > $ echo './bool1 && ./bool2' > both--- > $ echo 'True' > bool1--- > $ echo 'False' > bool2--- > $ dhall--- > [ ./bool1 , ./bool2 , ./both ] : List Bool--- > <Ctrl-D>--- > List Bool--- > --- > [ True, False, False ] : List Bool------ The only restriction is that the Dhall language will forbid cycles in these--- file references:------ > $ echo './bar' > foo--- > $ echo './foo' > bar--- > $ dhall < ./foo--- > dhall: --- > ⤷ ./bar --- > ⤷ ./foo --- > Cyclic import: ./bar ------ 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 all functions have been evaluated. 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.------ Similarly, you can use this normalization process to remove indirection--- introduced by well-meaning software engineers over-architecting the--- configuration file.+{-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining+ how to use the language, the compiler, and this library+-} module Dhall ( -- * Input input+ , detailed -- * Types , Type@@ -310,6 +29,7 @@ , vector -- * Re-exports+ , Natural , Text , Vector , Generic@@ -318,11 +38,14 @@ import Control.Applicative (empty, liftA2, (<|>)) import Control.Exception (Exception) import Data.Monoid ((<>))+import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text)+import Data.Typeable (Typeable) import Data.Vector (Vector) import Dhall.Core (Expr(..))+import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..))-import Dhall.TypeCheck (X)+import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) import GHC.Generics import Numeric.Natural (Natural) import Prelude hiding (maybe)@@ -370,12 +93,12 @@ input (Type {..}) text = do let delta = Directed "(input)" 0 0 0 0 expr <- throws (Dhall.Parser.exprFromText delta text)- expr' <- Dhall.Import.load Nothing expr+ expr' <- Dhall.Import.load expr let suffix = ( Data.ByteString.Lazy.toStrict . Data.Text.Lazy.Encoding.encodeUtf8 . Data.Text.Lazy.Builder.toLazyText- . Dhall.Core.buildExpr0+ . build ) expected let annot = case expr' of Note (Src begin end bytes) _ ->@@ -389,6 +112,121 @@ Just x -> return x Nothing -> fail "input: malformed `Type`" +{-| Use this to provide more detailed error messages++>> input auto "True" :: IO Integer+> *** Exception: Error: Expression doesn't match annotation+> +> True : Integer+> +> (input):1:1++>> detailed (input auto "True") :: IO Integer+> *** Exception: Error: Expression doesn't match annotation+> +> Explanation: You can annotate an expression with its type or kind using the+> ❰:❱ symbol, like this:+> +> +> ┌───────┐+> │ x : t │ ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱+> └───────┘+> +> The type checker verifies that the expression's type or kind matches the+> provided annotation+> +> For example, all of the following are valid annotations that the type checker+> accepts:+> +> +> ┌─────────────┐+> │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type+> └─────────────┘ checker accepts the annotation+> +> +> ┌────────────────────────┐+> │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type+> └────────────────────────┘ checker accepts the annotation+> +> +> ┌────────────────────┐+> │ List : Type → Type │ ❰List❱ is an expression that has kind ❰Type → Type❱,+> └────────────────────┘ so the type checker accepts the annotation+> +> +> ┌──────────────────┐+> │ List Text : Type │ ❰List Text❱ is an expression that has kind ❰Type❱, so+> └──────────────────┘ the type checker accepts the annotation+> +> +> However, the following annotations are not valid and the type checker will+> reject them:+> +> +> ┌──────────┐+> │ 1 : Text │ The type checker rejects this because ❰1❱ does not have type+> └──────────┘ ❰Text❱+> +> +> ┌─────────────┐+> │ List : Type │ ❰List❱ does not have kind ❰Type❱+> └─────────────┘+> +> +> You or the interpreter annotated this expression:+> +> ↳ True+> +> ... with this type or kind:+> +> ↳ Integer+> +> ... but the inferred type or kind of the expression is actually:+> +> ↳ Bool+> +> Some common reasons why you might get this error:+> +> ● The Haskell Dhall interpreter implicitly inserts a top-level annotation+> matching the expected type+> +> For example, if you run the following Haskell code:+> +> +> ┌───────────────────────────────┐+> │ >>> input auto "1" :: IO Text │+> └───────────────────────────────┘+> +> +> ... then the interpreter will actually type check the following annotated+> expression:+> +> +> ┌──────────┐+> │ 1 : Text │+> └──────────┘+> +> +> ... and then type-checking will fail+> +> ────────────────────────────────────────────────────────────────────────────────+> +> True : Integer+> +> (input):1:1++-}+detailed :: IO a -> IO a+detailed =+ Control.Exception.handle handler1 . Control.Exception.handle handler0+ where+ handler0 :: Imported (TypeError Src) -> IO a+ handler0 (Imported ps e) =+ Control.Exception.throwIO (Imported ps (DetailedTypeError e))++ handler1 :: TypeError Src -> IO a+ handler1 e = Control.Exception.throwIO (DetailedTypeError e)+ {-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall into Haskell @@ -479,8 +317,8 @@ {-| Decode a `Maybe` ->>> input (maybe integer) "[] : Maybe Integer"-Nothing+>>> input (maybe integer) "[1] : Optional Integer"+Just 1 -} maybe :: Type a -> Type (Maybe a) maybe (Type extractIn expectedIn) = Type extractOut expectedOut@@ -552,17 +390,47 @@ expected = Union Data.Map.empty -instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :+: g) where+instance (Constructor c1, Constructor c2, GenericInterpret f1, GenericInterpret f2) => GenericInterpret (M1 C c1 f1 :+: M1 C c2 f2) where genericAuto = Type {..} where- extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e)+ nL :: M1 i c1 f1 a+ nL = undefined - expected = Union (Data.Map.union expectedL expectedR)+ nR :: M1 i c2 f2 a+ nR = undefined + nameL = Data.Text.Lazy.pack (conName nL)+ nameR = Data.Text.Lazy.pack (conName nR)++ extract (UnionLit name e _)+ | name == nameL = fmap (L1 . M1) (extractL e)+ | name == nameR = fmap (R1 . M1) (extractR e)+ | otherwise = Nothing++ expected =+ Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])++ Type extractL expectedL = genericAuto+ Type extractR expectedR = genericAuto++instance (Constructor c, GenericInterpret (f :+: g), GenericInterpret h) => GenericInterpret ((f :+: g) :+: M1 C c h) where+ genericAuto = Type {..}+ where+ n :: M1 i c h a+ n = undefined++ name = Data.Text.Lazy.pack (conName n)++ extract u@(UnionLit name' e _)+ | name == name' = fmap (R1 . M1) (extractR e)+ | otherwise = fmap L1 (extractL u)++ expected = Union (Data.Map.insert name expectedR expectedL)+ Type extractL (Union expectedL) = genericAuto- Type extractR (Union expectedR) = genericAuto+ Type extractR expectedR = genericAuto -instance (Constructor c, GenericInterpret f) => GenericInterpret (M1 C c f) where+instance (Constructor c, GenericInterpret f, GenericInterpret (g :+: h)) => GenericInterpret (M1 C c f :+: (g :+: h)) where genericAuto = Type {..} where n :: M1 i c f a@@ -570,13 +438,27 @@ name = Data.Text.Lazy.pack (conName n) - extract (UnionLit name' e _)- | name == name' = fmap M1 (extract' e)- | otherwise = Nothing+ extract u@(UnionLit name' e _)+ | name == name' = fmap (L1 . M1) (extractL e)+ | otherwise = fmap R1 (extractR u) - expected = Union (Data.Map.singleton name expected')+ expected = Union (Data.Map.insert name expectedL expectedR) - Type extract' expected' = genericAuto+ Type extractL expectedL = genericAuto+ Type extractR (Union expectedR) = genericAuto++instance (GenericInterpret (f :+: g), GenericInterpret (h :+: i)) => GenericInterpret ((f :+: g) :+: (h :+: i)) where+ genericAuto = Type {..}+ where+ extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e)++ expected = Union (Data.Map.union expectedL expectedR)++ Type extractL (Union expectedL) = genericAuto+ Type extractR (Union expectedR) = genericAuto++instance GenericInterpret f => GenericInterpret (M1 C c f) where+ genericAuto = fmap M1 genericAuto instance GenericInterpret U1 where genericAuto = Type {..}
src/Dhall/Context.hs view
@@ -2,7 +2,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DeriveFunctor #-} --- | All `Context`-related operations+-- | This is a utility module that consolidates all `Context`-related operations module Dhall.Context ( -- * Context@@ -25,8 +25,8 @@ * You consume a `Context` using `lookup` and `toList` The difference between a `Context` and a `Map` is that a `Context` lets you- have multiple occurrences of the same key and you can query for the @n@th- occurrence of a given key.+ have multiple ordered occurrences of the same key and you can query for the+ @n@th occurrence of a given key. -} newtype Context a = Context { getContext :: [(Text, a)] } deriving (Functor)
src/Dhall/Core.hs view
@@ -8,8 +8,12 @@ {-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -Wall #-} --- | This module contains the core calculus for the Dhall language.+{-| This module contains the core calculus for the Dhall language. + Dhall is essentially a fork of the @morte@ compiler but with more built-in+ functionality, better error messages, and Haskell integration+-}+ module Dhall.Core ( -- * Syntax Const(..)@@ -22,29 +26,8 @@ , subst , shift - -- * Builders- -- $builders+ -- * Pretty-printing , pretty- , buildExpr0- , buildExpr1- , buildExpr2- , buildExpr3- , buildExpr4- , buildExpr5- , buildExpr6- , buildConst- , buildVar- , buildElems- , buildRecordLit- , buildFieldValues- , buildFieldValue- , buildRecord- , buildFieldTypes- , buildFieldType- , buildUnion- , buildAlternativeTypes- , buildAlternativeType- , buildUnionLit -- * Miscellaneous , internalError@@ -128,15 +111,15 @@ nearest bound variable and the index increases by one for each bound variable of the same name going outward. The following diagram may help: -> +-refers to-+-> | |-> v |-> \(x : *) -> \(y : *) -> \(x : *) -> x@0+> +---refers to--++> | |+> v |+> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0 >-> +-------------refers to-------------+-> | |-> v |-> \(x : *) -> \(y : *) -> \(x : *) -> x@1+> +------------------refers to-----------------++> | |+> v |+> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1 This `Int` behaves like a De Bruijn index in the special case where all variables have the same name.@@ -189,7 +172,7 @@ | BoolOr (Expr s a) (Expr s a) -- | > BoolEQ x y ~ x == y | BoolEQ (Expr s a) (Expr s a)- -- | > BoolNE x y ~ x /= y+ -- | > BoolNE x y ~ x != y | BoolNE (Expr s a) (Expr s a) -- | > BoolIf x y z ~ if x then y else z | BoolIf (Expr s a) (Expr s a) (Expr s a)@@ -389,8 +372,7 @@ where fromString str = Var (fromString str) -{- $builders- There is a one-to-one correspondence between the builders in this section+{- There is a one-to-one correspondence between the builders in this section and the sub-parsers in "Dhall.Parser". Each builder is named after the corresponding parser and the relationship between builders exactly matches the relationship between parsers. This leads to the nice emergent property@@ -425,228 +407,265 @@ buildText :: Builder -> Builder buildText a = build (show a) --- | Builder corresponding to the @Expr0@ parser in "Dhall.Parser"-buildExpr0 :: Buildable a => Expr s a -> Builder-buildExpr0 (Annot a b) = buildExpr1 a <> " : " <> buildExpr0 b-buildExpr0 (Note _ b) = buildExpr0 b-buildExpr0 a = buildExpr1 a+-- | Builder corresponding to the @expr@ parser in "Dhall.Parser"+buildExpr :: Buildable a => Expr s a -> Builder+buildExpr = buildExprA --- | Builder corresponding to the @Expr1@ parser in "Dhall.Parser"-buildExpr1 :: Buildable a => Expr s a -> Builder-buildExpr1 (Lam a b c) =+-- | Builder corresponding to the @exprA@ parser in "Dhall.Parser"+buildExprA :: Buildable a => Expr s a -> Builder+buildExprA (Annot a b) = buildExprB a <> " : " <> buildExprA b+buildExprA (Note _ b) = buildExprA b+buildExprA a = buildExprB a++-- | Builder corresponding to the @exprB@ parser in "Dhall.Parser"+buildExprB :: Buildable a => Expr s a -> Builder+buildExprB (Lam a b c) = "λ(" <> buildLabel a- <> " : "- <> buildExpr0 b- <> ") → "- <> buildExpr1 c-buildExpr1 (BoolIf a b c) =+ <> " : "+ <> buildExprA b+ <> ") → "+ <> buildExprB c+buildExprB (BoolIf a b c) = "if "- <> buildExpr0 a+ <> buildExprA a <> " then "- <> buildExpr1 b+ <> buildExprB b <> " else "- <> buildExpr1 c-buildExpr1 (Pi "_" b c) =- buildExpr2 b+ <> buildExprC c+buildExprB (Pi "_" b c) =+ buildExprC b <> " → "- <> buildExpr1 c-buildExpr1 (Pi a b c) =+ <> buildExprB c+buildExprB (Pi a b c) = "∀(" <> buildLabel a <> " : "- <> buildExpr0 b+ <> buildExprA b <> ") → "- <> buildExpr1 c-buildExpr1 (Let a Nothing c d) =+ <> buildExprB c+buildExprB (Let a Nothing c d) = "let " <> buildLabel a <> " = "- <> buildExpr0 c+ <> buildExprA c <> " in "- <> buildExpr1 d-buildExpr1 (Let a (Just b) c d) =+ <> buildExprB d+buildExprB (Let a (Just b) c d) = "let " <> buildLabel a <> " : "- <> buildExpr0 b+ <> buildExprA b <> " = "- <> buildExpr0 c+ <> buildExprA c <> " in "- <> buildExpr1 d-buildExpr1 (ListLit a b) =- "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExpr6 a-buildExpr1 (OptionalLit a b) =- "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExpr6 a-buildExpr1 (Merge a b c) =- "merge " <> buildExpr6 a <> " " <> buildExpr6 b <> " : " <> buildExpr5 c-buildExpr1 (Note _ b) =- buildExpr1 b-buildExpr1 a =- buildExpr2 a+ <> buildExprB d+buildExprB (ListLit a b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExprE a+buildExprB (OptionalLit a b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExprE a+buildExprB (Merge a b c) =+ "merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c+buildExprB (Note _ b) =+ buildExprB b+buildExprB a =+ buildExprC a --- | Builder corresponding to the @Expr2@ parser in "Dhall.Parser"-buildExpr2 :: Buildable a => Expr s a -> Builder-buildExpr2 (BoolEQ a b) = buildExpr2 a <> " == " <> buildExpr2 b-buildExpr2 (BoolNE a b) = buildExpr2 a <> " /= " <> buildExpr2 b-buildExpr2 (Note _ b) = buildExpr2 b-buildExpr2 a = buildExpr3 a+-- | Builder corresponding to the @exprC@ parser in "Dhall.Parser"+buildExprC :: Buildable a => Expr s a -> Builder+buildExprC = buildExprC0 --- | Builder corresponding to the @Expr3@ parser in "Dhall.Parser"-buildExpr3 :: Buildable a => Expr s a -> Builder-buildExpr3 (BoolOr a b) = buildExpr3 a <> " || " <> buildExpr3 b-buildExpr3 (NaturalPlus a b) = buildExpr3 a <> " + " <> buildExpr3 b-buildExpr3 (TextAppend a b) = buildExpr3 a <> " ++ " <> buildExpr3 b-buildExpr3 (Note _ b) = buildExpr3 b-buildExpr3 a = buildExpr4 a+-- | Builder corresponding to the @exprC0@ parser in "Dhall.Parser"+buildExprC0 :: Buildable a => Expr s a -> Builder+buildExprC0 (BoolOr a b) = buildExprC1 a <> " || " <> buildExprC0 b+buildExprC0 (Note _ b) = buildExprC0 b+buildExprC0 a = buildExprC1 a --- | Builder corresponding to the @Expr4@ parser in "Dhall.Parser"-buildExpr4 :: Buildable a => Expr s a -> Builder-buildExpr4 (BoolAnd a b) = buildExpr4 a <> " && " <> buildExpr4 b-buildExpr4 (NaturalTimes a b) = buildExpr4 a <> " * " <> buildExpr4 b-buildExpr4 (Combine a b) = buildExpr4 a <> " ∧ " <> buildExpr4 b-buildExpr4 (Note _ b) = buildExpr4 b-buildExpr4 a = buildExpr5 a+-- | Builder corresponding to the @exprC1@ parser in "Dhall.Parser"+buildExprC1 :: Buildable a => Expr s a -> Builder+buildExprC1 (TextAppend a b) = buildExprC2 a <> " ++ " <> buildExprC1 b+buildExprC1 (Note _ b) = buildExprC1 b+buildExprC1 a = buildExprC2 a --- | Builder corresponding to the @Expr5@ parser in "Dhall.Parser"-buildExpr5 :: Buildable a => Expr s a -> Builder-buildExpr5 (App a b) = buildExpr5 a <> " " <> buildExpr6 b-buildExpr5 (Note _ b) = buildExpr5 b-buildExpr5 a = buildExpr6 a+-- | Builder corresponding to the @exprC2@ parser in "Dhall.Parser"+buildExprC2 :: Buildable a => Expr s a -> Builder+buildExprC2 (NaturalPlus a b) = buildExprC3 a <> " + " <> buildExprC2 b+buildExprC2 (Note _ b) = buildExprC2 b+buildExprC2 a = buildExprC3 a --- | Builder corresponding to the @Expr6@ parser in "Dhall.Parser"-buildExpr6 :: Buildable a => Expr s a -> Builder-buildExpr6 (Var a) =+-- | Builder corresponding to the @exprC3@ parser in "Dhall.Parser"+buildExprC3 :: Buildable a => Expr s a -> Builder+buildExprC3 (BoolAnd a b) = buildExprC4 a <> " && " <> buildExprC3 b+buildExprC3 (Note _ b) = buildExprC3 b+buildExprC3 a = buildExprC4 a++-- | Builder corresponding to the @exprC4@ parser in "Dhall.Parser"+buildExprC4 :: Buildable a => Expr s a -> Builder+buildExprC4 (Combine a b) = buildExprC5 a <> " ∧ " <> buildExprC4 b+buildExprC4 (Note _ b) = buildExprC4 b+buildExprC4 a = buildExprC5 a++-- | Builder corresponding to the @exprC5@ parser in "Dhall.Parser"+buildExprC5 :: Buildable a => Expr s a -> Builder+buildExprC5 (NaturalTimes a b) = buildExprC6 a <> " * " <> buildExprC5 b+buildExprC5 (Note _ b) = buildExprC5 b+buildExprC5 a = buildExprC6 a++-- | Builder corresponding to the @exprC6@ parser in "Dhall.Parser"+buildExprC6 :: Buildable a => Expr s a -> Builder+buildExprC6 (BoolEQ a b) = buildExprC7 a <> " == " <> buildExprC6 b+buildExprC6 (Note _ b) = buildExprC6 b+buildExprC6 a = buildExprC7 a++-- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser"+buildExprC7 :: Buildable a => Expr s a -> Builder+buildExprC7 (BoolNE a b) = buildExprD a <> " != " <> buildExprC7 b+buildExprC7 (Note _ b) = buildExprC7 b+buildExprC7 a = buildExprD a++-- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"+buildExprD :: Buildable a => Expr s a -> Builder+buildExprD (App a b) = buildExprD a <> " " <> buildExprE b+buildExprD (Note _ b) = buildExprD b+buildExprD a = buildExprE a++-- | Builder corresponding to the @exprE@ parser in "Dhall.Parser"+buildExprE :: Buildable a => Expr s a -> Builder+buildExprE (Field a b) = buildExprE a <> "." <> buildLabel b+buildExprE (Note _ b) = buildExprE b+buildExprE a = buildExprF a++-- | Builder corresponding to the @exprF@ parser in "Dhall.Parser"+buildExprF :: Buildable a => Expr s a -> Builder+buildExprF (Var a) = buildVar a-buildExpr6 (Const k) =+buildExprF (Const k) = buildConst k-buildExpr6 Bool =+buildExprF Bool = "Bool"-buildExpr6 Natural =+buildExprF Natural = "Natural"-buildExpr6 NaturalFold =+buildExprF NaturalFold = "Natural/fold"-buildExpr6 NaturalBuild =+buildExprF NaturalBuild = "Natural/build"-buildExpr6 NaturalIsZero =+buildExprF NaturalIsZero = "Natural/isZero"-buildExpr6 NaturalEven =+buildExprF NaturalEven = "Natural/even"-buildExpr6 NaturalOdd =+buildExprF NaturalOdd = "Natural/odd"-buildExpr6 Integer =+buildExprF Integer = "Integer"-buildExpr6 Double =+buildExprF Double = "Double"-buildExpr6 Text =+buildExprF Text = "Text"-buildExpr6 List =+buildExprF List = "List"-buildExpr6 ListBuild =+buildExprF ListBuild = "List/build"-buildExpr6 ListFold =+buildExprF ListFold = "List/fold"-buildExpr6 ListLength =+buildExprF ListLength = "List/length"-buildExpr6 ListHead =+buildExprF ListHead = "List/head"-buildExpr6 ListLast =+buildExprF ListLast = "List/last"-buildExpr6 ListIndexed =+buildExprF ListIndexed = "List/indexed"-buildExpr6 ListReverse =+buildExprF ListReverse = "List/reverse"-buildExpr6 Optional =+buildExprF Optional = "Optional"-buildExpr6 OptionalFold =+buildExprF OptionalFold = "Optional/fold"-buildExpr6 (BoolLit True) =+buildExprF (BoolLit True) = "True"-buildExpr6 (BoolLit False) =+buildExprF (BoolLit False) = "False"-buildExpr6 (IntegerLit a) =+buildExprF (IntegerLit a) = buildNumber a-buildExpr6 (NaturalLit a) =+buildExprF (NaturalLit a) = "+" <> buildNatural a-buildExpr6 (DoubleLit a) =+buildExprF (DoubleLit a) = buildDouble a-buildExpr6 (TextLit a) =+buildExprF (TextLit a) = buildText a-buildExpr6 (Record a) =+buildExprF (Record a) = buildRecord a-buildExpr6 (RecordLit a) =+buildExprF (RecordLit a) = buildRecordLit a-buildExpr6 (Union a) =+buildExprF (Union a) = buildUnion a-buildExpr6 (UnionLit a b c) =+buildExprF (UnionLit a b c) = buildUnionLit a b c-buildExpr6 (Embed a) =+buildExprF (Embed a) = build a-buildExpr6 (Field a b) =- buildExpr6 a <> "." <> buildLabel b-buildExpr6 (Note _ b) =- buildExpr6 b-buildExpr6 a =- "(" <> buildExpr0 a <> ")"+buildExprF (Note _ b) =+ buildExprF b+buildExprF a =+ "(" <> buildExprA a <> ")" --- | Builder corresponding to the @Const@ parser in "Dhall.Parser"+-- | Builder corresponding to the @const@ parser in "Dhall.Parser" buildConst :: Const -> Builder buildConst Type = "Type" buildConst Kind = "Kind" --- | Builder corresponding to the @Var@ parser in "Dhall.Parser"+-- | Builder corresponding to the @var@ parser in "Dhall.Parser" buildVar :: Var -> Builder buildVar (V x 0) = buildLabel x buildVar (V x n) = buildLabel x <> "@" <> buildNumber n --- | Builder corresponding to the @Elems@ parser in "Dhall.Parser"+-- | Builder corresponding to the @elems@ parser in "Dhall.Parser" buildElems :: Buildable a => [Expr s a] -> Builder buildElems [] = ""-buildElems [a] = buildExpr0 a-buildElems (a:bs) = buildExpr0 a <> ", " <> buildElems bs+buildElems [a] = buildExprA a+buildElems (a:bs) = buildExprA a <> ", " <> buildElems bs --- | Builder corresponding to the @RecordLit@ parser in "Dhall.Parser"+-- | Builder corresponding to the @recordLit@ parser in "Dhall.Parser" buildRecordLit :: Buildable a => Map Text (Expr s a) -> Builder buildRecordLit a | Data.Map.null a = "{=}" buildRecordLit a = "{ " <> buildFieldValues (Data.Map.toList a) <> " }" --- | Builder corresponding to the @FieldValues@ parser in "Dhall.Parser"+-- | Builder corresponding to the @fieldValues@ parser in "Dhall.Parser" buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder buildFieldValues [] = "" buildFieldValues [a] = buildFieldValue a buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs --- | Builder corresponding to the @FieldValue@ parser in "Dhall.Parser"+-- | Builder corresponding to the @fieldValue@ parser in "Dhall.Parser" buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder-buildFieldValue (a, b) = buildLabel a <> " = " <> buildExpr0 b+buildFieldValue (a, b) = buildLabel a <> " = " <> buildExprA b --- | Builder corresponding to the @Record@ parser in "Dhall.Parser"+-- | Builder corresponding to the @record@ parser in "Dhall.Parser" buildRecord :: Buildable a => Map Text (Expr s a) -> Builder buildRecord a | Data.Map.null a = "{}" buildRecord a = "{ " <> buildFieldTypes (Data.Map.toList a) <> " }" --- | Builder corresponding to the @FieldTypes@ parser in "Dhall.Parser"+-- | Builder corresponding to the @fieldTypes@ parser in "Dhall.Parser" buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder buildFieldTypes [] = "" buildFieldTypes [a] = buildFieldType a buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs --- | Builder corresponding to the @FieldType@ parser in "Dhall.Parser"+-- | Builder corresponding to the @fieldType@ parser in "Dhall.Parser" buildFieldType :: Buildable a => (Text, Expr s a) -> Builder-buildFieldType (a, b) = buildLabel a <> " : " <> buildExpr0 b+buildFieldType (a, b) = buildLabel a <> " : " <> buildExprA b --- | Builder corresponding to the @Union@ parser in "Dhall.Parser"+-- | Builder corresponding to the @union@ parser in "Dhall.Parser" buildUnion :: Buildable a => Map Text (Expr s a) -> Builder buildUnion a | Data.Map.null a = "<>" buildUnion a = "< " <> buildAlternativeTypes (Data.Map.toList a) <> " >" --- | Builder corresponding to the @AlternativeTypes@ parser in "Dhall.Parser"+-- | Builder corresponding to the @alternativeTypes@ parser in "Dhall.Parser" buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder buildAlternativeTypes [] = ""@@ -655,24 +674,24 @@ buildAlternativeTypes (a:bs) = buildAlternativeType a <> " | " <> buildAlternativeTypes bs --- | Builder corresponding to the @AlternativeType@ parser in "Dhall.Parser"+-- | Builder corresponding to the @alternativeType@ parser in "Dhall.Parser" buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder-buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExpr0 b+buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExprA b --- | Builder corresponding to the @UnionLit@ parser in "Dhall.Parser"+-- | Builder corresponding to the @unionLit@ parser in "Dhall.Parser" buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder buildUnionLit a b c | Data.Map.null c = "< " <> buildLabel a <> " = "- <> buildExpr0 b+ <> buildExprA b <> " >" | otherwise = "< " <> buildLabel a <> " = "- <> buildExpr0 b+ <> buildExprA b <> " | " <> buildAlternativeTypes (Data.Map.toList c) <> " >"@@ -680,7 +699,7 @@ -- | Generates a syntactically valid Dhall program instance Buildable a => Buildable (Expr s a) where- build = buildExpr0+ build = buildExpr {-| `shift` is used by both normalization and type-checking to avoid variable capture by shifting variable indices@@ -1240,17 +1259,15 @@ where v' = normalize v kvs' = fmap normalize kvs- Combine x y ->- case x of- RecordLit kvsX ->- case y of+ Combine x0 y0 ->+ let combine x y = case x of+ RecordLit kvsX -> case y of RecordLit kvsY ->- RecordLit (fmap normalize (Data.Map.union kvsX kvsY))- _ -> Combine x' y'- _ -> Combine x' y'- where- x' = normalize x- y' = normalize y+ let kvs = Data.Map.unionWith combine kvsX kvsY+ in RecordLit (fmap normalize kvs)+ _ -> Combine x y+ _ -> Combine x y+ in combine (normalize x0) (normalize y0) Merge x y t -> case x' of RecordLit kvsX ->@@ -1284,6 +1301,9 @@ text = "normalize (" <> Data.Text.pack (show e'') <> ")" +{-| Utility function used to throw internal errors that should never happen+ (in theory) but that are not enforced by the type system+-} internalError :: Data.Text.Text -> forall b . b internalError text = error (Data.Text.unpack [NeatInterpolation.text| Error: Compiler bug
src/Dhall/Import.hs view
@@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE QuasiQuotes #-} {-# OPTIONS_GHC -Wall #-} {-| Dhall lets you import external expressions located either in local files or@@ -9,48 +8,40 @@ To import a local file as an expression, just insert the path to the file, prepending a @./@ if the path is relative to the current directory. For- example, suppose we had the following three local files:-- > -- id- > \(a : *) -> \(x : a) -> x-- > -- Bool- > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool-- > -- True- > \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True-- You could then reference them within a Dhall expression using this syntax:-- > ./id ./Bool ./True-- ... which would embed their expressions directly within the syntax tree:+ example, if you create a file named @id@ with the following contents: - > -- ... expands out to:- > (\(a : *) -> \(x : a) -> x)- > (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True)- > (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True)+ > $ cat id+ > λ(a : Type) → λ(x : a) → x - ... and which normalizes to:+ Then you can use the file directly within a @dhall@ program just by+ referencing the file's path: - > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True+ > $ dhall+ > ./id Bool True+ > <Ctrl-D>+ > Bool+ > + > True Imported expressions may contain imports of their own, too, which will continue to be resolved. However, Dhall will prevent cyclic imports. For example, if you had these two files: - > -- foo+ > $ cat foo > ./bar - > -- bar+ > $ cat bar > ./foo ... Dhall would throw the following exception if you tried to import @foo@: - > dhall: - > ⤷ ./foo- > ⤷ ./bar- > Cyclic import: ./foo+ > $ dhall+ > ./foo+ > ^D+ > ↳ ./foo + > ↳ ./bar + > + > Cyclic import: ./foo You can also import expressions hosted on network endpoints. Just use the URL@@ -72,12 +63,14 @@ module Dhall.Import ( -- * Import- load- , exprFromFile+ exprFromFile , exprFromURL+ , load , Cycle(..) , ReferentiallyOpaque(..) , Imported(..)+ , PrettyHttpException(..)+ , MissingFile(..) ) where import Control.Exception@@ -109,17 +102,15 @@ import qualified Control.Monad.Trans.State.Strict as State import qualified Data.ByteString.Lazy-import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Map.Strict as Map-import qualified Data.Text import qualified Data.Text.Lazy as Text import qualified Data.Text.Lazy.Builder as Builder import qualified Data.Text.Lazy.Encoding import qualified Dhall.Parser import qualified Dhall.TypeCheck+import qualified Filesystem import qualified Filesystem.Path.CurrentOS-import qualified NeatInterpolation import qualified Network.HTTP.Client as HTTP import qualified Network.HTTP.Client.TLS as HTTP import qualified Filesystem.Path.CurrentOS as Filesystem@@ -139,7 +130,7 @@ instance Exception Cycle instance Show Cycle where- show (Cycle path) = "Cyclic import: " ++ builderToString (build path)+ show (Cycle path) = "\nCyclic import: " ++ builderToString (build path) {-| Dhall tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will@@ -175,7 +166,7 @@ instance Show ReferentiallyOpaque where show (ReferentiallyOpaque path) =- "Referentially opaque import: " ++ builderToString (build path)+ "\nReferentially opaque import: " ++ builderToString (build path) -- | Extend another exception with the current import stack data Imported e = Imported@@ -187,23 +178,47 @@ instance Show e => Show (Imported e) where show (Imported paths e) =- unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths')- ++ "\n"+ (case paths of [] -> ""; _ -> "\n")+ ++ unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths') ++ show e where -- Canonicalize all paths paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths))) +-- | Newtype used to wrap `HttpException`s with a prettier `Show` instance newtype PrettyHttpException = PrettyHttpException HttpException deriving (Typeable) instance Exception PrettyHttpException instance Show PrettyHttpException where- show (PrettyHttpException (FailedConnectionException2 _ _ _ _)) =- "\ESC[1;31mError\ESC[0m: Connection timed out\n"- show (PrettyHttpException e) = show e+ show (PrettyHttpException e) = case e of+ FailedConnectionException2 _ _ _ e' ->+ "\n"+ <> "\ESC[1;31mError\ESC[0m: Wrong host\n"+ <> "\n"+ <> "↳ " <> show e'+ InvalidDestinationHost host ->+ "\n"+ <> "\ESC[1;31mError\ESC[0m: Invalid host name\n"+ <> "\n"+ <> "↳ " <> show host+ ResponseTimeout ->+ "\ESC[1;31mError\ESC[0m: The host took too long to respond\n"+ e' -> "\n"+ <> show e' +-- | Exception thrown when an imported file is missing+data MissingFile = MissingFile+ deriving (Typeable)++instance Exception MissingFile++instance Show MissingFile where+ show MissingFile =+ "\n"+ <> "\ESC[1;31mError\ESC[0m: Missing file\n"+ data Status = Status { _stack :: [Path] , _cache :: Map Path (Expr Src X)@@ -335,17 +350,23 @@ -- confusion Text.Trifecta.parseFromFileEx parser string' `onException` throwIO e + exists <- Filesystem.isFile path+ if exists+ then return ()+ else Control.Exception.throwIO MissingFile+ x <- Text.Trifecta.parseFromFileEx parser string `catch` handler case x of Failure errInfo -> throwIO (ParseError (Text.Trifecta._errDoc errInfo)) Success expr -> return expr where- parser = do+ parser = unParser (do Text.Parser.Token.whiteSpace- r <- unParser Dhall.Parser.exprA+ r <- Dhall.Parser.expr Text.Parser.Combinators.eof- return r+ return r ) +-- | Parse an expression from a URL hosting a Dhall program exprFromURL :: Manager -> Text -> IO (Expr Src Path) exprFromURL m url = do request <- HTTP.parseUrlThrow (Text.unpack url)@@ -389,11 +410,11 @@ Success expr -> return expr Success expr -> return expr where- parser = do+ parser = unParser (do Text.Parser.Token.whiteSpace- r <- unParser Dhall.Parser.exprA+ r <- Dhall.Parser.expr Text.Parser.Combinators.eof- return r+ return r ) {-| Load a `Path` as a \"dynamic\" expression (without resolving any imports) @@ -470,17 +491,8 @@ return expr -{-| Resolve all imports within an expression-- By default the starting path is the current directory, but you can override- the starting path with a file if you read in the expression from that file--}-load- :: Maybe Path- -- ^ Starting path- -> Expr Src Path- -- ^ Expression to resolve- -> IO (Expr Src X)-load here expr = State.evalStateT (fmap join (traverse loadStatic expr)) status+-- | Resolve all imports within an expression+load :: Expr Src Path -> IO (Expr Src X)+load expr = State.evalStateT (fmap join (traverse loadStatic expr)) status where- status = Status (Foldable.toList here) Map.empty Nothing+ status = Status [] Map.empty Nothing
src/Dhall/Parser.hs view
@@ -2,12 +2,14 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-} +-- | This module contains Dhall's parsing logic+ module Dhall.Parser ( -- * Utilities exprFromText -- * Parsers- , exprA+ , expr -- * Types , Src(..)@@ -62,6 +64,7 @@ import qualified Text.Trifecta.Combinators import qualified Text.Trifecta.Delta +-- | Source code extract data Src = Src Delta Delta ByteString deriving (Show) instance Buildable Src where@@ -75,6 +78,10 @@ text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes') +{-| A `Parser` that is almost identical to+ @"Text.Trifecta".`Text.Trifecta.Parser`@ except treating Haskell-style+ comments as whitespace+-} newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a } deriving ( Functor@@ -195,6 +202,10 @@ label :: Parser Text label = Text.Parser.Token.ident identifierStyle <?> "label" +-- | Parser for a top-level Dhall expression+expr :: Parser (Expr Src Path)+expr = exprA+ exprA :: Parser (Expr Src Path) exprA = do a <- exprB@@ -302,26 +313,21 @@ reserve "Optional" return OptionalLit --- TODO: Add `noted` in the right places here exprC :: Parser (Expr Src Path)-exprC = expressionParser+exprC = exprC0 where- expressionParser = Text.Parser.Expression.buildExpressionParser- [ [ operator BoolAnd (symbol "&&")- , operator NaturalTimes (symbol "*" )- , operator Combine combine- ]- , [ operator BoolOr (symbol "||")- , operator TextAppend (symbol "++")- , operator NaturalPlus (symbol "+" )- ]- , [ operator BoolEQ (symbol "==")- , operator BoolNE (symbol "/=")- ]- ]- exprD+ chain pA pOp op pB = noted (do+ a <- pA+ try (do pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a ) - operator op parser = Infix (do parser; return op) AssocRight+ exprC0 = chain exprC1 (symbol "||") BoolOr exprC0+ exprC2 = chain exprC3 (symbol "++") TextAppend exprC2+ exprC1 = chain exprC2 (symbol "+" ) NaturalPlus exprC1+ exprC3 = chain exprC4 (symbol "&&") BoolAnd exprC3+ exprC4 = chain exprC5 combine Combine exprC4+ exprC5 = chain exprC6 (symbol "*" ) NaturalTimes exprC5+ exprC6 = chain exprC7 (symbol "==") BoolEQ exprC6+ exprC7 = chain exprD (symbol "!=") BoolNE exprC7 -- We can't use left-recursion to define `exprD` otherwise the parser will -- loop infinitely. However, I'd still like to use left-recursion in the@@ -333,43 +339,25 @@ -- arguments exprD :: Parser (Expr Src Path) exprD = do- es <- some (noted exprE)+ es <- some (noted (try exprE)) let app nL@(Note (Src before _ bytesL) eL) nR@(Note (Src _ after bytesR) eR) = Note (Src before after (bytesL <> bytesR)) (App nL nR) app _ _ = Dhall.Core.internalError- ("exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")")+ ("Dhall.Parser.exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")") return (Data.List.foldl1 app es) exprE :: Parser (Expr Src Path) exprE = noted (do a <- exprF- b <- many (do+ b <- many (try (do symbol "."- label )+ label )) return (Data.List.foldl Field a b) ) exprF :: Parser (Expr Src Path) exprF = choice- [ noted exprF01- , noted exprF03- , noted exprF04- , noted exprF05- , noted exprF06- , noted exprF07- , noted exprF12- , noted exprF13- , noted exprF14- , noted exprF15- , noted exprF16- , noted exprF17- , noted exprF18- , noted exprF20- , noted exprF19- , noted exprF21- , noted exprF22+ [ noted (try exprF26) , noted (try exprF25)- , noted exprF23- , noted (try exprF26) , noted exprF24 , noted exprF27 , noted (try exprF28)@@ -377,11 +365,32 @@ , noted (try exprF30) , noted exprF31 , noted exprF32- , noted exprF02- , noted exprF08- , noted exprF09- , noted exprF10- , noted exprF11+ , (choice+ [ noted exprF03+ , noted exprF04+ , noted exprF05+ , noted exprF06+ , noted exprF07+ , noted exprF12+ , noted exprF13+ , noted exprF14+ , noted exprF15+ , noted exprF16+ , noted exprF17+ , noted exprF18+ , noted exprF20+ , noted exprF21+ , noted exprF19+ , noted exprF02+ , noted exprF08+ , noted exprF09+ , noted exprF10+ , noted exprF11+ , noted exprF22+ , noted exprF23+ , noted exprF01+ ]+ ) <?> "built-in value" , noted exprF00 , exprF33 ]@@ -483,32 +492,35 @@ return (BoolLit False) exprF24 = do- a <- Text.Parser.Token.natural+ a <- Text.Parser.Token.integer return (IntegerLit a) - exprF25 = do+ exprF25 = (do Text.Parser.Char.char '+' a <- Text.Parser.Token.natural- return (NaturalLit (fromIntegral a))+ return (NaturalLit (fromIntegral a)) ) <?> "natural" exprF26 = do+ sign <- fmap (\_ -> negate) (Text.Parser.Char.char '-')+ <|> fmap (\_ -> id ) (Text.Parser.Char.char '+')+ <|> pure id a <- Text.Parser.Token.double- return (DoubleLit a)+ return (DoubleLit (sign a)) exprF27 = do a <- Text.Parser.Token.stringLiteral return (TextLit a) - exprF28 = record+ exprF28 = record <?> "record type" - exprF29 = recordLit+ exprF29 = recordLit <?> "record literal" - exprF30 = union+ exprF30 = union <?> "union type" - exprF31 = unionLit+ exprF31 = unionLit <?> "union literal" exprF32 = do- a <- import_+ a <- import_ <?> "import" return (Embed a) exprF33 = do
+ src/Dhall/Tutorial.hs view
@@ -0,0 +1,2090 @@+{-# 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+ -- $optional++ -- * Records+ -- $records++ -- * Functions+ -- $functions++ -- * Combine+ -- $combine++ -- * Let expressions+ -- $let++ -- * Unions+ -- $unions++ -- * Polymorphic functions+ -- $polymorphic++ -- * Total+ -- $total++ -- * Built-in functions+ -- $builtins++ -- ** Caveats+ -- $caveats++ -- ** Overview+ -- $builtinOverview++ -- ** @Bool@+ -- $bool++ -- *** @(||)@+ -- $or++ -- *** @(&&)@+ -- $and++ -- *** @(==)@+ -- $equal++ -- *** @(/=)@+ -- $unequal++ -- *** @if@\/@then@\/@else@+ -- $ifthenelse++ -- ** @Natural@+ -- $natural++ -- *** @(+)@+ -- $plus++ -- *** @(*)@+ -- $times++ -- *** @Natural/even@+ -- $even++ -- *** @Natural/odd@+ -- $odd++ -- *** @Natural/isZero@+ -- $isZero++ -- *** @Natural/fold@+ -- $naturalFold++ -- *** @Natural/build@+ -- $naturalBuild++ -- ** @Integer@+ -- $integer++ -- ** @Double@+ -- $double++ -- ** @Text@+ -- $text++ -- *** @(++)@+ -- $textAppend++ -- ** @List@+ -- $list++ -- *** @List/fold@+ -- $listFold++ -- *** @List/build@+ -- $listBuild++ -- *** @List/length@+ -- $listLength++ -- *** @List/head@+ -- $listHead++ -- *** @List/last@+ -- $listLast++ -- *** @List/indexed@+ -- $listIndexed++ -- *** @List/reverse@+ -- $listReverse++ -- ** @Optional@+ -- $optional++ -- *** @Optional/fold@+ -- $optionalFold++ -- * Prelude+ -- $prelude++ -- * Conclusion+ -- $conclusion+ ) where++import Data.Vector (Vector)+import Dhall (Interpret(..), Type, detailed, input)++-- $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] : List Double+-- > }+-- +-- You can read the above configuration file into Haskell using the following+-- code:+-- +-- > -- example.hs+-- > +-- > {-# LANGUAGE DeriveGeneric #-}+-- > {-# LANGUAGE OverloadedStrings #-}+-- > +-- > import Dhall+-- > +-- > data Example = Example { foo :: Integer, bar :: Vector Double }+-- > deriving (Generic, Show)+-- > +-- > instance Interpret Example+-- > +-- > main :: IO ()+-- > main = do+-- > x <- input auto "./config"+-- > print (x :: Example)+-- +-- If you compile and run the above example, the program prints the corresponding+-- Haskell record:+-- +-- > $ ./example+-- > Example {foo = 1, bar = [3.0,4.0,5.0]}+--+-- You can also load some types directly into Haskell without having to define a+-- record, like this:+--+-- > >>> :set -XOverloadedStrings+-- > >>> input auto "True" :: IO Bool+-- > True+--+-- The `input` function can decode any value if we specify the value's expected+-- `Type`:+--+-- > input+-- > :: Type a -- Expected type+-- > -> Text -- Dhall program+-- > -> IO a -- Decoded expression+--+-- ... and we can either specify an explicit type like `bool`:+--+-- > bool :: Type Bool+-- > +-- > input bool :: Text -> IO Bool+-- >+-- > input bool "True" :: IO Bool+-- >+-- > >>> input bool "True"+-- > True+--+-- ... or we can use `auto` to let the compiler infer what type to decode from+-- the expected return type:+--+-- > auto :: Interpret a => Type a+-- >+-- > input auto :: Interpret a => Text -> IO a+-- >+-- > >>> input auto "True" :: IO Bool+-- > True+--+-- You can see what types `auto` supports \"out-of-the-box\" by browsing the+-- instances for the `Interpret` class. For example, the following instance+-- says that we can directly decode any Dhall expression that evaluates to a+-- @Bool@ into a Haskell `Bool`:+--+-- > instance Interpret Bool+--+-- ... which is why we could directly decode the string @\"True\"@ into the+-- value `True`.+--+-- There is also another instance that says that if we can decode a value of+-- type @a@, then we can also decode a @List@ of values as a `Vector` of @a@s:+--+-- > instance Interpret a => Interpret (Vector a)+--+-- Therefore, since we can decode a @Bool@, we must also be able to decode a+-- @List@ of @Bool@s, like this:+--+-- > >>> input auto "[True, False] : List Bool" :: 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] : List Bool"+-- > [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+-- > +-- > 1 : Bool+-- > +-- > (input):1:1+--+-- The interpreter complains because the string @\"1\"@ cannot be decoded into a+-- Haskell value of type `Bool`.+--+-- The code excerpt from the above error message has two components:+--+-- * the expression being type checked (i.e. @1@)+-- * the expression's expected type (i.e. @Bool@)+--+-- > Expression+-- > ⇩+-- > 1 : Bool+-- > ⇧+-- > Expected type+--+-- The @(:)@ symbol is how Dhall annotates values with their expected types.+-- This notation is equivalent to type annotations in Haskell using the @(::)@+-- symbol. Whenever you see:+--+-- > x : t+--+-- ... you should read that as \"we expect the expression @x@ to have type+-- @t@\". However, we might be wrong and if our expected type does not match the+-- expression's actual type then the type checker will complain.+--+-- In this case, the expression @1@ does not have type @Bool@ so type checking+-- fails with an exception.+--+-- __Exercise:__ Load the Dhall library into @ghci@ and run these commands to get+-- get a more detailed error message:+--+-- > >>> import Dhall+-- > >>> :set -XOverloadedStrings+-- > >>> detailed (input auto "1") :: IO Bool+-- > ...+--+-- ... then read the entire error message+--+-- __Exercise:__ Fix the type error, either by changing the value to decode or+-- changing the expected type++-- $imports+--+-- You might wonder why in some cases we can decode a configuration file:+--+-- > >>> writeFile "bool" "True"+-- > >>> input auto "./bool" :: IO Bool+-- > True+--+-- ... and in other cases we can decode a value directly:+--+-- > >>> input auto "True" :: IO Bool+-- > True+--+-- This is because importing a configuration from a file is a special case of a+-- more general language feature: Dhall expressions can reference other+-- expressions by their file path.+--+-- To illustrate this, let's create three files:+-- +-- > $ echo "True" > bool1+-- > $ echo "False" > bool2+-- > $ echo "./bool1 && ./bool2" > both+--+-- ... and read in all three files in a single expression:+-- +-- > >>> input auto "[ ./bool1 , ./bool2 , ./both ] : List Bool" :: 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 ] : List Double" > ./bar+--+-- > $ ./example+-- > Example {foo = 1, bar = [3.0,4.0,5.0]}+--+-- However, the Dhall language will forbid cycles in these file references. For+-- example, if we create the following cycle:+--+-- > $ echo './file1' > file2+-- > $ echo './file2' > file1+--+-- ... then the interpreter will reject the import:+--+-- > >>> input auto "./file1" :: IO Integer+-- > *** Exception: +-- > ↳ ./file1+-- > ↳ ./file2+-- >+-- > Cyclic import: ./file1+--+-- You can also import expressions by URL. For example, you can find a Dhall+-- expression hosted at this URL using @ipfs@:+--+-- <https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB>+--+-- > $ curl https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB+-- > True+--+-- ... and you can reference that expression either directly:+--+-- > >>> input auto "https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > True+-- +-- ... or inside of a larger expression:+--+-- > >>> input auto "False == https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > False+--+-- You're not limited to hosting Dhall expressions on @ipfs@. You can host a+-- Dhall expression anywhere that you can host UTF8-encoded text on the web, such+-- as Github, a pastebin, or your own web server.+--+-- You can import types, too. For example, we can change our @./bar@ file to:+--+-- > $ echo "[ 3.0, 4.0, 5.0 ] : List ./type" > ./bar+--+-- ... then specify the @./type@ in a separate file:+--+-- > $ echo "Double" > ./type+--+-- ... and everything still type checks:+--+-- > $ ./example+-- > Example {foo = 1, bar = [3.0,4.0,5.0]}+--+-- Note that all imports must be terminated by whitespace or you will get either+-- an import error or a parse error, like this:+--+-- > >>> writeFile "baz" "2.0"+-- > >>> input auto "./baz: Double" :: IO Double+-- > *** Exception: +-- > ↳ ./baz: +-- > +-- > Error: Missing file+--+-- This is because the parser thinks that @./baz:@ is a single token due to+-- the missing whitespace before the colon and tries to import a file named+-- @./baz:@, which does not exist. To fix the problem we have to add a space+-- after @./baz@:+--+-- > >>> input auto "./baz : Double" :: IO Double+-- > 2.0+--+-- __Exercise:__ There is a @not@ function hosted online here:+--+-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>+--+-- Visit that link and read the documentation. Then try to guess what this+-- code returns:+--+-- > >>> input auto "https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > ???+--+-- Run the code to test your guess++-- $lists+--+-- You can store 0 or more values of the same type in a list, like this:+--+-- > [1, 2, 3] : List Integer+--+-- Every list must be followed by the type of the list. The type annotation is+-- not optional and you will get an error if you omit the annotation:+--+-- > >>> input auto "[1, 2, 3]" :: IO (Vector Integer)+-- > *** Exception: (input):1:10: error: unexpected+-- > EOF, expected: ":"+-- > [1, 2, 3]<EOF> +-- > ^ +--+-- Also, list elements must all have the same type which must match the declared+-- type of the list. You will get an error if you try to store any other type+-- of element:+--+-- > input auto "[1, True, 3] : List Integer" :: IO (Vector Integer)+-- > *** Exception: +-- > Error: List element has the wrong type+-- > +-- > [1, True, 3] : List Integer+-- > +-- > (input):1:1+--+-- __Exercise:__ Create a @./config@ file that decodes to the following result:+--+-- > >>> input auto "./config" :: IO (Vector (Vector Integer))+-- > [[1,2,3],[4,5,6]]++-- $optional+--+-- @Optional@ values are exactly like lists except they can only hold 0 or 1+-- elements. They cannot hold 2 or more elements:+--+-- For example, these are valid @Optional@ values:+--+-- > [1] : Optional Integer+-- >+-- > [] : Optional Integer+--+-- ... but this is /not/ valid:+--+-- > [1, 2] : Optional Integer -- NOT valid+--+-- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes:+--+-- > >>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)+-- > Just 1+-- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer)+-- > Nothing+--+-- __Exercise:__ What is the shortest possible @./config@ file that you can decode+-- like this:+--+-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))+-- > ???+--+-- __Exercise:__ Try to decode an @Optional@ value with more than one element and+-- see what happens++-- $records+--+-- Record literals are delimited by curly braces and their fields are separated+-- by commas. For example, this is a valid record literal:+--+-- > { foo = True+-- > , bar = 2+-- > , baz = 4.2+-- > }+--+-- A record type is like a record literal except instead of specifying each+-- field's value we specify each field's type. For example, the preceding+-- record literal has the following record type:+--+-- > { foo : Bool+-- > , bar : Integer+-- > , baz : Double+-- > }+--+-- If you want to specify an empty record literal, you must use @{=}@, which is+-- special syntax reserved for empty records. If you want to specify the empty+-- record type, then you use @{}@. If you forget which is which you can always+-- ask the @dhall@ compiler to remind you of the type for each one:+--+-- > $ dhall+-- > {=}+-- > <Ctrl-D>+-- > {}+-- > +-- > {=}+--+-- > $ dhall+-- > {}+-- > <Ctrl-D>+-- > Type+-- > +-- > {}+--+-- You can access a field of a record using the following syntax:+--+-- > record.fieldName+--+-- ... which means to access the value of the field named @fieldName@ from the+-- @record@. For example:+--+-- > >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double+-- > 4.2+--+-- __Exercise__: What is the type of this record:+--+-- > { foo = 1+-- > , bar =+-- > { baz = 2.0+-- > , qux = True+-- > }+-- > }+--+-- __Exercise__: Save the above code to a file named @./record@ and then try to+-- access the value of the @baz@ field++-- $functions+--+-- The Dhall programming language also supports user-defined anonymous+-- functions. For example, we can save the following anonymous function to a+-- file:+--+-- > $ cat > makeBools+-- > \(n : Bool) ->+-- > [ n && True, n && False, n || True, n || False ] : List Bool+-- > <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 ] : List Bool+-- > <Ctrl-D>+--+-- You can read either one 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.+--+-- 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.+--+-- We can test our @makeBools@ function directly from the command line. This+-- library comes with a command-line executable program named @dhall@ that you+-- can use to both type-check files and convert them to a normal form. Our+-- compiler takes a program on standard input and then prints the program's type+-- to standard error followed by the program's normal form to standard output:+--+-- > $ dhall+-- > ./makeBools+-- > <Ctrl-D>+-- > ∀(n : Bool) → List Bool+-- > +-- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool+--+-- The first line says that @makeBools@ is a function of one argument named @n@+-- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@+-- (U+2200) symbol is shorthand for the ASCII @forall@ keyword:+--+-- > ∀(x : a) → b -- This type ...+-- > +-- > forall (x : a) → b -- ... is the same as this type+--+-- ... and Dhall's @forall@ keyword behaves the same way as Haskell's @forall@+-- keyword for input values that are @Type@s:+--+-- > forall (x : Type) → b -- This Dhall type ...+-- +-- > forall x . b -- ... is the same as this Haskell type+--+-- The part where Dhall differs from Haskell is that you can also use @∀@/@forall@+-- to give names to non-@Type@ arguments (such as the first argument to+-- @makeBools@).+--+-- The second line of Dhall's output is our program's normal form:+--+-- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool+--+-- ... which in this case happens to be identical to our original program.+--+-- To apply a function to an argument you separate the function and argument by+-- whitespace (just like Haskell):+--+-- @f x@+--+-- You can read the above as \"apply the function @f@ to the argument @x@\". This+-- means that we can \"apply\" our @./makeBools@ function to a @Bool@ argument+-- like this:+--+-- > $ dhall+-- > ./makeBools True+-- > <Ctrl-D>+-- > List Bool+-- > +-- > [True, False, True, True] : List Bool+--+-- 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] : List Bool) True+-- > <Ctrl-D>+-- > List Bool+-- > +-- > [True, False, True, True] : List Bool+--+-- 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] : List Bool+-- >+-- > -- ... then we get this:+-- > [True && True, True && False, True || True, True || False] : List Bool+-- >+-- > -- ... which reduces to the following normal form:+-- > [True, False, True, True] : List Bool+--+-- 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++-- $combine+--+-- You can combine two records, using the @(/\\)@ operator or the+-- corresponding Unicode @(∧)@ (U+2227) operator:+--+-- > $ dhall+-- > { foo = 1, bar = "ABC" } /\ { baz = True }+-- > <Ctrl-D>+-- > { bar : Text, baz : Bool, foo : Integer }+-- > +-- > { bar = "ABC", baz = True, foo = 1 }+--+-- > $ dhall+-- > { foo = 1, bar = "ABC" } ∧ { baz = True } -- Fancy unicode+-- > <Ctrl-D>+-- > { bar : Text, baz : Bool, foo : Integer }+-- > +-- > { bar = "ABC", baz = True, foo = 1 }+--+-- Note that the order of record fields does not matter. The compiler+-- automatically sorts the fields when normalizing expressions.+--+-- The @(∧)@ operator also merges records recursively. For example:+--+-- > $ 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 } }+--+-- However, you cannot combine two records if they share a field that is not a+-- record:+--+-- > $ dhall+-- > { foo = 1, bar = "ABC" } ∧ { foo = True }+-- > <Ctrl-D>+-- > Use "dhall --explain" for detailed errors+-- > +-- > Error: Field collision+-- > +-- > { foo = 1, bar = "ABC" } ∧ { foo = True }+-- > +-- > (stdin):1:1+--+-- __Exercise__: Combine any record with the empty record. What do you expect to+-- happen?++-- $let+--+-- Dhall also supports @let@ expressions, which you can use to define+-- intermediate values in the course of a computation, like this:+--+-- > $ dhall+-- > let x = "ha" in x ++ x+-- > <Ctrl-D>+-- > Text+-- >+-- > "haha"+--+-- You can also annotate the types of values defined within a @let@ expression,+-- like this:+--+-- > $ dhall+-- > let x : Text = "ha" in x ++ x+-- > <Ctrl-D>+-- > Text+-- >+-- > "haha"+--+-- Every @let@ expression of the form:+--+-- > let x : t = y in e+--+-- ... is exactly equivalent to:+--+-- > (λ(x : t) → e) y+--+-- So for example, this @let@ expression:+--+-- > let x : Text = "ha" in x ++ x+--+-- ... is equivalent to:+--+-- > (λ(x : Text) → x ++ x) "ha"+--+-- ... which in turn reduces to:+--+-- > "ha" ++ "ha"+--+-- ... which in turn reduces to:+--+-- > "haha"+--+-- You need to nest @let@ expressions if you want to define more than one value+-- in this way:+--+-- > $ dhall+-- > let x = "Hello, "+-- > in let y = "world!"+-- > in x ++ y+-- > <Ctrl-D>+-- > Text+-- > +-- > "Hello, world!"+--+-- Dhall is whitespace-insensitive, so feel free to format things over multiple+-- lines or indent in any way that you please.+--+-- If you want to define a named function, just give a name to an anonymous+-- function:+--+-- > $ dhall+-- > let twice = λ(x : Text) → x ++ x in twice "ha"+-- > <Ctrl-D>+-- > Text+-- > +-- > "haha"+--+-- Unlike Haskell, Dhall does not support function arguments on the left-hand+-- side of the equals sign, so this will not work:+--+-- > $ dhall+-- > let twice (x : Text) = x ++ x in twice "ha"+-- > <Ctrl-D>+-- > (stdin):1:11: error: expected: ":",+-- > "="+-- > let twice (x : Text) = x ++ x in twice "ha" +-- > ^+--+-- The error message says that Dhall expected either a @(:)@ (i.e. the beginning+-- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a+-- function argument.+--+-- You can also use @let@ expressions to rename imports, like this:+--+-- > $ dhall+-- > let not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > in not True+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- __Exercise:__ What do you think the following code will normalize to?+--+-- > let x = 1+-- > in let x = 2+-- > in x+--+-- Test your guess using the @dhall@ compiler+--+-- __Exercise:__ Now try to guess what this code will normalize to:+--+-- > let x = "ha"+-- > in let x = x ++ "ha"+-- > in x+--+-- __Exercise:__ What about this code?+--+-- > let x = x ++ "ha"+-- > in x++-- $unions+--+-- A union is a value that can be one of many alternative types of values. For+-- example, the following union type:+--+-- > < Left : Natural | Right : Bool >+--+-- ... represents a value that can be either a @Natural@ or a @Bool@ value. If+-- you are familiar with Haskell these are exactly analogous to Haskell's+-- \"sum types\".+--+-- Each alternative is associated with a tag that distinguishes that alternative+-- from other alternatives. In the above example, the @Left@ tag is used for+-- the @Natural@ alternative and the @Right@ tag is used for the @Bool@+-- alternative.+--+-- A union literal specifies the value of one alternative and the types of the+-- remaining alternatives. For example, both of the following union literals+-- have the same type, which is the above union type:+--+-- > < Left = +0 | Right : Bool >+--+-- > < Right = True | Left : Natural >+--+-- You can consume a union using the built-in @merge@ function. For example,+-- suppose we want to convert our union to a @Bool@ but we want to behave+-- differently depending on whether or not the union is a @Natural@ wrapped in+-- the @Left@ alternative or a @Bool@ wrapped in the @Right@ alternative. We+-- would write:+--+-- > $ cat > process <<EOF+-- > λ(union : < Left : Natural | Right : Bool >)+-- > → let handlers =+-- > { Left = Natural/even -- Natural/even is a built-in function+-- > , Right = λ(b : Bool) → b+-- > }+-- > in merge handlers union : Bool+-- > EOF+--+-- Now our @./process@ function can handle both alternatives:+--+-- > $ dhall+-- > ./process < Left = +3 | Right : Bool >+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- > $ dhall+-- > ./process < Right = True | Left : Natural >+-- > <Ctrl-D>+-- > Bool+-- > +-- > True+--+-- Every @merge@ has the following form:+--+-- > merge handlers union : type+--+-- ... where: +--+-- * @union@ is the union you want to consume+-- * @handlers@ is a record with one function per alternative of the union+-- * @type@ is the declared result type of the @merge@+--+-- The @merge@ function selects which function to apply from the record based on+-- which alternative the union selects:+--+-- > merge { Foo = f, ... } < Foo = x | ... > : t = f x : t+--+-- So, for example:+--+-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool+-- > = Natural/even +3 : Bool+-- > = False+--+-- ... and similarly:+--+-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Right = True | Left : Natural > : Bool+-- > = (λ(b : Bool) → b) True : Bool+-- > = True+--+-- Notice that each handler has to return the same type of result (@Bool@ in+-- this case) which must also match the declared result type of the @merge@.+--+-- __Exercise__: Create a list of the following type with at least one element:+-- per alternative:+--+-- > List < Left : Integer | Right : Double >++-- $polymorphic+--+-- The Dhall language supports defining polymorphic functions (a.k.a.+-- \"generic\" functions) that work on more than one type of value. However,+-- Dhall differs from Haskell by not inferring the types of these polymorphic+-- functions. Instead, you must be explicit about what type of value the+-- function is specialized to.+--+-- Take, for example, Haskell's identity function named @id@:+--+-- > id :: a -> a+-- > id = \x -> x+--+-- The identity function is polymorphic, meaning that `id` works on values of+-- different types:+--+-- > >>> id 4+-- > 4+-- > >>> id True+-- > True+--+-- The equivalent function in Dhall is:+--+-- > λ(a : Type) → λ(x : a) → x+--+-- Notice how this function takes two arguments instead of one. The first+-- argument is the type of the second argument.+--+-- Let's illustrate how this works by actually using the above function:+--+-- > $ echo "λ(a : Type) → λ(x : a) → x" > id+--+-- If we supply the function alone to the compiler we get the inferred type as+-- the first line:+-- +-- > $ dhall+-- > ./id+-- > <Ctrl-D>+-- > ∀(a : Type) → ∀(x : a) → a+-- > +-- > λ(a : Type) → λ(x : a) → x+--+-- You can read the type @(∀(a : Type) → ∀(x : a) → a)@ as saying: \"This is the+-- type of a function whose first argument is named @a@ and is a @Type@. The+-- second argument is named @x@ and has type @a@ (i.e. the value of the first+-- argument). The result also has type @a@.\"+--+-- This means that the type of the second argument changes depending on what+-- type we provide for the first argument. When we apply @./id@ to @Integer@, we+-- create a function that expects an @Integer@ argument:+--+-- > $ dhall+-- > ./id Integer+-- > <Ctrl-D>+-- > ∀(x : Integer) → Integer+-- > +-- > λ(x : Integer) → x+--+-- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a+-- @Bool@ argument:+--+-- > $ dhall+-- > ./id Bool+-- > <Ctrl-D>+-- > ∀(x : Bool) → Bool+-- > +-- > λ(x : Bool) → x+--+-- We can then supply the final argument to each of those functions to show+-- that they both work on their respective types:+--+-- > $ dhall+-- > ./id Integer 4+-- > <Ctrl-D>+-- > Integer+-- > +-- > 4+--+-- > $ dhall+-- > ./id Bool True+-- > <Ctrl-D>+-- > Bool+-- > +-- > True+--+-- Built-in functions can also be polymorphic, too. For example, we can ask+-- the compiler for the type of @List/reverse@, the function that reverses a+-- list:+--+-- > $ dhall+-- > List/reverse+-- > <Ctrl-D>+-- > ∀(a : Type) → List a → List a+-- > +-- > List/reverse+--+-- The first argument to @List/reverse@ is the type of the list to reverse:+--+-- > $ dhall+-- > List/reverse Bool+-- > <Ctrl-D>+-- > List Bool → List Bool+-- > +-- > List/reverse Bool+--+-- ... and the second argument is the list to reverse:+--+-- > $ dhall+-- > List/reverse Bool ([True, False] : List Bool)+-- > <Ctrl-D>+-- > List Bool+-- > +-- > [False, True] : List Bool+--+-- Note that the second argument has no name. This type:+--+-- > ∀(a : Type) → List a → List a+--+-- ... is equivalent to this type:+--+-- > ∀(a : Type) → ∀(_ : List a) → List a+--+-- In other words, if you don't see the @∀@ symbol surrounding a function+-- argument type then that means that the name of the argument is @"_"@. This+-- is true even for user-defined functions:+--+-- > $ dhall+-- > λ(_ : Text) → 1+-- > <Ctrl-D>+-- > Text → Integer+-- > +-- > λ(_ : Text) → 1+--+-- The type @(Text → Integer)@ is the same as @(∀(_ : Text) → Integer)@+--+-- __Exercise__ : Translate Haskell's `flip` function to Dhall++-- $total+--+-- Dhall is a total programming language, which means that Dhall is not+-- Turing-complete and evaluation of every Dhall program is guaranteed to+-- eventually halt. There is no upper bound on how long the program might take+-- to evaluate, but the program is guaranteed to terminate in a finite amount of+-- time and not hang forever.+--+-- This guarantees that all Dhall programs can be safely reduced to a normal+-- form where as many functions have been evaluated as possible. In fact, Dhall+-- expressions can be evaluated even if all function arguments haven't been fully+-- applied. For example, the following program is an anonymous function:+--+-- > $ dhall+-- > \(n : Bool) -> +10 * +10+-- > <Ctrl-D>+-- > ∀(n : Bool) → Natural+-- > +-- > λ(n : Bool) → +100+--+-- ... and even though the function is still missing the first argument named+-- @n@ the compiler is smart enough to evaluate the body of the anonymous+-- function ahead of time before the function has even been invoked.+--+-- We can use the @map@ function from the Prelude to illustrate an even more+-- complex example:+--+-- > $ dhall+-- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > in λ(f : Integer → Integer) → List/map Integer Integer f ([1, 2, 3] : List Integer)+-- > <Ctrl-D>+-- > ∀(f : Integer → Integer) → List Integer+-- > +-- > λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer+--+-- Dhall can apply our function to each element of the list even before we specify+-- which function to apply.+--+-- The language will also never crash or throw any exceptions. Every+-- computation will succeed and produce something, even if the result might be+-- an @Optional@ value:+--+-- > $ dhall+-- > List/head Integer ([] : List Integer)+-- > <Ctrl-D>+-- > Optional Integer+-- > +-- > [] : Optional Integer+--+-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can+-- find here:+--+-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate>+--+-- Test what the following Dhall expression normalizes to:+--+-- > let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate+-- > in replicate +10+--+-- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by+-- finding an input expression that crashes or loops forever (and file a bug+-- report if you succeed)++-- $builtins+--+-- Dhall is a restricted programming language that only supports simple built-in+-- functions and operators. If you want to do anything fancier you will need to+-- load your data into Haskell for further processing+--+-- This section covers types, functions, and operators that are built into the+-- language, meaning that you do not need to import any code to use them.+-- Additionally, Dhall also comes with a Prelude (covered in the next section)+-- hosted online that contains functions derived from these base utilities. The+-- Prelude also re-exports all built-in functions for people who prefer+-- consistency.+--+-- The following documentation on built-ins is provided primarily as a reference.+-- You don't need to read about every single built-in and you may want to skip to+-- the following Prelude section.++-- The language provides built-in support for the following primitive types:+--+-- * @Bool@ values+-- * @Natural@ values+-- * @Integer@ values+-- * @Double@ values+-- * @Text@ values+--+-- ... as well as support for the following derived types:+--+-- * @List@s of values+-- * @Optional@ values+-- * Anonymous records+-- * Anonymous unions++-- $caveats+--+-- Dhall differs in a few important ways from other programming languages, so+-- you should keep the following caveats in mind:+--+-- First, Dhall only supports addition and multiplication on @Natural@ numbers+-- (i.e. non-negative integers), which are not the same type of number as+-- @Integer@s (which can be negative). A @Natural@ number is a number prefixed+-- with the @+@ symbol. If you try to add or multiply two @Integer@s (without+-- the @+@ prefix) you will get a type error:+--+-- > $ dhall+-- > 2 + 2+-- > <Ctrl-D>+-- > Use "dhall --explain" for detailed errors+-- > +-- > Error: ❰+❱ only works on ❰Natural❱s+-- > +-- > 2 + 2+-- > +-- > (stdin):1:1+--+-- In fact, there are no built-in functions for @Integer@s (or @Double@s). As+-- far as the language is concerned they are opaque values that can only be+-- shuffled around but not used in any meaningful way until they have been+-- loaded into Haskell.+--+-- Second, the equality @(==)@ and inequality @(/=)@ operators only work on+-- @Bool@s. You cannot test any other types of values for equality.++-- $builtinOverview+--+-- Each of the following sections provides an overview of builtin functions and+-- operators for each type. For each function you get:+--+-- * An example use of that function+--+-- * A \"type judgement\" explaining when that function or operator is well+-- typed+--+-- For example, for the following judgement:+--+-- > Γ ⊢ x : Bool Γ ⊢ y : Bool+-- > ───────────────────────────+-- > Γ ⊢ x && y : Bool+--+-- ... you can read that as saying: "if @x@ has type @Bool@ and @y@ has type+-- @Bool@, then @x && y@ has type @Bool@"+--+-- Similarly, for the following judgement:+--+-- > ─────────────────────────────────+-- > Γ ⊢ Natural/even : Natural → Bool+--+-- ... you can read that as saying: "@Natural/even@ always has type+-- @Natural → Bool@"+--+-- * Rules for how that function or operator behaves+--+-- These rules are just equalities that come in handy when reasoning about code.+-- For example, the section on @(&&)@ has the following rules:+--+-- > (x && y) && z = x && (y && z)+-- >+-- > x && True = x+-- >+-- > True && x = x+--+-- These rules are also a contract for how the compiler should behave. If you+-- ever observe code that does not obey these rules you should file a bug+-- report.++-- $bool+--+-- There are two values that have type @Bool@ named @True@ and @False@:+--+-- > ───────────────+-- > Γ ⊢ True : Bool+--+-- > ────────────────+-- > Γ ⊢ False : Bool+--+-- The built-in operations for values of type @Bool@ are:+--++-- $or+--+-- Example:+--+-- > $ dhall+-- > True || False+-- > <Ctrl-D>+-- > Bool+-- > +-- > True+--+-- Type:+--+-- > Γ ⊢ x : Bool Γ ⊢ y : Bool+-- > ───────────────────────────+-- > Γ ⊢ x || y : Bool+--+-- Rules:+--+-- > (x || y) || z = x || (y || z)+-- > +-- > x || False = x+-- > +-- > False || x = x+-- >+-- > x || (y && z) = (x || y) && (x || z)+-- > +-- > x || True = True+-- > +-- > True || x = True++-- $and+--+-- Example:+--+-- > $ dhall+-- > True && False+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Type:+--+-- > Γ ⊢ x : Bool Γ ⊢ y : Bool+-- > ───────────────────────────+-- > Γ ⊢ x && y : Bool+--+-- Rules:+--+-- > (x && y) && z = x && (y && z)+-- > +-- > x && True = x+-- > +-- > True && x = x+-- >+-- > x && (y || z) = (x && y) || (x && z)+-- > +-- > x && False = False+-- > +-- > False && x = False++-- $equal+--+-- Example:+--+-- > $ dhall+-- > True == False+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Type:+--+-- > Γ ⊢ x : Bool Γ ⊢ y : Bool+-- > ───────────────────────────+-- > Γ ⊢ x == y : Bool+--+-- Rules:+--+-- > (x == y) == z = x == (y == z)+-- > +-- > x == True = x+-- > +-- > True == x = x+-- >+-- > x == x = True++-- $unequal+--+-- Example:+--+-- > $ dhall+-- > True != False+-- > <Ctrl-D>+-- > Bool+-- > +-- > True+--+-- Type:+--+-- > Γ ⊢ x : Bool Γ ⊢ y : Bool+-- > ───────────────────────────+-- > Γ ⊢ x != y : Bool+--+-- Rules:+--+-- > (x != y) != z = x != (y != z)+-- > +-- > x != False = x+-- > +-- > False != x = x+-- >+-- > x != x = False++-- $ifthenelse+--+-- Example:+--+-- > $ dhall+-- > if True then 3 else 5+-- > <Ctrl-D>+-- > Integer+-- > +-- > 3+--+-- Type:+--+-- > Γ ⊢ t : Type+-- > ─────────────────────+-- > Γ ⊢ b : Bool Γ ⊢ l : t Γ ⊢ r : t+-- > ────────────────────────────────────+-- > Γ ⊢ if b then l else r+--+-- Rules:+--+-- > if b then True else False = b+-- > +-- > if True then l else r = l+-- > +-- > if False then l else r = r++-- $natural+--+-- @Natural@ literals are numbers prefixed by a @+@ sign, like this:+--+-- > +4 : Natural+--+-- If you omit the @+@ sign then you get an @Integer@ literal, which is a+-- different type of value++-- $plus+--+-- Example:+--+-- > $ dhall+-- > +2 + +3+-- > <Ctrl-D>+-- > Natural+-- > +-- > +5+--+-- Type:+--+-- > Γ ⊢ x : Natural Γ ⊢ y : Natural+-- > ─────────────────────────────────+-- > Γ ⊢ x + y : Natural+--+-- Rules:+--+-- > (x + y) + z = x + (y + z)+-- >+-- > x + +0 = x+-- >+-- > +0 + x = x++-- $times+--+-- Example:+--+-- > $ dhall+-- > +2 * +3+-- > <Ctrl-D>+-- > Natural+-- > +-- > +6+--+-- Type:+--+-- > Γ ⊢ x : Natural Γ ⊢ y : Natural+-- > ─────────────────────────────────+-- > Γ ⊢ x * y : Natural+--+-- Rules:+--+-- > (x * y) * z = x * (y * z)+-- >+-- > x * +1 = x+-- >+-- > +1 * x = x+-- >+-- > (x + y) * z = (x * z) + (y * z)+-- >+-- > x * (y + z) = (x * y) + (x * z)+-- >+-- > x * +0 = +0+-- >+-- > +0 * x = +0++-- $even+--+-- Example:+--+-- > $ dhall+-- > Natural/even +6+-- > <Ctrl-D>+-- > Bool+-- > +-- > True+--+-- Type:+--+-- > ─────────────────────────────────+-- > Γ ⊢ Natural/even : Natural → Bool+--+-- Rules:+--+-- > Natural/even (x + y) = Natural/even x == Natural/even y+-- >+-- > Natural/even +0 = True+-- >+-- > Natural/even (x * y) = Natural/even x || Natural/even y+-- >+-- > Natural/even +1 = False++-- $odd+--+-- Example:+--+-- > $ dhall+-- > Natural/odd +6+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Type:+--+-- > ────────────────────────────────+-- > Γ ⊢ Natural/odd : Natural → Bool+--+-- Rules:+--+-- > Natural/odd (x + y) = Natural/odd x /= Natural/odd y+-- >+-- > Natural/odd +0 = False+-- >+-- > Natural/odd (x * y) = Natural/odd x && Natural/odd y+-- >+-- > Natural/odd +1 = True++-- $isZero+--+-- Example:+--+-- > $ dhall+-- > Natural/isZero +6+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Type:+--+-- > ───────────────────────────────────+-- > Γ ⊢ Natural/isZero : Natural → Bool+--+-- Rules:+--+-- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y+-- >+-- > Natural/isZero +0 = True+-- >+-- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y+-- >+-- > Natural/isZero +1 = False++-- $naturalFold+--+-- Example:+--+-- > $ dhall+-- > Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome"+-- > <Ctrl-D>+-- > Text+-- > +-- > "You're welcome!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"+--+-- Type:+--+-- > ──────────────────────────────────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ Natural/fold : Natural → ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural+--+-- Rules:+-- +-- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z)+-- > +-- > Natural/fold +0 n s z = z+-- > +-- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s)+-- > +-- > Natural/fold 1 n s = s++-- $naturalBuild+--+-- Example:+--+-- > $ dhall+-- > Natural/build (λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ zero))+-- > <Ctrl-D>+-- > Natural+-- > +-- > +2+--+-- Type:+--+-- > ─────────────────────────────────────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ Natural/build : (∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural) → Natural+--+-- Rules:+--+-- > Natural/fold (Natural/build x) = x+-- >+-- > Natural/build (Natural/fold x) = x++-- $integer+--+-- @Integer@ literals are either prefixed with a @-@ sign (if they are negative)+-- or no sign (if they are positive), like this:+--+-- > 3 : Integer+-- > -2 : Integer+--+-- If you prefix them with a @+@ sign then they are @Natural@ literals and not+-- @Integer@s+--+-- There are no built-in operations on @Integer@s. For all practical purposes+-- they are opaque values within the Dhall language++-- $double+--+-- A @Double@ literal is a floating point value with at least one decimal+-- place, such as:+--+-- > -2.0 : Double+-- > 3.14159 : Double+--+-- There are no built-in operations on @Double@s. For all practical purposes+-- they are opaque values within the Dhall language++-- $text+--+-- A @Text@ literal is just a sequence of characters enclosed in double quotes,+-- like:+--+-- > "ABC" : Text+--+-- The only thing you can do with @Text@ values is concatenate them++-- $textAppend+--+-- Example:+--+-- > $ dhall+-- > "Hello, " ++ "world!"+-- > <Ctrl-D>+-- > Text+-- > +-- > "Hello, world!"+--+-- Type:+--+-- > Γ ⊢ x : Text Γ ⊢ y : Text+-- > ───────────────────────────+-- > Γ ⊢ x && y : Text+--+-- Rules:+--+-- > (x ++ y) ++ z = x ++ (y ++ z)+-- > +-- > x ++ "" = x+-- > +-- > "" ++ x = x++-- $list+--+-- Dhall @List@ literals are a sequence of values inside of brackets separated by+-- commas:+--+-- > Γ ⊢ t : Type Γ ⊢ x : t Γ ⊢ y : t ...+-- > ──────────────────────────────────────────+-- > Γ ⊢ [x, y, ... ] : List t+--+-- Also, every @List@ must end with a mandatory type annotation+--+-- The built-in operations on @List@s are:++-- $listFold+--+-- Example:+--+-- > $ dhall+-- > List/fold Bool ([True, False, True] : List Bool) Bool (λ(x : Bool) → λ(y : Bool) → x && y) True+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Type:+--+-- > ────────────────────────────────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ List/fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list+--+-- Rules:+--+-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- >+-- > List/fold a (List/concat a xss) b c+-- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)+-- >+-- > List/fold a ([] : List a) b c n = n+-- >+-- > List/fold a ([x] : List a) b c = c x++-- $listBuild+--+-- Example:+--+-- > $ dhall+-- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))+-- > <Ctrl-D>+-- > List Integer+-- > +-- > [1, 2, 3] : List Integer+--+-- Type:+--+-- > ───────────────────────────────────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ List/build : ∀(a : Type) → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → List a+--+-- Rules:+--+-- > List/build t (List/fold t x) = x+-- >+-- > List/fold t (List/build t x) = x++-- $listLength+--+-- Example:+--+-- > $ dhall+-- > List/length Integer ([1, 2, 3] : List Integer)+-- > <Ctrl-D>+-- > Natural+-- > +-- > +3+--+-- Type:+--+-- > ────────────────────────────────────────────────+-- > Γ ⊢ List/length : ∀(a : Type) → List a → Natural+--+-- Rules:+--+-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0++-- $listHead+--+-- Example:+--+-- > $ dhall+-- > List/head Integer ([1, 2, 3] : List Integer)+-- > <Ctrl-D>+-- > Optional Integer+-- > +-- > [1] : Optional Integer+--+-- Type:+--+-- > ─────────────────────────────────────+-- > Γ ⊢ List/head ∀(a : Type) → List a → Optional a+--+-- Rules:+--+-- > let Optional/head = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/head+-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap+-- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > +-- > List/head a (List/concat a xss) =+-- > Optional/head a (List/map (List a) (Optional a) (List/head a) xss)+-- > +-- > List/head a ([x] : List a) = [x] : Optional a+-- > +-- > List/head b (List/concatMap a b f m)+-- > = Optional/concatMap a b (λ(x : a) → List/head b (f x)) (List/head a m)++-- $listLast+--+-- Example:+--+-- > $ dhall+-- > List/last Integer ([1, 2, 3] : List Integer)+-- > <Ctrl-D>+-- > Optional Integer+-- > +-- > [1] : Optional Integer+--+-- Type:+--+-- > ─────────────────────────────────────+-- > Γ ⊢ List/last : ∀(a : Type) → List a → Optional a+--+-- Rules:+--+-- > let Optional/last = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/last+-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap+-- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > +-- > List/last a (List/concat a xss) =+-- > Optional/last a (List/map (List a) (Optional a) (List/last a) xss)+-- > +-- > List/last a ([x] : List a) = [x] : Optional a+-- > +-- > List/last b (List/concatMap a b f m)+-- > = Optional/concatMap a b (λ(x : a) → List/last b (f x)) (List/last a m)++-- $listIndexed+--+-- Example+--+-- > $ dhall+-- > List/indexed Text (["ABC", "DEF", "GHI"] : List Text)+-- > <Ctrl-D>+-- > List { index : Natural, value : Text }+-- > +-- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text }+--+-- Type:+--+-- > ─────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a }+--+-- Rules:+--+-- > let List/shifted = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/shifted+-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > +-- > List/indexed a (List/concat a xss) =+-- > List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)++-- $listReverse+--+-- Example:+--+-- > $ dhall+-- > List/reverse Integer ([1, 2, 3] : List Integer)+-- > <Ctrl-D>+-- > List Integer+-- > +-- > [3, 2, 1] : List Integer+--+-- Type:+--+-- > ─────────────────────────────────────────────────+-- > Γ ⊢ List/reverse : ∀(a : Type) → List a → List a+--+-- Rules:+--+-- > let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap+-- > +-- > List/reverse a (List/concat a xss)+-- > = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss))+-- >+-- > List/reverse a ([x] : List a) = [x] : List a+-- >+-- > List/reverse b (List/concatMap a b f xs)+-- > = List/concatMap a b (λ(x : a) → List/reverse b (f x)) (List/reverse a xs)+-- >+-- > List/reverse a ([x, y] : List a) = [y, x] : List a++-- $optional+--+-- Dhall @Optional@ literals are a 0 or 1 values inside of brackets:+--+-- > Γ ⊢ t : Type Γ ⊢ x : t+-- > ────────────────────────+-- > Γ ⊢ ([x] : Optional t) : Optional t+--+-- > Γ ⊢ t : Type+-- > ────────────────────────+-- > Γ ⊢ ([] : Optional t) : Optional t+--+-- Also, every @Optional@ literal must end with a mandatory type annotation+--+-- The built-in operations on @Optional@ values are:++-- $optionalFold+--+-- Example:+--+-- > $ dhall+-- > Optional/fold Text (["ABC"] : Optional Text) Text (λ(t : Text) → t) ""+-- > <Ctrl-D>+-- > Text+-- > +-- > "ABC"+--+-- Type:+--+-- > ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────+-- > Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(just : a → optional) → ∀(nothing : optional) → optional+--+-- Rules:+--+-- > Optional/fold a ([] : Optional a) o j n = n+-- >+-- > Optional/fold a ([x] : Optional a) o j n = j x++-- $prelude+--+-- There is also a Prelude available at:+--+-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>+--+-- There is nothing \"official\" or \"standard\" about this Prelude other than+-- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a+-- set of convenient utilities which didn't quite make the cut to be built into+-- the language. Feel free to host your own custom Prelude if you want!+--+-- If you visit the above link you can browse the Prelude, which has a few+-- subdirectories. For example, the @Bool@ subdirectory has a @not@ file+-- located here:+--+-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>+--+-- The @not@ function is just a UTF8-encoded text file hosted online with the+-- following contents+--+-- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > {-+-- > Flip the value of a `Bool`+-- > +-- > Examples:+-- > +-- > ```+-- > ./not True = False+-- > +-- > ./not False = True+-- > ```+-- > -}+-- > let not : Bool → Bool+-- > = λ(b : Bool) → b == False+-- > +-- > in not+--+-- The file could have been much shorter, like this:+--+-- > λ(b : Bool) → b == False+--+-- ... but all the functions exported from the Prelude try to be as+-- self-documenting as possible by including:+--+-- * the name of the function+-- * the type of the function+-- * documentation (including a few examples)+--+-- The performance penalty for adding these helpful features is negligible.+--+-- You can use this @not@ function either directly:+--+-- > $ dhall+-- > https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not True+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- ... or assign the URL to a shorter name:+--+-- > $ dhall+-- > let Bool/not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > in Bool/not True+-- > <Ctrl-D>+-- > Bool+-- > +-- > False+--+-- Some functions in the Prelude just re-export built-in functions for+-- consistency and documentation, such as @Prelude/Natural/even@, which+-- re-exports the built-in @Natural/even@ function:+--+-- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even+-- > {-+-- > Returns `True` if a number if even and returns `False` otherwise+-- > +-- > Examples:+-- > +-- > ```+-- > ./even +3 = False+-- > +-- > ./even +0 = True+-- > ```+-- > -}+-- > let even : Natural → Bool+-- > = Natural/even+-- > +-- > in even+--+-- You can also download the Prelude locally to your filesystem if you prefer+-- using local relative paths instead of URLs. For example, you can use @wget@,+-- like this:+--+-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/+-- > $ tree Prelude+-- > Prelude+-- > ├── Bool+-- > │ ├── and+-- > │ ├── build+-- > │ ├── even+-- > │ ├── fold+-- > │ ├── not+-- > │ ├── odd+-- > │ └── or+-- > ├── List+-- > │ ├── all+-- > │ ├── any+-- > │ ├── build+-- > │ ├── concat+-- > │ ├── filter+-- > │ ├── fold+-- > │ ├── generate+-- > │ ├── head+-- > │ ├── indexed+-- > │ ├── iterate+-- > │ ├── last+-- > │ ├── length+-- > │ ├── map+-- > │ ├── null+-- > │ ├── replicate+-- > │ ├── reverse+-- > │ ├── shifted+-- > │ └── unzip+-- > ├── Monoid+-- > ├── Natural+-- > │ ├── build+-- > │ ├── enumerate+-- > │ ├── even+-- > │ ├── fold+-- > │ ├── isZero+-- > │ ├── odd+-- > │ ├── product+-- > │ └── sum+-- > ├── Optional+-- > │ ├── build+-- > │ ├── concat+-- > │ ├── fold+-- > │ ├── head+-- > │ ├── last+-- > │ ├── map+-- > │ ├── toList+-- > │ └── unzip+-- > └── Text+-- > └── concat+--+-- ... or if you have an @ipfs@ daemon running, you can mount the Prelude+-- locally like this:+--+-- > $ ipfs mount+-- > $ cd /ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude+--+-- Browse the Prelude online to learn more by seeing what functions are+-- available and reading their inline documentation:+--+-- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>+--+-- __Exercise__: Try to use a new Prelude function that has not been covered+-- previously in this tutorial++-- $conclusion+--+-- By this point you should be able to use the Dhall configuration language to+-- author, import, and program configuration files. If you run into any issues+-- you can report them at:+--+-- <https://github.com/Gabriel439/Haskell-Dhall-Library/issues>+--+-- You can also request features, support, or documentation improvements on the+-- above issue tracker.+--+-- If you would like to contribute to the Dhall project you can try to port Dhall+-- to other languages besides Haskell so that Dhall configuration files can be+-- read into those languages, too.
src/Dhall/TypeCheck.hs view
@@ -5,6 +5,8 @@ {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall #-} +-- | This module contains the logic for type checking Dhall code+ module Dhall.TypeCheck ( -- * Type-checking typeWith@@ -18,12 +20,13 @@ ) where import Control.Exception (Exception)-import Data.Foldable (forM_)+import Data.Foldable (forM_, toList) import Data.Monoid ((<>)) import Data.Set (Set) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder)+import Data.Traversable (forM) import Data.Typeable (Typeable) import Dhall.Core (Const(..), Expr(..), Var(..)) import Dhall.Context (Context)@@ -419,9 +422,9 @@ return (Pi "a" (Const Type) (Pi "_" (App Optional "a")- (Pi "maybe" (Const Type)- (Pi "just" (Pi "_" "a" "maybe")- (Pi "nothing" "maybe" "maybe") ) ) ) )+ (Pi "optional" (Const Type)+ (Pi "just" (Pi "_" "a" "optional")+ (Pi "nothing" "optional" "optional") ) ) ) ) typeWith ctx e@(Record kts ) = do let process (k, t) = do s <- fmap Dhall.Core.normalize (typeWith ctx t)@@ -461,19 +464,29 @@ ktsX <- case tKvsX of Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))- let ksX = Data.Map.keysSet ktsX tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY) ktsY <- case tKvsY of Record kts -> return kts _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))- let ksY = Data.Map.keysSet ktsY - let ks = Data.Set.intersection ksX ksY- if Data.Set.null ks- then return ()- else Left (TypeError ctx e (FieldCollision ks))- return (Record (Data.Map.union ktsX ktsY))+ let combineTypes ktsL ktsR = do+ let ks =+ Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)+ kts <- forM (toList ks) (\k -> do+ case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of+ (Just (Record ktsL'), Just (Record ktsR')) -> do+ t <- combineTypes ktsL' ktsR'+ return (k, t)+ (Nothing, Just t) -> do+ return (k, t)+ (Just t, Nothing) -> do+ return (k, t)+ _ -> do+ Left (TypeError ctx e (FieldCollision k)) )+ return (Record (Data.Map.fromList kts))++ combineTypes ktsX ktsY typeWith ctx e@(Merge kvsX kvsY t) = do tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX) ktsX <- case tKvsX of@@ -563,7 +576,7 @@ | InvalidAlternativeType Text (Expr s X) | DuplicateAlternative Text | MustCombineARecord (Expr s X) (Expr s X)- | FieldCollision (Set Text)+ | FieldCollision Text | MustMergeARecord (Expr s X) (Expr s X) | MustMergeUnion (Expr s X) (Expr s X) | UnusedHandler (Set Text)@@ -605,12 +618,6 @@ -- ^ Longer and more detailed explanation of the error } -instance Buildable ErrorMessages where- build (ErrorMessages {..}) =- "Error: " <> build short <> "\n"- <> "\n"- <> long- _NOT :: Data.Text.Text _NOT = "\ESC[1mnot\ESC[0m" @@ -977,7 +984,7 @@ prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..} where- short = "Wrong function argument"+ short = "Wrong type of function argument" long = Builder.fromText [NeatInterpolation.text|@@ -2008,7 +2015,7 @@ ↳ $txt0 -... which is not a record, but is actually a value of type:+... which is not a record, but is actually a: ↳ $txt1 |]@@ -2016,7 +2023,7 @@ txt0 = Text.toStrict (Dhall.Core.pretty expr0) txt1 = Text.toStrict (Dhall.Core.pretty expr1) -prettyTypeMessage (FieldCollision ks) = ErrorMessages {..}+prettyTypeMessage (FieldCollision k) = ErrorMessages {..} where short = "Field collision" @@ -2067,7 +2074,7 @@ patch-oriented programming |] where- txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks))+ txt0 = Text.toStrict k prettyTypeMessage (MustMergeARecord expr0 expr1) = ErrorMessages {..} where@@ -2816,7 +2823,8 @@ instance Buildable s => Buildable (TypeError s) where build (TypeError ctx expr msg)- = ( if Text.null (Builder.toLazyText (buildContext ctx))+ = "\n"+ <> ( if Text.null (Builder.toLazyText (buildContext ctx)) then "" else buildContext ctx <> "\n" )@@ -2836,6 +2844,9 @@ Note s _ -> build s _ -> mempty +{-| Newtype used to wrap error messages so that they render with a more+ detailed explanation of what went wrong+-} newtype DetailedTypeError s = DetailedTypeError (TypeError s) deriving (Typeable) @@ -2846,7 +2857,8 @@ instance Buildable s => Buildable (DetailedTypeError s) where build (DetailedTypeError (TypeError ctx expr msg))- = ( if Text.null (Builder.toLazyText (buildContext ctx))+ = "\n"+ <> ( if Text.null (Builder.toLazyText (buildContext ctx)) then "" else buildContext ctx <> "\n" )