Dhall.Core

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

Syntax

data Const

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

Instances

Bounded Const

Methods

minBound :: Const

maxBound :: Const

Enum Const

Methods

succ :: Const -> Const

pred :: Const -> Const

toEnum :: Int -> Const

fromEnum :: Const -> Int

enumFrom :: Const -> [Const]

enumFromThen :: Const -> Const -> [Const]

enumFromTo :: Const -> Const -> [Const]

enumFromThenTo :: Const -> Const -> Const -> [Const]

Eq Const

Methods

(==) :: Const -> Const -> Bool

(/=) :: Const -> Const -> Bool

Show Const

Methods

showsPrec :: Int -> Const -> ShowS

show :: Const -> String

showList :: [Const] -> ShowS

Buildable Const

Methods

build :: Const -> Builder

data HasHome

Whether or not a path is relative to the user's home directory

Constructors

Home

Homeless

Instances

Eq HasHome

Methods

(==) :: HasHome -> HasHome -> Bool

(/=) :: HasHome -> HasHome -> Bool

Ord HasHome

Methods

compare :: HasHome -> HasHome -> Ordering

(<) :: HasHome -> HasHome -> Bool

(<=) :: HasHome -> HasHome -> Bool

(>) :: HasHome -> HasHome -> Bool

(>=) :: HasHome -> HasHome -> Bool

max :: HasHome -> HasHome -> HasHome

min :: HasHome -> HasHome -> HasHome

Show HasHome

Methods

showsPrec :: Int -> HasHome -> ShowS

show :: HasHome -> String

showList :: [HasHome] -> ShowS

data PathType

The type of path to import (i.e. local vs. remote vs. environment)

Constructors

File HasHome FilePath

Local path

URL Text (Maybe PathHashed)

URL of emote resource and optional headers stored in a path

Env Text

Environment variable

Instances

Eq PathType

Methods

(==) :: PathType -> PathType -> Bool

(/=) :: PathType -> PathType -> Bool

Ord PathType

Methods

compare :: PathType -> PathType -> Ordering

(<) :: PathType -> PathType -> Bool

(<=) :: PathType -> PathType -> Bool

(>) :: PathType -> PathType -> Bool

(>=) :: PathType -> PathType -> Bool

max :: PathType -> PathType -> PathType

min :: PathType -> PathType -> PathType

Show PathType

Methods

showsPrec :: Int -> PathType -> ShowS

show :: PathType -> String

showList :: [PathType] -> ShowS

Buildable PathType

Methods

build :: PathType -> Builder

data PathHashed

A PathType extended with an optional hash for semantic integrity checks

Constructors

PathHashed

Fields

• hash :: Maybe (Digest SHA256)
• pathType :: PathType

Instances

Eq PathHashed

Methods

(==) :: PathHashed -> PathHashed -> Bool

(/=) :: PathHashed -> PathHashed -> Bool

Ord PathHashed

Methods

compare :: PathHashed -> PathHashed -> Ordering

(<) :: PathHashed -> PathHashed -> Bool

(<=) :: PathHashed -> PathHashed -> Bool

(>) :: PathHashed -> PathHashed -> Bool

(>=) :: PathHashed -> PathHashed -> Bool

max :: PathHashed -> PathHashed -> PathHashed

min :: PathHashed -> PathHashed -> PathHashed

Show PathHashed

Methods

showsPrec :: Int -> PathHashed -> ShowS

show :: PathHashed -> String

showList :: [PathHashed] -> ShowS

Buildable PathHashed

Methods

build :: PathHashed -> Builder

data PathMode

How to interpret the path's contents (i.e. as Dhall code or raw text)

Constructors

Code

RawText

Instances

Eq PathMode

Methods

(==) :: PathMode -> PathMode -> Bool

(/=) :: PathMode -> PathMode -> Bool

Ord PathMode

Methods

compare :: PathMode -> PathMode -> Ordering

(<) :: PathMode -> PathMode -> Bool

