Built-in types, functions, and operators

A list of all available built-in functionality

This section describes all of the types, functions, and operators built into the Dhall language.

Note that this page does not yet include certain keywords, such as:

  • let/in - Used to define intermediate expressions
  • merge - Used to consume unions
  • toMap - Used to convert records to dictionaries
  • using/as - Used to modify imports
  • assert - Used to write tests

However, in the meantime you can still consult the Cheatsheet to get an intuition for how these keywords work.

Bool

Example

$ dhall --annotate <<< 'Bool'
Bool : Type

Type

────────────────
Γ ⊢ Bool : Type

Literals: Bool

Example

$ dhall --annotate <<< 'True'
True : Bool

Type

───────────────
Γ ⊢ True : Bool
────────────────
Γ ⊢ False : Bool

Construct: if/then/else

Example

$ dhall <<< 'if True then 3 else 5'
3

Type

               Γ ⊢ t : Type
               ─────────────────────
Γ ⊢ b : Bool   Γ ⊢ l : t   Γ ⊢ r : t
────────────────────────────────────
Γ ⊢ if b then l else r : t

Rules

if b then True else False = b

if True  then l else r = l

if False then l else r = r

Operator: ||

Example

$ dhall <<< 'True || False'
True

Type

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x || y : Bool

Rules

x || False = x

False || x = x

(x || y) || z = x || (y || z)

x || True = True

True || x = True

x || (y && z) = (x || y) && (x || z)

(x && y) || z = (x || z) && (y || z)

Operator: &&

Example

$ dhall <<< 'True && False'
False

Type

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x && y : Bool

Rules

x && True = x

True && x = x

(x && y) && z = x && (y && z)

x && False = False

False && x = False

x && (y || z) = (x && y) || (x && z)

(x || y) && z = (x && z) || (y && z)

Operator: ==

Example

$ dhall <<< 'True == False'
False

Type

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x == y : Bool

Rules

x == x = True

x == True = x

True == x = x

(x == y) == z = x == (y == z)

Operator: !=

Example

$ dhall <<< 'True != False'
True

Type

Γ ⊢ x : Bool   Γ ⊢ y : Bool
───────────────────────────
Γ ⊢ x != y : Bool

Rules

x != x = False

False != x = x

x != False = x

(x != y) != z = x != (y != z)

Natural

Example

$ dhall --annotate <<< 'Natural'
Natural : Type

Type

──────────────────
Γ ⊢ Natural : Type

Literals: Natural

A Natural number literal is an unsigned non-negative integer

Example

$ dhall --annotate <<< '2'
2 : Natural
$ dhall --annotate <<< '0xFF'
255 : Natural
$ dhall --annotate <<< '0xff'
255 : Natural

Type

────────────────
Γ ⊢ n : Natural

Rules

n = 1 + 1 + … + 1 + 1  -- n times

Operator: +

Example

$ dhall <<< '2 + 3'
5

Type

Γ ⊢ x : Natural   Γ ⊢ y : Natural
─────────────────────────────────
Γ ⊢ x + y : Natural

Rules

x + 0 = x

0 + x = x

(x + y) + z = x + (y + z)

Operator: *

Example

$ dhall <<< '2 * 3'
6

Type

Γ ⊢ x : Natural   Γ ⊢ y : Natural
─────────────────────────────────
Γ ⊢ x * y : Natural

Rules

x * 1 = x

1 * x = x

(x * y) * z = x * (y * z)

x * 0 = 0

0 * x = 0

(x + y) * z = (x * z) + (y * z)

x * (y + z) = (x * y) + (x * z)

Function: Natural/even

Example

$ dhall <<< 'Natural/even 6'
True

Type

─────────────────────────────────
Γ ⊢ Natural/even : Natural → Bool

Rules

Natural/even 0 = True

Natural/even (x + y) = Natural/even x == Natural/even y

Natural/even 1 = False

Natural/even (x * y) = Natural/even x || Natural/even y

Function: Natural/odd

Example

$ dhall <<< 'Natural/odd 6'
False

Type

────────────────────────────────
Γ ⊢ Natural/odd : Natural → Bool

Rules

Natural/odd 0 = False

Natural/odd (x + y) = Natural/odd x != Natural/odd y

Natural/odd 1 = True

Natural/odd (x * y) = Natural/odd x && Natural/odd y

Function: Natural/isZero

Example

$ dhall <<< 'Natural/isZero 6'
False

Type

───────────────────────────────────
Γ ⊢ Natural/isZero : Natural → Bool

Rules

Natural/isZero 0 = True

Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y

Natural/isZero 1 = False

Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y

Function: Natural/subtract

Examples

$ dhall <<< 'Natural/subtract 1 3'
2
$ dhall <<< 'Natural/subtract 3 1'
0

