dhall-1.0.2: A configuration language guaranteed to terminate

Safe HaskellNone
LanguageHaskell98

Dhall.Core

Contents

Description

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

Synopsis

Syntax

data Const Source #

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

Constructors

Type 
Kind 

data Path Source #

Path to an external resource

Constructors

File FilePath 
URL Text 

Instances

Eq Path Source # 

Methods

(==) :: Path -> Path -> Bool #

(/=) :: Path -> Path -> Bool #

Ord Path Source # 

Methods

compare :: Path -> Path -> Ordering #

(<) :: Path -> Path -> Bool #

(<=) :: Path -> Path -> Bool #

(>) :: Path -> Path -> Bool #

(>=) :: Path -> Path -> Bool #

max :: Path -> Path -> Path #

min :: Path -> Path -> Path #

Show Path Source # 

Methods

showsPrec :: Int -> Path -> ShowS #

show :: Path -> String #

showList :: [Path] -> ShowS #

Buildable Path Source # 

Methods

build :: Path -> Builder #

data Var Source #

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.

Constructors

V Text !Integer 

Instances

Eq Var Source # 

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Show Var Source # 

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

IsString Var Source # 

Methods

fromString :: String -> Var #

Buildable Var Source # 

Methods

build :: Var -> Builder #

data Expr s a Source #

Syntax tree for expressions

Constructors

Const Const
Const c                                  ~  c
Var Var
Var (V x 0)                              ~  x
Var (V x n)                              ~  x@n
Lam Text (Expr s a) (Expr s a)
Lam x     A b                            ~  λ(x : A) -> b
Pi Text (Expr s a) (Expr s a)
Pi "_" A B                               ~        A  -> B
Pi x   A B                               ~  ∀(x : A) -> B
App (Expr s a) (Expr s a)
App f a                                  ~  f a
Let Text (Maybe (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
Annot (Expr s a) (Expr s a)
Annot x t                                ~  x : t
Bool
Bool                                     ~  Bool
BoolLit Bool
BoolLit b                                ~  b
BoolAnd (Expr s a) (Expr s a)
BoolAnd x y                              ~  x && y
BoolOr (Expr s a) (Expr s a)
BoolOr  x y                              ~  x || y
BoolEQ (Expr s a) (Expr s a)
BoolEQ  x y                              ~  x == y
BoolNE (Expr s a) (Expr s a)
BoolNE  x y                              ~  x != y
BoolIf (Expr s a) (Expr s a) (Expr s a)
BoolIf x y z                             ~  if x then y else z
Natural
Natural                                  ~  Natural
NaturalLit Natural
NaturalLit n                             ~  +n
NaturalFold
NaturalFold                              ~  Natural/fold
NaturalBuild
NaturalBuild                             ~  Natural/build
NaturalIsZero
NaturalIsZero                            ~  Natural/isZero
NaturalEven
NaturalEven                              ~  Natural/even
NaturalOdd
NaturalOdd                               ~  Natural/odd
NaturalPlus (Expr s a) (Expr s a)
NaturalPlus x y                          ~  x + y
NaturalTimes (Expr s a) (Expr s a)
NaturalTimes x y                         ~  x * y
Integer
Integer                                  ~  Integer
IntegerLit Integer
IntegerLit n                             ~  n
Double
Double                                   ~  Double
DoubleLit Double
DoubleLit n                              ~  n
Text
Text                                     ~  Text
TextLit Builder
TextLit t                                ~  t
TextAppend (Expr s a) (Expr s a)
TextAppend x y                           ~  x ++ y
List
List                                     ~  List
ListLit (Expr s a) (Vector (Expr s a))
ListLit t [x, y, z]                      ~  [x, y, z] : List t
ListBuild
ListBuild                                ~  List/build
ListFold
ListFold                                 ~  List/fold
ListLength
ListLength                               ~  List/length
ListHead
ListHead                                 ~  List/head
ListLast
ListLast                                 ~  List/last
ListIndexed
ListIndexed                              ~  List/indexed
ListReverse
ListReverse                              ~  List/reverse
Optional
Optional                                 ~  Optional
OptionalLit (Expr s a) (Vector (Expr s a))
OptionalLit t [e]                        ~  [e] : Optional t
OptionalLit t []                         ~  []  : Optional t
OptionalFold
OptionalFold                             ~  Optional/fold
Record (Map Text (Expr s a))
Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }
RecordLit (Map Text (Expr s a))
RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }
Union (Map Text (Expr s a))
Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >
UnionLit Text (Expr s a) (Map Text (Expr s a))
UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 > 
Combine (Expr s a) (Expr s a)
Combine x y                              ~  x ∧ y
Merge (Expr s a) (Expr s a) (Expr s a)
Merge x y t                              ~  merge x y : t
Field (Expr s a) Text
Field e x                                ~  e.x
Note s (Expr s a)
Note s x                                 ~  e
Embed a
Embed path                               ~  path