(<=) :: PathMode -> PathMode -> Bool

(>) :: PathMode -> PathMode -> Bool

(>=) :: PathMode -> PathMode -> Bool

max :: PathMode -> PathMode -> PathMode

min :: PathMode -> PathMode -> PathMode

Show PathMode

Methods

showsPrec :: Int -> PathMode -> ShowS

show :: PathMode -> String

showList :: [PathMode] -> ShowS

data Path

Path to an external resource

Constructors

Path

Fields

• pathHashed :: PathHashed
• pathMode :: PathMode

Instances

Eq Path

Methods

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

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

Ord Path

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

Methods

showsPrec :: Int -> Path -> ShowS

show :: Path -> String

showList :: [Path] -> ShowS

Buildable Path

Methods

build :: Path -> Builder

Pretty Path

Methods

pretty :: Path -> Doc ann

prettyList :: [Path] -> Doc ann

data Var

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 : Type) → λ(y : Type) → λ(x : Type) → 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

Methods

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

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

Show Var

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

IsString Var

Methods

fromString :: String -> Var

Buildable Var

Methods

build :: Var -> Builder

data Chunks s a

The body of an interpolated Text literal

Constructors

Chunks [(Builder, Expr s a)] Builder

Instances

Functor (Chunks s)

Methods

fmap :: (a -> b) -> Chunks s a -> Chunks s b

(<$) :: a -> Chunks s b -> Chunks s a

Foldable (Chunks s)

Methods

fold :: Monoid m => Chunks s m -> m

foldMap :: Monoid m => (a -> m) -> Chunks s a -> m

foldr :: (a -> b -> b) -> b -> Chunks s a -> b

foldr' :: (a -> b -> b) -> b -> Chunks s a -> b

foldl :: (b -> a -> b) -> b -> Chunks s a -> b

foldl' :: (b -> a -> b) -> b -> Chunks s a -> b

foldr1 :: (a -> a -> a) -> Chunks s a -> a

foldl1 :: (a -> a -> a) -> Chunks s a -> a

toList :: Chunks s a -> [a]

null :: Chunks s a -> Bool

length :: Chunks s a -> Int

elem :: Eq a => a -> Chunks s a -> Bool

maximum :: Ord a => Chunks s a -> a

minimum :: Ord a => Chunks s a -> a

sum :: Num a => Chunks s a -> a

product :: Num a => Chunks s a -> a

Traversable (Chunks s)

Methods

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

sequenceA :: Applicative f => Chunks s (f a) -> f (Chunks s a)

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

sequence :: Monad m => Chunks s (m a) -> m (Chunks s a)

(Eq s, Eq a) => Eq (Chunks s a)

Methods

(==) :: Chunks s a -> Chunks s a -> Bool

(/=) :: Chunks s a -> Chunks s a -> Bool

(Show s, Show a) => Show (Chunks s a)

Methods

showsPrec :: Int -> Chunks s a -> ShowS

show :: Chunks s a -> String

showList :: [Chunks s a] -> ShowS

IsString (Chunks s a)

Methods

fromString :: String -> Chunks s a

Semigroup (Chunks s a)

Methods

(<>) :: Chunks s a -> Chunks s a -> Chunks s a

sconcat :: NonEmpty (Chunks s a) -> Chunks s a

stimes :: Integral b => b -> Chunks s a -> Chunks s a

Monoid (Chunks s a)

Methods

mempty :: Chunks s a

mappend :: Chunks s a -> Chunks s a -> Chunks s a

mconcat :: [Chunks s a] -> Chunks s a

data Expr s a

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

NaturalToInteger

NaturalToInteger                         ~  Natural/toInteger

NaturalShow

NaturalShow                              ~  Natural/show

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

IntegerShow

IntegerShow                              ~  Integer/show

Double

Double                                   ~  Double

DoubleLit Scientific

DoubleLit n                              ~  n

DoubleShow

DoubleShow                               ~  Double/show

Text

Text                                     ~  Text

