Skip to content

Built in types, functions, and operators

Fabrizio Ferrai edited this page Jan 28, 2019 · 9 revisions

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

Bool

Example

$ dhall <<< 'Bool'
Type

Bool

Type

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

Literals: Bool

Example

$ dhall <<< 'True'
Bool

True

Type

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

Construct: if/then/else

Example

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

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'
Bool

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'
Bool

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'
Bool

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'
Bool

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 <<< 'Natural'
Type

Natural

Type

Natural : Type

Literals: Natural

A Natural number literal is an unsigned non-negative integer

Example

$ dhall <<< '2'
Natural

2

Type

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

Rules

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

Operator: +

Example

$ dhall <<< '2 + 3'
Natural

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'
Natural

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'
Bool

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'
Bool

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'
Bool

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/fold

Example

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

"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))'
Natural

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

Integer

Example

$ dhall <<< 'Integer'
Type

Integer

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 <<< '+3'
Integer

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

-2

Type

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

Double

Example

$ dhall <<< 'Double'
Type

Double

Type

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

Literals: Double

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

Examples

$ dhall <<< '3.14159'
Double

3.14159
$ dhall <<< '-2e10'
Double

-2.0e10

Type

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

Text

Example

$ dhall <<< 'Text'
Type

Text

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 <<< '"ABC"'
Text

"ABC"
$ dhall <<EOF
> ''
>     Line 1
>     Line 2
> ''
> EOF
Text

"Line 1\nLine 2\n"

Type

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

Rules

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

Operator: ++

Example

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

"Hello, world!"

Type

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

Rules

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

x ++ "" = x

"" ++ x = x

List

Example

$ dhall <<< 'List'
Type  Type

List

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 <<< '[ 1, 2, 3 ]'
List Natural

[ 1, 2, 3 ]
dhall <<< '[] : List Natural'
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 ]'
List Natural

[ 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'
Bool

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)))'
List Natural

[1, 2, 3] : List Natural

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 ]'
Natural

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 ]'
Optional Natural

[ 1 ] : Optional Natural

Type

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

Rules

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

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

List/head a [ x ] = [ x ] : Optional a

Function: List/last

Example

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

[ 3 ] : Optional Natural

Type

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

Rules

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

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

List/last a [ x ] = [ x ] : Optional a

Function: List/indexed

Example

$ dhall <<< 'List/indexed Text [ "ABC", "DEF", "GHI" ]'
List { index : Natural, value : Text }

[{ 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 ]'
List Natural

[ 3, 2, 1 ] : List Natural

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 (xs # ys) = List/reverse a ys # List/reverse a xs

Optional

Example

$ dhall <<< 'Optional'
Type  Type

Optional

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 <<< 'None Natural'
Optional Natural

None Natural
$ dhall <<< 'Some 1'
Optional Natural

Some 1

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) ""'
Text

"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")'
Optional Text

[ "abc" ] : Optional Text

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 <<< '{ foo : Natural, bar : Bool }'
Type

{ foo : Natural, bar : Bool }
$ dhall <<< '{}'
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 <<< '{ foo = 1, bar = True }'
{ foo : Natural, bar : Bool }

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

{=}

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 }'
Type

{ 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 : Bool, baz : Text }, qux : List Natural }

{ 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 : Natural, bar : Bool }

{ foo = 2, bar = True }

Rules

x  {=} = x

{=}  x = x

(x  y)  z = x  (y  z)
You can’t perform that action at this time.