Instances

Bifunctor Expr Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Expr a c -> Expr b d #

first :: (a -> b) -> Expr a c -> Expr b c #

second :: (b -> c) -> Expr a b -> Expr a c #

Monad (Expr s) Source # 

Methods

(>>=) :: Expr s a -> (a -> Expr s b) -> Expr s b #

(>>) :: Expr s a -> Expr s b -> Expr s b #

return :: a -> Expr s a #

fail :: String -> Expr s a #

Functor (Expr s) Source # 

Methods

fmap :: (a -> b) -> Expr s a -> Expr s b #

(<$) :: a -> Expr s b -> Expr s a #

Applicative (Expr s) Source # 

Methods

pure :: a -> Expr s a #

(<*>) :: Expr s (a -> b) -> Expr s a -> Expr s b #

(*>) :: Expr s a -> Expr s b -> Expr s b #

(<*) :: Expr s a -> Expr s b -> Expr s a #

Foldable (Expr s) Source # 

Methods

fold :: Monoid m => Expr s m -> m #

foldMap :: Monoid m => (a -> m) -> Expr s a -> m #

foldr :: (a -> b -> b) -> b -> Expr s a -> b #

foldr' :: (a -> b -> b) -> b -> Expr s a -> b #

foldl :: (b -> a -> b) -> b -> Expr s a -> b #

foldl' :: (b -> a -> b) -> b -> Expr s a -> b #

foldr1 :: (a -> a -> a) -> Expr s a -> a #

foldl1 :: (a -> a -> a) -> Expr s a -> a #

toList :: Expr s a -> [a] #

null :: Expr s a -> Bool #

length :: Expr s a -> Int #

elem :: Eq a => a -> Expr s a -> Bool #

maximum :: Ord a => Expr s a -> a #

minimum :: Ord a => Expr s a -> a #

sum :: Num a => Expr s a -> a #

product :: Num a => Expr s a -> a #

Traversable (Expr s) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Expr s a -> f (Expr s b) #

sequenceA :: Applicative f => Expr s (f a) -> f (Expr s a) #

mapM :: Monad m => (a -> m b) -> Expr s a -> m (Expr s b) #

sequence :: Monad m => Expr s (m a) -> m (Expr s a) #

(Show a, Show s) => Show (Expr s a) Source # 

Methods

showsPrec :: Int -> Expr s a -> ShowS #

show :: Expr s a -> String #

showList :: [Expr s a] -> ShowS #

IsString (Expr s a) Source # 

Methods

fromString :: String -> Expr s a #

Buildable a => Buildable (Expr s a) Source #

Generates a syntactically valid Dhall program

Methods

build :: Expr s a -> Builder #

Normalization

normalize :: Expr s a -> Expr t a Source #

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.

subst :: Var -> Expr s a -> Expr t a -> Expr s a Source #

Substitute all occurrences of a variable with an expression

subst x C B  ~  B[x := C]

shift :: Integer -> Var -> Expr s a -> Expr t a Source #

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:

  • We need to increase the index of the outer x@1 to x@2 before we substitute it into the body of the innermost lambda expression in order to avoid variable capture. This substitution changes the body of the lambda expression to (f x@2 x@1)
  • We then remove the innermost lambda and therefore decrease the indices of both xs in (f x@2 x@1) to (f x@1 x) in order to reflect that one less x variable is now bound within that scope

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:

  • increment variables by 1 to avoid variable capture during substitution
  • decrement variables by 1 when deleting lambdas after substitution

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.

isNormalized :: Expr s a -> Bool Source #

Quickly check if an expression is in normal form

Pretty-printing

pretty :: Buildable a => a -> Text Source #

Pretty-print a value

Miscellaneous

internalError :: Text -> forall b. b Source #

Utility function used to throw internal errors that should never happen (in theory) but that are not enforced by the type system