TextLit (Chunks s a)

TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~  "t1${e1}t2${e2}t3"

TextAppend (Expr s a) (Expr s a)

TextAppend x y                           ~  x ++ y

List

List                                     ~  List

ListLit (Maybe (Expr s a)) (Seq (Expr s a))

ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
ListLit  Nothing  [x, y, z]              ~  [x, y, z]

ListAppend (Expr s a) (Expr s a)

ListAppend x y                           ~  x # y

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) (Maybe (Expr s a))

OptionalLit t (Just e)                   ~  [e] : Optional t
OptionalLit t Nothing                    ~  []  : Optional t

OptionalFold

OptionalFold                             ~  Optional/fold

OptionalBuild

OptionalBuild                            ~  Optional/build

Record (InsOrdHashMap Text (Expr s a))

Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }

RecordLit (InsOrdHashMap Text (Expr s a))

RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }

Union (InsOrdHashMap Text (Expr s a))

Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1 | k2 : t2 >

UnionLit Text (Expr s a) (InsOrdHashMap 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

Prefer (Expr s a) (Expr s a)

CombineRight x y                         ~  x ⫽ y

Merge (Expr s a) (Expr s a) (Maybe (Expr s a))

Merge x y (Just t )                      ~  merge x y : t
Merge x y  Nothing                       ~  merge x y

Constructors (Expr s a)

Constructors e                           ~  constructors e

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

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)

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)

Methods

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

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

Applicative (Expr s)

Methods

pure :: a -> Expr s a

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

liftA2 :: (a -> b -> c) -> Expr s a -> Expr s b -> Expr s c

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

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

Foldable (Expr s)

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)

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)

(Eq s, Eq a) => Eq (Expr s a)

Methods

(==) :: Expr s a -> Expr s a -> Bool

(/=) :: Expr s a -> Expr s a -> Bool

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

Methods

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

show :: Expr s a -> String

showList :: [Expr s a] -> ShowS

IsString (Expr s a)

Methods

fromString :: String -> Expr s a

Buildable a => Buildable (Expr s a)

Generates a syntactically valid Dhall program

Methods

build :: Expr s a -> Builder

Pretty a => Pretty (Expr s a)

Methods

pretty :: Expr s a -> Doc ann

prettyList :: [Expr s a] -> Doc ann

Normalization

alphaNormalize :: Expr s a -> Expr s a

α-normalize an expression by renaming all variables to "_" and using De Bruijn indices to distinguish them

normalize :: Eq a => Expr s a -> Expr t 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.

normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a

Reduce an expression to its normal form, performing beta reduction and applying any custom definitions.

normalizeWith is designed to be used with function typeWith. The typeWith function allows typing of Dhall functions in a custom typing context whereas normalizeWith allows evaluating Dhall expressions in a custom context.

To be more precise normalizeWith applies the given normalizer when it finds an application term that it cannot reduce by other means.

Note that the context used in normalization will determine the properties of normalization. That is, if the functions in custom context are not total then the Dhall language, evaluated with those functions is not total either.

type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)

Use this to wrap you embedded functions (see normalizeWith) to make them polymorphic enough to be used.

judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool

Returns True if two expressions are α-equivalent and β-equivalent and False otherwise

subst :: Var -> Expr s a -> Expr s a -> Expr s a

Substitute all occurrences of a variable with an expression

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

shift :: Integer -> Var -> Expr s 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:

• 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

Quickly check if an expression is in normal form

isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool

Check if an expression is in a normal form given a context of evaluation. Unlike isNormalized, this will fully normalize and traverse through the expression.

It is much more efficient to use isNormalized.

denote :: Expr s a -> Expr t a

Remove all Note constructors from an Expr (i.e. de-Note)

Pretty-printing

pretty :: Pretty a => a -> Text

Miscellaneous

internalError :: Text -> forall b. b

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

reservedIdentifiers :: HashSet Text

The set of reserved identifiers for the Dhall language

escapeText :: Builder -> Builder