Type

──────────────────────────────────────────────────
Γ ⊢ Natural/subtract : Natural → Natural → Natural

Rules

Natural/subtract 0 x = x

Natural/subtract x 0 = 0

Natural/subtract x x = 0

Natural/subtract y (x + y) = x

Function: Natural/fold

Example

$ dhall <<< 'Natural/fold 40 Text (λ(t : Text) → t ++ "!") "Hello"'
"Hello!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"

Type

──────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Natural/fold : Natural → ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural

Rules

Natural/fold 0 n s z = z

Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z)

Natural/fold 1 n s = s

Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s)

Function: Natural/build

Example

$ dhall <<< 'Natural/build (λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ zero))'
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

Function Natural/show

Example

$ dhall <<< 'Natural/show 42'
"42"

Type

─────────────────────────────────
Γ ⊢ Natural/show : Natural → Text

Function Natural/toInteger

Example

$ dhall <<< 'Natural/toInteger 2'
+2

Type

─────────────────────────────────────────
Γ ⊢ Natural/toInteger : Natural → Integer

Integer

Example

$ dhall --annotate <<< 'Integer'
Integer : Type

Type

────────────────
Γ ⊢ Integer : Type

Literals: Integer

An Integer literal is a either a non-negative integer prefixed with a + or a negative integer prefixed with a -.

Examples

$ dhall --annotate <<< '+3'
+3 : Integer
$ dhall --annotate <<< '-2'
-2 : Integer
$ dhall --annotate <<< '+0xFF'
+255 : Integer
$ dhall --annotate <<< '+0xff'
+255 : Integer

Type

────────────────
Γ ⊢ ±n : Integer

Function Integer/negate

Example

$ dhall <<< 'Integer/negate +2'
-2
$ dhall <<< 'Integer/negate -3'
+3

Type

──────────────────────────────────────
Γ ⊢ Integer/negate : Integer → Integer

Rules

Integer/negate (Integer/negate x) = x

Function Integer/clamp

Example

$ dhall <<< 'Integer/clamp +2'
2
$ dhall <<< 'Integer/clamp -3'
0

Type

─────────────────────────────────────
Γ ⊢ Integer/clamp : Integer → Natural

Rules

Natural/isZero (Integer/clamp -x) = True

Integer/clamp (Natural/toInteger x) = x

Natural/isZero (Integer/clamp x) || Natural/isZero (Integer/clamp (Integer/negate x)) = True

Function Integer/toDouble

Example

$ dhall <<< 'Integer/toDouble +2'
2.0
$ dhall <<< 'Integer/toDouble -3'
-3.0

Type

───────────────────────────────────────
Γ ⊢ Integer/toDouble : Integer → Double

Function Integer/show

Example

$ dhall <<< 'Integer/show +2'
"+2"
$ dhall <<< 'Integer/show -3'
"-3"

Type

─────────────────────────────────
Γ ⊢ Integer/show : Integer → Text

Double

Example

$ dhall --annotate <<< 'Double'
Double : Type

Type

────────────────
Γ ⊢ Double : Type

Literals: Double

A Double literal must have either at least one decimal place or an exponent (or both):

Examples

$ dhall --annotate <<< '3.14159'
3.14159 : Double
$ dhall --annotate <<< '-2e10'
-2.0e10 : Double

Type

────────────────
Γ ⊢ n.n : Double

Function Double/show

Example

$ dhall <<< 'Double/show 2.0'
"2.0"
$ dhall <<< 'Double/show -1e2'
"-100"

Type

───────────────────────────────
Γ ⊢ Double/show : Double → Text

Text

Example

$ dhall --annotate <<< 'Text'
Text : Type

Type

────────────────
Γ ⊢ Text : Type

Literals: Text

A Text literal is either a double-quoted string literal with JSON-style escaping rules or a Nix-style multi-line string literal:

Examples

$ dhall --annotate <<< '"ABC"'
"ABC" : Text
$ dhall <<EOF
> ''
>     Line 1
>     Line 2
> ''
> EOF
"Line 1\nLine 2\n"

Type

────────────────
Γ ⊢ "…" : Text

Rules

"abc…xyz" = "a" ++ "b" ++ "c" ++++ "x" ++ "y" ++ "z"

Function Text/show

Example

$ dhall <<< 'Text/show "ABC"'
"\"ABC\""
$ dhall <<< 'Text/show "\n🎉"'
"\"\\n🎉\""

Type

───────────────────────────
Γ ⊢ Text/show : Text → Text

Operator: ++

Example

$ dhall <<< '"Hello, " ++ "world!"'
"Hello, world!"

Type

Γ ⊢ x : Text   Γ ⊢ y : Text
───────────────────────────
Γ ⊢ x ++ y : Text

