# Built in types, functions, and operators

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

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)```
##### Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.