diff --git a/dhall.cabal b/dhall.cabal --- a/dhall.cabal +++ b/dhall.cabal @@ -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 diff --git a/exec/Main.hs b/exec/Main.hs --- a/exec/Main.hs +++ b/exec/Main.hs @@ -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 diff --git a/src/Dhall.hs b/src/Dhall.hs --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -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 --- > --- --- 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 --- > --- > 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!" --- > --- > 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 --- > --- > 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 --- > --- > 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 --- > --- > ∀(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 {..} diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs --- a/src/Dhall/Context.hs +++ b/src/Dhall/Context.hs @@ -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) diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -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 diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs --- a/src/Dhall/Import.hs +++ b/src/Dhall/Import.hs @@ -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 + > + > 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 diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs --- a/src/Dhall/Parser.hs +++ b/src/Dhall/Parser.hs @@ -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 diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs new file mode 100644 --- /dev/null +++ b/src/Dhall/Tutorial.hs @@ -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 < { 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@: +-- +-- +-- +-- > $ 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: +-- +-- +-- +-- 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] +-- > ^ +-- +-- 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 +-- > {=} +-- > +-- > {} +-- > +-- > {=} +-- +-- > $ dhall +-- > {} +-- > +-- > 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 +-- > +-- +-- ... 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 +-- > +-- +-- 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 +-- > +-- > ∀(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 +-- > +-- > 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 +-- > +-- > 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 } +-- > +-- > { bar : Text, baz : Bool, foo : Integer } +-- > +-- > { bar = "ABC", baz = True, foo = 1 } +-- +-- > $ dhall +-- > { foo = 1, bar = "ABC" } ∧ { baz = True } -- Fancy unicode +-- > +-- > { 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 } } +-- > +-- > { 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 } +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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" +-- > +-- > 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" +-- > +-- > (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 +-- > +-- > 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 < λ(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 > +-- > +-- > Bool +-- > +-- > False +-- +-- > $ dhall +-- > ./process < Right = True | Left : Natural > +-- > +-- > 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 +-- > +-- > ∀(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 +-- > +-- > ∀(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 +-- > +-- > ∀(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 +-- > +-- > Integer +-- > +-- > 4 +-- +-- > $ dhall +-- > ./id Bool True +-- > +-- > 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 +-- > +-- > ∀(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 +-- > +-- > List Bool → List Bool +-- > +-- > List/reverse Bool +-- +-- ... and the second argument is the list to reverse: +-- +-- > $ dhall +-- > List/reverse Bool ([True, False] : List Bool) +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > ∀(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) +-- > +-- > ∀(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) +-- > +-- > Optional Integer +-- > +-- > [] : Optional Integer +-- +-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can +-- find here: +-- +-- +-- +-- 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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 +-- > +-- > 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" +-- > +-- > 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)) +-- > +-- > 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!" +-- > +-- > 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 +-- > +-- > 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))) +-- > +-- > 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) +-- > +-- > 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) +-- > +-- > 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) +-- > +-- > 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) +-- > +-- > 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) +-- > +-- > 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) "" +-- > +-- > 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: +-- +-- +-- +-- 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: +-- +-- +-- +-- 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 +-- > +-- > 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 +-- > +-- > 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: +-- +-- +-- +-- __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: +-- +-- +-- +-- 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. diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs --- a/src/Dhall/TypeCheck.hs +++ b/src/Dhall/TypeCheck.hs @@ -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" )