Rules

(x ++ y) ++ z = x ++ (y ++ z)

x ++ "" = x

"" ++ x = x

List

Example

$ dhall --annotate <<< 'List'
List : TypeType

Type

──────────────────────
Γ ⊢ List : Type → Type

Literals: List

A List literal is a sequence of 0 or more comma-separated values inside square brackets.

An empty List literal must end with a type annotation.

Examples

$ dhall --annotate <<< '[ 1, 2, 3 ]'
[ 1, 2, 3 ] : List Natural
dhall <<< '[] : List Natural'
[] : List Natural

Type

Γ ⊢ t : Type   Γ ⊢ x : t   Γ ⊢ y : t   …
────────────────────────────────────────
Γ ⊢ [x, y, … ] : List t

Rules

[ a, b, c,, x, y, z ] = [ a ] # [ b ] # [ c ] # … # [ x ] # [ y ] # [ z ]

Operator: #

Example

$ dhall <<< '[ 1, 2, 3] # [ 4, 5, 6 ]'
[ 1, 2, 3, 4, 5, 6, ]

Type

Γ ⊢ x : List a    Γ ⊢ y : List a
─────────────────────────────────
Γ ⊢ x # y : List a

Rules

([] : List a) # xs = xs

xs # ([] : List a) = xs

