-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A configuration language guaranteed to terminate -- -- Dhall is an explicitly typed configuration language that is not Turing -- complete. Despite being Turing incomplete, Dhall is a real programming -- language with a type-checker and evaluator. -- -- Use this library to parse, type-check, evaluate, and pretty-print the -- Dhall configuration language. This package also includes an executable -- which type-checks a Dhall file and reduces the file to a fully -- evaluated normal form. -- -- Read Dhall.Tutorial to learn how to use this library @package dhall @version 1.0.2 -- | 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 -- | Constants for a pure type system -- -- The only axiom is: -- -- 
--   ⊦ Type : Kind
--
-- -- ... and the valid rule pairs are: -- -- 
--   ⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)
--   ⊦ Kind ↝ Type : Type  -- Functions from types to terms (polymorphic functions)
--   ⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type constructors)
--
-- -- These are the same rule pairs as System Fω -- -- Note that Dhall does not support functions from terms to types and -- therefore Dhall is not a dependently typed language data Const Type :: Const Kind :: Const -- | Path to an external resource data Path File :: FilePath -> Path URL :: Text -> Path -- | Label for a bound variable -- -- The Text field is the variable's name (i.e. "x"). -- -- The Int field disambiguates variables with the same name if -- there are multiple bound variables of the same name in scope. Zero -- refers to the 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 : Type) -> \(y : Type) -> \(x : Type) -> x@0
--   
--     +------------------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. -- -- You can optionally omit the index if it is 0: -- -- 
--                             +refers to+
--                             |         |
--                             v         |
--   \(x : *) -> \(y : *) -> \(x : *) -> x
--
-- -- Zero indices are omitted when pretty-printing Vars and non-zero -- indices appear as a numeric suffix. data Var V :: Text -> !Integer -> Var -- | Syntax tree for expressions data Expr s a -- | 
--   Const c                                  ~  c
--
Const :: Const -> Expr s a -- | 
--   Var (V x 0)                              ~  x
--   Var (V x n)                              ~  x@n
--
Var :: Var -> Expr s a -- | 
--   Lam x     A b                            ~  λ(x : A) -> b
--
Lam :: Text -> (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Pi "_" A B                               ~        A  -> B
--   Pi x   A B                               ~  ∀(x : A) -> B
--
Pi :: Text -> (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   App f a                                  ~  f a
--
App :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Let x Nothing  r e  ~  let x     = r in e
--   Let x (Just t) r e  ~  let x : t = r in e
--
Let :: Text -> (Maybe (Expr s a)) -> (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Annot x t                                ~  x : t
--
Annot :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Bool                                     ~  Bool
--
Bool :: Expr s a -- | 
--   BoolLit b                                ~  b
--
BoolLit :: Bool -> Expr s a -- | 
--   BoolAnd x y                              ~  x && y
--
BoolAnd :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   BoolOr  x y                              ~  x || y
--
BoolOr :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   BoolEQ  x y                              ~  x == y
--
BoolEQ :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   BoolNE  x y                              ~  x != y
--
BoolNE :: (Expr s a) -> (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) -> Expr s a -- | 
--   Natural                                  ~  Natural
--
Natural :: Expr s a -- | 
--   NaturalLit n                             ~  +n
--
NaturalLit :: Natural -> Expr s a -- | 
--   NaturalFold                              ~  Natural/fold
--
NaturalFold :: Expr s a -- | 
--   NaturalBuild                             ~  Natural/build
--
NaturalBuild :: Expr s a -- | 
--   NaturalIsZero                            ~  Natural/isZero
--
NaturalIsZero :: Expr s a -- | 
--   NaturalEven                              ~  Natural/even
--
NaturalEven :: Expr s a -- | 
--   NaturalOdd                               ~  Natural/odd
--
NaturalOdd :: Expr s a -- | 
--   NaturalPlus x y                          ~  x + y
--
NaturalPlus :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   NaturalTimes x y                         ~  x * y
--
NaturalTimes :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Integer                                  ~  Integer
--
Integer :: Expr s a -- | 
--   IntegerLit n                             ~  n
--
IntegerLit :: Integer -> Expr s a -- | 
--   Double                                   ~  Double
--
Double :: Expr s a -- | 
--   DoubleLit n                              ~  n
--
DoubleLit :: Double -> Expr s a -- | 
--   Text                                     ~  Text
--
Text :: Expr s a -- | 
--   TextLit t                                ~  t
--
TextLit :: Builder -> Expr s a -- | 
--   TextAppend x y                           ~  x ++ y
--
TextAppend :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   List                                     ~  List
--
List :: Expr s a -- | 
--   ListLit t [x, y, z]                      ~  [x, y, z] : List t
--
ListLit :: (Expr s a) -> (Vector (Expr s a)) -> Expr s a -- | 
--   ListBuild                                ~  List/build
--
ListBuild :: Expr s a -- | 
--   ListFold                                 ~  List/fold
--
ListFold :: Expr s a -- | 
--   ListLength                               ~  List/length
--
ListLength :: Expr s a -- | 
--   ListHead                                 ~  List/head
--
ListHead :: Expr s a -- | 
--   ListLast                                 ~  List/last
--
ListLast :: Expr s a -- | 
--   ListIndexed                              ~  List/indexed
--
ListIndexed :: Expr s a -- | 
--   ListReverse                              ~  List/reverse
--
ListReverse :: Expr s a -- | 
--   Optional                                 ~  Optional
--
Optional :: Expr s a -- | 
--   OptionalLit t [e]                        ~  [e] : Optional t
--   OptionalLit t []                         ~  []  : Optional t
--
OptionalLit :: (Expr s a) -> (Vector (Expr s a)) -> Expr s a -- | 
--   OptionalFold                             ~  Optional/fold
--
OptionalFold :: Expr s a -- | 
--   Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }
--
Record :: (Map Text (Expr s a)) -> Expr s a -- | 
--   RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }
--
RecordLit :: (Map Text (Expr s a)) -> Expr s a -- | 
--   Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >
--
Union :: (Map Text (Expr s a)) -> Expr s a -- | 
--   UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 > 
--
UnionLit :: Text -> (Expr s a) -> (Map Text (Expr s a)) -> Expr s a -- | 
--   Combine x y                              ~  x ∧ y
--
Combine :: (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Merge x y t                              ~  merge x y : t
--
Merge :: (Expr s a) -> (Expr s a) -> (Expr s a) -> Expr s a -- | 
--   Field e x                                ~  e.x
--
Field :: (Expr s a) -> Text -> Expr s a -- | 
--   Note s x                                 ~  e
--
Note :: s -> (Expr s a) -> Expr s a -- | 
--   Embed path                               ~  path
--
Embed :: a -> Expr s a -- | Reduce an expression to its normal form, performing beta reduction -- -- normalize does not type-check the expression. You may want to -- type-check expressions before normalizing them since normalization can -- convert an ill-typed expression into a well-typed expression. -- -- However, normalize will not fail if the expression is ill-typed -- and will leave ill-typed sub-expressions unevaluated. normalize :: Expr s a -> Expr t a -- | Substitute all occurrences of a variable with an expression -- -- 
--   subst x C B  ~  B[x := C]
--
subst :: Var -> Expr s a -> Expr t a -> Expr s a -- | shift is used by both normalization and type-checking to avoid -- variable capture by shifting variable indices -- -- For example, suppose that you were to normalize the following -- expression: -- -- 
--   λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
--
-- -- If you were to substitute y with x without shifting -- any variable indices, then you would get the following incorrect -- result: -- -- 
--   λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
--
-- -- In order to substitute x in place of y we need to -- shift x by 1 in order to avoid being -- misinterpreted as the x bound by the innermost lambda. If we -- perform that shift then we get the correct result: -- -- 
--   λ(a : Type) → λ(x : a) → λ(x : a) → x@1
--
-- -- As a more worked example, suppose that you were to normalize the -- following expression: -- -- 
--       λ(a : Type)
--   →   λ(f : a → a → a)
--   →   λ(x : a)
--   →   λ(x : a)
--   →   (λ(x : a) → f x x@1) x@1
--
-- -- The correct normalized result would be: -- -- 
--       λ(a : Type)
--   →   λ(f : a → a → a)
--   →   λ(x : a)
--   →   λ(x : a)
--   →   f x@1 x
--
-- -- The above example illustrates how we need to both increase and -- decrease variable indices as part of substitution: -- -- -- -- Formally, (shift d (V x n) e) modifies the expression -- e by adding d to the indices of all variables named -- x whose indices are greater than (n + m), where -- m is the number of bound variables of the same name within -- that scope -- -- In practice, d is always 1 or -1 because we -- either: -- -- -- -- n starts off at 0 when substitution begins and -- increments every time we descend into a lambda or let expression that -- binds a variable of the same name in order to avoid shifting the bound -- variables by mistake. shift :: Integer -> Var -> Expr s a -> Expr t a -- | Quickly check if an expression is in normal form isNormalized :: Expr s a -> Bool -- | Pretty-print a value pretty :: Buildable a => a -> Text -- | Utility function used to throw internal errors that should never -- happen (in theory) but that are not enforced by the type system internalError :: Text -> forall b. b instance (GHC.Show.Show a, GHC.Show.Show s) => GHC.Show.Show (Dhall.Core.Expr s a) instance Data.Traversable.Traversable (Dhall.Core.Expr s) instance Data.Foldable.Foldable (Dhall.Core.Expr s) instance GHC.Base.Functor (Dhall.Core.Expr s) instance GHC.Show.Show Dhall.Core.Var instance GHC.Classes.Eq Dhall.Core.Var instance GHC.Show.Show Dhall.Core.Path instance GHC.Classes.Ord Dhall.Core.Path instance GHC.Classes.Eq Dhall.Core.Path instance GHC.Enum.Enum Dhall.Core.Const instance GHC.Enum.Bounded Dhall.Core.Const instance GHC.Show.Show Dhall.Core.Const instance Data.Text.Buildable.Buildable Dhall.Core.Const instance Data.Text.Buildable.Buildable Dhall.Core.Path instance Data.String.IsString Dhall.Core.Var instance Data.Text.Buildable.Buildable Dhall.Core.Var instance GHC.Base.Applicative (Dhall.Core.Expr s) instance GHC.Base.Monad (Dhall.Core.Expr s) instance Data.Bifunctor.Bifunctor Dhall.Core.Expr instance Data.String.IsString (Dhall.Core.Expr s a) instance Data.Text.Buildable.Buildable a => Data.Text.Buildable.Buildable (Dhall.Core.Expr s a) -- | This module contains Dhall's parsing logic module Dhall.Parser -- | Parse an expression from Text containing a Dhall program exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path) -- | Parser for a top-level Dhall expression expr :: Parser (Expr Src Path) -- | Source code extract data Src Src :: Delta -> Delta -> ByteString -> Src -- | A parsing error newtype ParseError ParseError :: Doc -> ParseError -- | A Parser that is almost identical to -- Text.Trifecta.Parser except treating -- Haskell-style comments as whitespace newtype Parser a Parser :: Parser a -> Parser a [unParser] :: Parser a -> Parser a instance Text.Trifecta.Combinators.MarkParsing Text.Trifecta.Delta.Delta Dhall.Parser.Parser instance Text.Trifecta.Combinators.DeltaParsing Dhall.Parser.Parser instance Text.Parser.Char.CharParsing Dhall.Parser.Parser instance Text.Parser.Combinators.Parsing Dhall.Parser.Parser instance GHC.Base.MonadPlus Dhall.Parser.Parser instance GHC.Base.Alternative Dhall.Parser.Parser instance GHC.Base.Monad Dhall.Parser.Parser instance GHC.Base.Applicative Dhall.Parser.Parser instance GHC.Base.Functor Dhall.Parser.Parser instance GHC.Show.Show Dhall.Parser.Src instance Data.Text.Buildable.Buildable Dhall.Parser.Src instance Text.Parser.Token.TokenParsing Dhall.Parser.Parser instance GHC.Show.Show Dhall.Parser.ParseError instance GHC.Exception.Exception Dhall.Parser.ParseError -- | This is a utility module that consolidates all Context-related -- operations module Dhall.Context -- | A (Context a) associates Text labels with values of -- type a -- -- The Context is used for type-checking when (a = Expr -- X) -- -- -- -- The difference between a Context and a Map is that a -- Context lets you have multiple ordered occurrences of the same -- key and you can query for the nth occurrence of a given key. data Context a -- | An empty context with no key-value pairs empty :: Context a -- | Add a key-value pair to the Context insert :: Text -> a -> Context a -> Context a -- | Look up a key by name and index -- -- 
--   lookup _ _         empty  = Nothing
--   lookup k 0 (insert k v c) = Just v
--   lookup k n (insert k v c) = lookup k (n - 1) c  -- 1 <= n
--   lookup k n (insert j v c) = lookup k  n      c  -- k /= j
--
lookup :: Text -> Integer -> Context a -> Maybe a -- | Return all key-value associations as a list -- -- 
--   toList           empty  = []
--   toList (insert k v ctx) = (k, v) : toList ctx
--
toList :: Context a -> [(Text, a)] instance GHC.Base.Functor Dhall.Context.Context -- | This module contains the logic for type checking Dhall code module Dhall.TypeCheck -- | Type-check an expression and return the expression's type if -- type-checking suceeds or an error if type-checking fails -- -- typeWith does not necessarily normalize the type since full -- normalization is not necessary for just type-checking. If you actually -- care about the returned type then you may want to normalize -- it afterwards. typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X) -- | typeOf is the same as typeWith with an empty context, -- meaning that the expression must be closed (i.e. no free variables), -- otherwise type-checking will fail. typeOf :: Expr s X -> Either (TypeError s) (Expr s X) -- | Like Void, except with a shorter inferred type newtype X X :: (forall a. a) -> X [absurd] :: X -> forall a. a -- | A structured type error that includes context data TypeError s TypeError :: Context (Expr s X) -> Expr s X -> TypeMessage s -> TypeError s [context] :: TypeError s -> Context (Expr s X) [current] :: TypeError s -> Expr s X [typeMessage] :: TypeError s -> TypeMessage s -- | 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) -> DetailedTypeError s -- | The specific type error data TypeMessage s UnboundVariable :: TypeMessage s InvalidInputType :: (Expr s X) -> TypeMessage s InvalidOutputType :: (Expr s X) -> TypeMessage s NotAFunction :: (Expr s X) -> (Expr s X) -> TypeMessage s TypeMismatch :: (Expr s X) -> (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s AnnotMismatch :: (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s Untyped :: TypeMessage s InvalidListElement :: Int -> (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s InvalidListType :: (Expr s X) -> TypeMessage s InvalidOptionalElement :: (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s InvalidOptionalLiteral :: Int -> TypeMessage s InvalidOptionalType :: (Expr s X) -> TypeMessage s InvalidPredicate :: (Expr s X) -> (Expr s X) -> TypeMessage s IfBranchMismatch :: (Expr s X) -> (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s IfBranchMustBeTerm :: Bool -> (Expr s X) -> (Expr s X) -> (Expr s X) -> TypeMessage s InvalidField :: Text -> (Expr s X) -> TypeMessage s InvalidFieldType :: Text -> (Expr s X) -> TypeMessage s InvalidAlternative :: Text -> (Expr s X) -> TypeMessage s InvalidAlternativeType :: Text -> (Expr s X) -> TypeMessage s DuplicateAlternative :: Text -> TypeMessage s MustCombineARecord :: (Expr s X) -> (Expr s X) -> TypeMessage s FieldCollision :: Text -> TypeMessage s MustMergeARecord :: (Expr s X) -> (Expr s X) -> TypeMessage s MustMergeUnion :: (Expr s X) -> (Expr s X) -> TypeMessage s UnusedHandler :: (Set Text) -> TypeMessage s MissingHandler :: (Set Text) -> TypeMessage s HandlerInputTypeMismatch :: Text -> (Expr s X) -> (Expr s X) -> TypeMessage s HandlerOutputTypeMismatch :: Text -> (Expr s X) -> (Expr s X) -> TypeMessage s HandlerNotAFunction :: Text -> (Expr s X) -> TypeMessage s NotARecord :: Text -> (Expr s X) -> (Expr s X) -> TypeMessage s MissingField :: Text -> (Expr s X) -> TypeMessage s CantAnd :: (Expr s X) -> (Expr s X) -> TypeMessage s CantOr :: (Expr s X) -> (Expr s X) -> TypeMessage s CantEQ :: (Expr s X) -> (Expr s X) -> TypeMessage s CantNE :: (Expr s X) -> (Expr s X) -> TypeMessage s CantTextAppend :: (Expr s X) -> (Expr s X) -> TypeMessage s CantAdd :: (Expr s X) -> (Expr s X) -> TypeMessage s CantMultiply :: (Expr s X) -> (Expr s X) -> TypeMessage s NoDependentLet :: (Expr s X) -> (Expr s X) -> TypeMessage s NoDependentTypes :: (Expr s X) -> (Expr s X) -> TypeMessage s instance GHC.Show.Show s => GHC.Show.Show (Dhall.TypeCheck.TypeMessage s) instance GHC.Show.Show Dhall.TypeCheck.X instance Data.Text.Buildable.Buildable Dhall.TypeCheck.X instance Data.Text.Buildable.Buildable s => GHC.Show.Show (Dhall.TypeCheck.TypeError s) instance (Data.Text.Buildable.Buildable s, Data.Typeable.Internal.Typeable s) => GHC.Exception.Exception (Dhall.TypeCheck.TypeError s) instance Data.Text.Buildable.Buildable s => Data.Text.Buildable.Buildable (Dhall.TypeCheck.TypeError s) instance Data.Text.Buildable.Buildable s => GHC.Show.Show (Dhall.TypeCheck.DetailedTypeError s) instance (Data.Text.Buildable.Buildable s, Data.Typeable.Internal.Typeable s) => GHC.Exception.Exception (Dhall.TypeCheck.DetailedTypeError s) instance Data.Text.Buildable.Buildable s => Data.Text.Buildable.Buildable (Dhall.TypeCheck.DetailedTypeError s) -- | Dhall lets you import external expressions located either in local -- files or hosted on network endpoints. -- -- 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, if you create a file named id with -- the following contents: -- -- 
--   $ cat id
--   λ(a : Type) → λ(x : a) → x
--
-- -- Then you can use the file directly within a dhall program -- just by referencing the file's path: -- -- 
--   $ dhall
--   ./id Bool True
--   <Ctrl-D>
--   Bool
--   
--   True
--
-- -- Imported expressions may contain imports of their own, too, which will -- continue to be resolved. However, Dhall will prevent cyclic imports. -- For example, if you had these two files: -- -- 
--   $ cat foo
--   ./bar
--
-- -- 
--   $ cat bar
--   ./foo
--
-- -- ... Dhall would throw the following exception if you tried to import -- foo: -- -- 
--   $ dhall
--   ./foo
--   ^D
--   ↳ ./foo
--     ↳ ./bar
--   
--   Cyclic import: ./foo
--
-- -- You can also import expressions hosted on network endpoints. Just use -- the URL -- -- 
--   http://host[:port]/path
--
-- -- The compiler expects the downloaded expressions to be in the same -- format as local files, specifically UTF8-encoded source code text. -- -- For example, if our id expression were hosted at -- http://example.com/id, then we would embed the -- expression within our code using: -- -- 
--   http://example.com/id
--
-- -- You can also reuse directory names as expressions. If you provide a -- path to a local or remote directory then the compiler will look for a -- file named @ within that directory and use that file to -- represent the directory. module Dhall.Import -- | Parse an expression from a FilePath containing a Dhall program exprFromFile :: FilePath -> IO (Expr Src Path) -- | Parse an expression from a URL hosting a Dhall program exprFromURL :: Manager -> Text -> IO (Expr Src Path) -- | Resolve all imports within an expression load :: Expr Src Path -> IO (Expr Src X) -- | An import failed because of a cycle in the import graph newtype Cycle Cycle :: Path -> Cycle -- | The offending cyclic import [cyclicImport] :: Cycle -> Path -- | Dhall tries to ensure that all expressions hosted on network endpoints -- are weakly referentially transparent, meaning roughly that any two -- clients will compile the exact same result given the same URL. -- -- To be precise, a strong interpretaton of referential transparency -- means that if you compiled a URL you could replace the expression -- hosted at that URL with the compiled result. Let's term this "static -- linking". Dhall (very intentionally) does not satisfy this stronger -- interpretation of referential transparency since "statically linking" -- an expression (i.e. permanently resolving all imports) means that the -- expression will no longer update if its dependencies change. -- -- In general, either interpretation of referential transparency is not -- enforceable in a networked context since one can easily violate -- referential transparency with a custom DNS, but Dhall can still try to -- guard against common unintentional violations. To do this, Dhall -- enforces that a non-local import may not reference a local import. -- -- Local imports are defined as: -- -- -- -- All other imports are defined to be non-local newtype ReferentiallyOpaque ReferentiallyOpaque :: Path -> ReferentiallyOpaque -- | The offending opaque import [opaqueImport] :: ReferentiallyOpaque -> Path -- | Extend another exception with the current import stack data Imported e Imported :: [Path] -> e -> Imported e -- | Imports resolved so far, in reverse order [importStack] :: Imported e -> [Path] -- | The nested exception [nested] :: Imported e -> e -- | Newtype used to wrap HttpExceptions with a prettier Show -- instance newtype PrettyHttpException PrettyHttpException :: HttpException -> PrettyHttpException -- | Exception thrown when an imported file is missing data MissingFile MissingFile :: MissingFile instance GHC.Exception.Exception Dhall.Import.Cycle instance GHC.Show.Show Dhall.Import.Cycle instance GHC.Exception.Exception Dhall.Import.ReferentiallyOpaque instance GHC.Show.Show Dhall.Import.ReferentiallyOpaque instance GHC.Exception.Exception e => GHC.Exception.Exception (Dhall.Import.Imported e) instance GHC.Show.Show e => GHC.Show.Show (Dhall.Import.Imported e) instance GHC.Exception.Exception Dhall.Import.PrettyHttpException instance GHC.Show.Show Dhall.Import.PrettyHttpException instance GHC.Exception.Exception Dhall.Import.MissingFile instance GHC.Show.Show Dhall.Import.MissingFile -- | Please read the Dhall.Tutorial module, which contains a -- tutorial explaining how to use the language, the compiler, and this -- library module Dhall -- | Type-check and evaluate a Dhall program, decoding the result into -- Haskell -- -- The first argument determines the type of value that you decode: -- -- 
--   >>> input integer "2"
--   2
--   
--   >>> input (vector double) "[ 1.0, 2.0 ] : List Bool"
--   [1.0,2.0]
--
-- -- Use auto to automatically select which type to decode based on -- the inferred return type: -- -- 
--   >>> input auto "True" :: IO Bool
--   True
--
input :: Type a -> Text -> IO a -- | 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 -- | A (Type a) represents a way to marshal a value of type -- 'a' from Dhall into Haskell -- -- You can produce Types either explicitly: -- -- 
--   example :: Type (Vector Text)
--   example = vector text
--
-- -- ... or implicitly using auto: -- -- 
--   example :: Type (Vector Text)
--   example = auto
--
-- -- You can consume Types using the input function: -- -- 
--   input :: Type a -> Text -> IO a
--
data Type a -- | Any value that implements Interpret can be automatically -- decoded based on the inferred return type of input -- -- 
--   >>> input auto "[1, 2, 3 ] : List Integer" :: IO (Vector Integer)
--   [1,2,3]
--
-- -- This class auto-generates a default implementation for records that -- implement Generic. This does not auto-generate an instance for -- sum types nor recursive types. class Interpret a where auto = fmap to genericAuto auto :: Interpret a => Type a auto :: (Interpret a, Generic a, GenericInterpret (Rep a)) => Type a -- | Decode a Bool -- -- 
--   >>> input bool "True"
--   True
--
bool :: Type Bool -- | Decode a Natural -- -- 
--   >>> input natural "+42"
--   42
--
natural :: Type Natural -- | Decode an Integer -- -- 
--   >>> input integer "42"
--   42
--
integer :: Type Integer -- | Decode a Double -- -- 
--   >>> input double "42.0"
--   42.0
--
double :: Type Double -- | Decode Text -- -- 
--   >>> input text "\"Test\""
--   "Test"
--
text :: Type Text -- | Decode a Maybe -- -- 
--   >>> input (maybe integer) "[1] : Optional Integer"
--   Just 1
--
maybe :: Type a -> Type (Maybe a) -- | Decode a Vector -- -- 
--   >>> input (vector integer) "[ 1, 2, 3 ] : List Integer"
--   [1,2,3]
--
vector :: Type a -> Type (Vector a) -- | Type representing arbitrary-precision non-negative integers. -- -- Operations whose result would be negative throw -- (Underflow :: ArithException). data Natural :: * data Text :: * -- | Boxed vectors, supporting efficient slicing. data Vector a :: * -> * -- | Representable types of kind *. This class is derivable in GHC with the -- DeriveGeneric flag on. class Generic a instance GHC.Base.Functor Dhall.Type instance Dhall.Interpret GHC.Types.Bool instance Dhall.Interpret GHC.Natural.Natural instance Dhall.Interpret GHC.Integer.Type.Integer instance Dhall.Interpret GHC.Types.Double instance Dhall.Interpret Data.Text.Internal.Lazy.Text instance Dhall.Interpret a => Dhall.Interpret (GHC.Base.Maybe a) instance Dhall.Interpret a => Dhall.Interpret (Data.Vector.Vector a) instance Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.D d f) instance Dhall.GenericInterpret GHC.Generics.V1 instance (GHC.Generics.Constructor c1, GHC.Generics.Constructor c2, Dhall.GenericInterpret f1, Dhall.GenericInterpret f2) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c1 f1 GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c2 f2) instance (GHC.Generics.Constructor c, Dhall.GenericInterpret (f GHC.Generics.:+: g), Dhall.GenericInterpret h) => Dhall.GenericInterpret ((f GHC.Generics.:+: g) GHC.Generics.:+: GHC.Generics.M1 GHC.Generics.C c h) instance (GHC.Generics.Constructor c, Dhall.GenericInterpret f, Dhall.GenericInterpret (g GHC.Generics.:+: h)) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c f GHC.Generics.:+: (g GHC.Generics.:+: h)) instance (Dhall.GenericInterpret (f GHC.Generics.:+: g), Dhall.GenericInterpret (h GHC.Generics.:+: i)) => Dhall.GenericInterpret ((f GHC.Generics.:+: g) GHC.Generics.:+: (h GHC.Generics.:+: i)) instance Dhall.GenericInterpret f => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.C c f) instance Dhall.GenericInterpret GHC.Generics.U1 instance (Dhall.GenericInterpret f, Dhall.GenericInterpret g) => Dhall.GenericInterpret (f GHC.Generics.:*: g) instance (GHC.Generics.Selector s, Dhall.Interpret a) => Dhall.GenericInterpret (GHC.Generics.M1 GHC.Generics.S s (GHC.Generics.K1 i a)) -- | 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