| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Dhall.Core
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
- data Const
- newtype Directory = Directory {
- components :: [Text]
- data File = File {}
- data FilePrefix
- data Import = Import {}
- data ImportHashed = ImportHashed {
- hash :: Maybe (Digest SHA256)
- importType :: ImportType
- data ImportMode
- data ImportType
- type Path = Import
- data Var = V Text !Integer
- data Chunks s a = Chunks [(Builder, Expr s a)] Builder
- data Expr s a
- = Const Const
- | Var Var
- | Lam Text (Expr s a) (Expr s a)
- | Pi Text (Expr s a) (Expr s a)
- | App (Expr s a) (Expr s a)
- | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)
- | Annot (Expr s a) (Expr s a)
- | Bool
- | BoolLit Bool
- | BoolAnd (Expr s a) (Expr s a)
- | BoolOr (Expr s a) (Expr s a)
- | BoolEQ (Expr s a) (Expr s a)
- | BoolNE (Expr s a) (Expr s a)
- | BoolIf (Expr s a) (Expr s a) (Expr s a)
- | Natural
- | NaturalLit Natural
- | NaturalFold
- | NaturalBuild
- | NaturalIsZero
- | NaturalEven
- | NaturalOdd
- | NaturalToInteger
- | NaturalShow
- | NaturalPlus (Expr s a) (Expr s a)
- | NaturalTimes (Expr s a) (Expr s a)
- | Integer
- | IntegerLit Integer
- | IntegerShow
- | Double
- | DoubleLit Scientific
- | DoubleShow
- | Text
- | TextLit (Chunks s a)
- | TextAppend (Expr s a) (Expr s a)
- | List
- | ListLit (Maybe (Expr s a)) (Seq (Expr s a))
- | ListAppend (Expr s a) (Expr s a)
- | ListBuild
- | ListFold
- | ListLength
- | ListHead
- | ListLast
- | ListIndexed
- | ListReverse
- | Optional
- | OptionalLit (Expr s a) (Maybe (Expr s a))
- | OptionalFold
- | OptionalBuild
- | Record (InsOrdHashMap Text (Expr s a))
- | RecordLit (InsOrdHashMap Text (Expr s a))
- | Union (InsOrdHashMap Text (Expr s a))
- | UnionLit Text (Expr s a) (InsOrdHashMap Text (Expr s a))
- | Combine (Expr s a) (Expr s a)
- | CombineTypes (Expr s a) (Expr s a)
- | Prefer (Expr s a) (Expr s a)
- | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
- | Constructors (Expr s a)
- | Field (Expr s a) Text
- | Project (Expr s a) (Set Text)
- | Note s (Expr s a)
- | Embed a
- alphaNormalize :: Expr s a -> Expr s a
- normalize :: Eq a => Expr s a -> Expr t a
- normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a
- type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)
- judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
- subst :: Var -> Expr s a -> Expr s a -> Expr s a
- shift :: Integer -> Var -> Expr s a -> Expr s a
- isNormalized :: Expr s a -> Bool
- isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
- denote :: Expr s a -> Expr t a
- pretty :: Pretty a => a -> Text
- internalError :: Text -> forall b. b
- reservedIdentifiers :: HashSet Text
- escapeText :: Builder -> Builder
Syntax
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
Internal representation of a directory that stores the path components in reverse order
In other words, the directory foobar/baz is encoded as
Directory { components = [ "baz", "bar", "foo" ] }
Constructors
| Directory | |
Fields
| |
data FilePrefix Source #
Constructors
| Absolute | Absolute path |
| Here | Path relative to |
| Parent | Path relative to |
| Home | Path relative to |
Instances
Reference to an external resource
Constructors
| Import | |
Fields | |
data ImportHashed Source #
A ImportType extended with an optional hash for semantic integrity checks
Constructors
| ImportHashed | |
Fields
| |
data ImportMode Source #
How to interpret the import's contents (i.e. as Dhall code or raw text)
Instances
data ImportType Source #
The type of import (i.e. local vs. remote vs. environment)
Constructors
| Local FilePrefix File | Local path |
| URL Text File Text (Maybe ImportHashed) | URL of remote resource and optional headers stored in an import |
| Env Text | Environment variable |
Instances
Deprecated: Use Dhall.Core.Import instead
Type synonym for Import, provided for backwards compatibility
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@1This 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) → xZero indices are omitted when pretty-printing Vars and non-zero indices
appear as a numeric suffix.
The body of an interpolated Text literal
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 k v [(k1, t1), (k2, t2)] ~ < k = v | k1 : t1 | k2 : t2 > |
| Combine (Expr s a) (Expr s a) | Combine x y ~ x ∧ y |
| CombineTypes (Expr s a) (Expr s a) | CombineTypes 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 |
| Project (Expr s a) (Set Text) | Project e xs ~ e.{ xs } |
| Note s (Expr s a) | Note s x ~ e |
| Embed a | Embed import ~ import |
Instances
| Bifunctor Expr Source # | |
| Monad (Expr s) Source # | |
| Functor (Expr s) Source # | |
| Applicative (Expr s) Source # | |
| Foldable (Expr s) Source # | |
| Traversable (Expr s) Source # | |
| (Eq s, Eq a) => Eq (Expr s a) Source # | |
| (Show s, Show a) => Show (Expr s a) Source # | |
| IsString (Expr s a) Source # | |
| Buildable a => Buildable (Expr s a) Source # | Generates a syntactically valid Dhall program |
| Pretty a => Pretty (Expr s a) Source # | |
Normalization
alphaNormalize :: Expr s a -> Expr s a Source #
α-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 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.
normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a Source #
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) Source #
Use this to wrap you embedded functions (see normalizeWith) to make them
polymorphic enough to be used.
subst :: Var -> Expr s a -> Expr s 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 s 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@1tox@2before 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 lessxvariable 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
1to avoid variable capture during substitution - decrement variables by
1when 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
isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool Source #
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.
Pretty-printing
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
reservedIdentifiers :: HashSet Text Source #
The set of reserved identifiers for the Dhall language
escapeText :: Builder -> Builder Source #