(xs # ys) # zs = xs # (ys # zs)

Function: List/fold

Example

$ dhall <<< 'List/fold Bool [True, False, True] Bool (λ(x : Bool) → λ(y : Bool) → x && y) True'
False

Type

────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ List/fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list

Rules

List/fold a ([] : List a) b c n = n

List/fold a (xs # ys) b c n = List/fold a xs b c (List/fold ys b c n)

List/fold a ([x] : List a) b c = c x

Function: List/build

Example

$ dhall <<< 'List/build Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))'
[1, 2, 3]

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

Function: List/length

Example

$ dhall <<< 'List/length Natural [ 1, 2, 3 ]'
3

Type

────────────────────────────────────────────────
Γ ⊢ List/length : ∀(a : Type) → List a → Natural

Rules

List/length t ([] : List t) = 0

List/length t (xs # ys) = List/length t xs + List/length t ys

List/length t [ x ] = 1

Function: List/head

$ dhall <<< 'List/head Natural [ 1, 2, 3 ]'
Some 1

Type

───────────────────────────────────────────────
Γ ⊢ List/head ∀(a : Type) → List a → Optional a

Rules

List/head a ([] : List a) = None a

List/head a (xs # ys) =
      let combine =
              λ(a : Type)
            → λ(l : Optional a)
            → λ(r : Optional a)
            → Optional/fold a l (Optional a) (λ(x : a) → Some x) r
  in  combine a (List/head a xs) (List/head a ys)

List/head a [ x ] = Some x

Function: List/last

Example

$ dhall <<< 'List/last Natural [ 1, 2, 3 ]'
Some 3

Type

─────────────────────────────────────────────────
Γ ⊢ List/last : ∀(a : Type) → List a → Optional a

Rules

List/last a ([] : List a) = None a

List/last a (xs # ys) =
      let combine =
              λ(a : Type)
            → λ(l : Optional a)
            → λ(r : Optional a)
            → Optional/fold a r (Optional a) (λ(x : a) → Some x) l
  in  combine a (List/last a xs) (List/last a ys)

List/last a [ x ] = Some x

Function: List/indexed

Example

$ dhall <<< 'List/indexed Text [ "ABC", "DEF", "GHI" ]'
[{ 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

List/indexed a ([] : List a) = [] : List { index : Natural, value : a }

List/indexed a (xs # ys) =
      let combine =
          λ(a : Type)
        → λ(xs : List { index : Natural, value : a })
        → λ(ys : List { index : Natural, value : a })
        →   xs
          # List/build
            { index : Natural, value : a }
            (   λ(list : Type)
              → λ(cons : { index : Natural, value : a } → list → list)
              → List/fold
                { index : Natural, value : a }
                ys
                list
                (   λ(x : { index : Natural, value : a })
                  → cons
                    { index = x.index + List/length { index : Natural, value : a } xs
                    , value = x.value
                    }
                )
            )
  in  combine a (List/indexed a xs) (List/indexed a ys)

List/indexed a [ x ] = [ { index = 0, value = x } ]

Function: List/reverse

Example

$ dhall <<< 'List/reverse Natural [ 1, 2, 3 ]'
[ 3, 2, 1 ]

Type

─────────────────────────────────────────────────
Γ ⊢ List/reverse : ∀(a : Type) → List a → List a

Rules

List/reverse a ([] : List a) = [] : List a

List/reverse a [ x ] = [ x ]

List/reverse a (List/reverse a xs) = xs

List/reverse a (xs # ys) = List/reverse a ys # List/reverse a xs

List/head a (List/reverse a xs) = List/last a xs

List/last a (List/reverse a xs) = List/head a xs

List/length a (List/reverse a xs) = List/length a xs

Optional

Example

$ dhall --annotate <<< 'Optional'
Optional : TypeType

Type

──────────────────────────
Γ ⊢ Optional : Type → Type

Literals: Optional

An Optional literal is either a present value wrapped in a Some or an absent value using None followed by a type

Example

$ dhall --annotate <<< 'None Natural'
None Natural : Optional Natural
$ dhall --annotate <<< 'Some 1'
Some 1 : Optional Natural

Type

Γ ⊢ t : Type   Γ ⊢ x : t
────────────────────────
Γ ⊢ Some x : Optional t
Γ ⊢ t : Type
───────────────────────
Γ ⊢ None t : Optional t

Function: Optional/fold

Example

$ dhall <<< 'Optional/fold Text (Some "ABC") Text (λ(t : Text) → t) ""'
"ABC"

Type

─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Optional/fold : ∀(a : Type) → Optional a → ∀(optional : Type) → ∀(just : a → optional) → ∀(nothing : optional) → optional

Rules

Optional/fold a (None a) o j n = n

Optional/fold a (Some x) o j n = j x

Function: Optional/build

Example

$ dhall <<< 'Optional/build Text (λ(optional : Type) → λ(just : Text → optional) → λ(nothing : optional) → just "abc")'
Some "abc"

Type

────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Γ ⊢ Optional/build : ∀(a : Type) → (∀(optional : Type) → ∀(just : a → optional) → ∀(nothing : optional) → optional) → Optional a

Rules

Optional/build t (Optional/fold t x) = x

Optional/fold t (Optional/build t x) = x

Records

Record types

A record type is a sequence of 0 or more key-type pairs inside curly braces.

Examples

$ dhall --annotate <<< '{ foo : Natural, bar : Bool }'
{ foo : Natural, bar : Bool } : Type
$ dhall --annotate <<< '{}'
{} : Type

Rules

{ k₀ : T₀, k₁ : T₁, k₂ : T₂, … } = { k₀ : T₀ } ⩓ { k₁ : T₁ } ⩓ { k₂ : T₂ } ⩓ …

Record values

A record value is a sequence of 0 or more key-value pairs inside curly braces.

An empty record literal must have a single = sign between the curly braces to distinguish the empty record literal from the empty record type.

Examples

$ dhall --annotate <<< '{ foo = 1, bar = True }'
{ foo = 1, bar = True } : { foo : Natural, bar : Bool }
$ dhall --annotate <<< '{=}'
{=} : {}

Rules

{ k₀ = v₀, k₁ = v₁, k₂ = v₂, … } = { k₀ = v₀ } ∧ { k₁ = v₁ } ∧ { k₂ = v₂ } ∧ …

Operator:

  • ASCII: //\\
  • Unicode: U+2A53

The operator recursively merges record types

Example

$ dhall <<< '{ foo : { bar : Bool } } ⩓ { foo : { baz : Text }, qux : List Natural }'
{ foo : { bar : Bool, baz : Text }, qux : List Natural }

Rules

x ⩓ {} = x

{} ⩓ x = x

(x ⩓ y) ⩓ z = x ⩓ (y ⩓ z)

Operator:

  • ASCII: /\
  • Unicode: U+2227

The operator recursively merges record values

Example

$ dhall <<< '{ foo = { bar = True } } ∧ { foo = { baz = "ABC" }, qux = [1, 2, 3] }'
{ foo = { bar = True, baz = "ABC" }, qux = [ 1, 2, 3 ] }

Rules

x ∧ {=} = x

{=} ∧ x = x

(x ∧ y) ∧ z = x ∧ (y ∧ z)

Operator:

  • ASCII: //
  • Unicode: U+2AFD

The operator non-recursively merges record values, preferring fields from the right record when they conflict

Example

$ dhall <<< '{ foo = 1, bar = True } ⫽ { foo = 2 }'
{ foo = 2, bar = True }

Rules

x ⫽ {=} = x

{=} ⫽ x = x

(x ⫽ y) ⫽ z = x ⫽ (y ⫽ z)

Operator: ::

The :: operator auto-completes a record given a provided “schema” (a record containing the expected Type and default values):

Example

$ dhall <<EOF
let Example = { Type = { foo : Natural, bar : Bool }, default = { bar = False } }
in  Example::{ foo = 1 }
EOF
{ bar = False, foo = 1 }

Rules

T::r = (T.default ⫽ r) : T.Type