# Built-ins¶

The Agda type checker knows about, and has special treatment for, a number of
different concepts. The most prominent is natural numbers, which has a special
representation as Haskell integers and support for fast arithmetic. The surface
syntax of these concepts are not fixed, however, so in order to use the special
treatment of natural numbers (say) you define an appropriate data type and then
bind that type to the natural number concept using a `BUILTIN`

pragma.

Some built-in types support primitive functions that have no corresponding Agda
definition. These functions are declared using the `primitive`

keyword by
giving their type signature.

## Using the built-in types¶

While it is possible to define your own versions of the built-in types and bind
them using `BUILTIN`

pragmas, it is recommended to use the definitions in the
`Agda.Builtin`

modules. These modules are installed when you install Agda and
so are always available. For instance, built-in natural numbers are defined in
`Agda.Builtin.Nat`

. The standard library and the agda-prelude
reexport the definitions from these modules.

## The unit type¶

```
module Agda.Builtin.Unit
```

The unit type is bound to the built-in `UNIT`

as follows:

```
record ⊤ : Set where
{-# BUILTIN UNIT ⊤ #-}
```

Agda needs to know about the unit type since some of the primitive operations in the reflected type checking monad return values in the unit type.

## Booleans¶

```
module Agda.Builtin.Bool where
```

Built-in booleans are bound using the `BOOLEAN`

, `TRUE`

and `FALSE`

built-ins:

```
data Bool : Set where
false true : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}
```

Note that unlike for natural numbers, you need to bind the constructors separately. The reason for this is that Agda cannot tell which constructor should correspond to true and which to false, since you are free to name them whatever you like.

The only effect of binding the boolean type is that you can then use primitive
functions returning booleans, such as built-in `NATEQUALS`

.

## Natural numbers¶

```
module Agda.Builtin.Nat
```

Built-in natural numbers are bound using the `NATURAL`

built-in as follows:

```
data Nat : Set where
zero : Nat
suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}
```

The names of the data type and the constructors can be chosen freely, but the shape of the datatype needs to match the one given above (modulo the order of the constructors). Note that the constructors need not be bound explicitly.

Binding the built-in natural numbers as above has the following effects:

- The use of natural number literals is
enabled. By default the type of a natural number literal will be
`Nat`

, but it can be overloaded to include other types as well. - Closed natural numbers are represented as Haskell integers at compile-time.
- The compiler backends compile natural numbers to the appropriate number type in the target language.
- Enabled binding the built-in natural number functions described below.

### Functions on natural numbers¶

There are a number of built-in functions on natural numbers. These are special in that they have both an Agda definition and a primitive implementation. The primitive implementation is used to evaluate applications to closed terms, and the Agda definition is used otherwise. This lets you prove things about the functions while still enjoying good performance of compile-time evaluation. The built-in functions are the following:

```
_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-}
_-_ : Nat → Nat → Nat
n - zero = n
zero - suc m = zero
suc n - suc m = n - m
{-# BUILTIN NATMINUS _-_ #-}
_*_ : Nat → Nat → Nat
zero * m = zero
suc n * m = (n * m) + m
{-# BUILTIN NATTIMES _*_ #-}
_==_ : Nat → Nat → Bool
zero == zero = true
suc n == suc m = n == m
_ == _ = false
{-# BUILTIN NATEQUALS _==_ #-}
_<_ : Nat → Nat → Bool
_ < zero = false
zero < suc _ = true
suc n < suc m = n < m
{-# BUILTIN NATLESS _<_ #-}
div-helper : Nat → Nat → Nat → Nat → Nat
div-helper k m zero j = k
div-helper k m (suc n) zero = div-helper (suc k) m n m
div-helper k m (suc n) (suc j) = div-helper k m n j
{-# BUILTIN NATDIVSUCAUX div-helper #-}
mod-helper : Nat → Nat → Nat → Nat → Nat
mod-helper k m zero j = k
mod-helper k m (suc n) zero = mod-helper 0 m n m
mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
{-# BUILTIN NATMODSUCAUX mod-helper #-}
```

The Agda definitions are checked to make sure that they really define the corresponding built-in function. The definitions are not required to be exactly those given above, for instance, addition and multiplication can be defined by recursion on either argument, and you can swap the arguments to the addition in the recursive case of multiplication.

The `NATDIVSUCAUX`

and `NATMODSUCAUX`

are built-ins bind helper functions
for defining natural number division and modulo operations, and satisfy the
properties

```
div n (suc m) ≡ div-helper 0 m n m
mod n (suc m) ≡ mod-helper 0 m n m
```

## Integers¶

```
module Agda.Builtin.Int
```

Built-in integers are bound with the `INTEGER`

built-in to a data type with
two constructors: one for positive and one for negative numbers. The built-ins
for the constructors are `INTEGERPOS`

and `INTEGERNEGSUC`

.

```
data Int : Set where
pos : Nat → Int
negsuc : Nat → Int
{-# BUILTIN INTEGER Int #-}
{-# BUILTIN INTEGERPOS pos #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}
```

Here `negsuc n`

represents the integer `-n - 1`

. Unlike for natural
numbers, there is no special representation of integers at compile-time since
the overhead of using the data type compared to Haskell integers is not that
big.

Built-in integers support the following primitive operation (given a suitable binding for String):

```
primitive
primShowInteger : Int → String
```

## Floats¶

```
module Agda.Builtin.Float
```

Floating point numbers are bound with the `FLOAT`

built-in:

```
postulate Float : Set
{-# BUILTIN FLOAT Float #-}
```

This lets you use floating point literals. Floats are represented by the type checker as IEEE 754 binary64 double precision floats, with the restriction that there is exactly one NaN value. The following primitive functions are available (with suitable bindings for Nat, Bool, String and Int):

```
primitive
primNatToFloat : Nat → Float
primFloatPlus : Float → Float → Float
primFloatMinus : Float → Float → Float
primFloatTimes : Float → Float → Float
primFloatNegate : Float → Float
primFloatDiv : Float → Float → Float
primFloatEquality : Float → Float → Bool
primFloatNumericalEquality : Float → Float → Bool
primFloatNumericalLess : Float → Float → Bool
primRound : Float → Int
primFloor : Float → Int
primCeiling : Float → Int
primExp : Float → Float
primLog : Float → Float
primSin : Float → Float
primCos : Float → Float
primTan : Float → Float
primASin : Float → Float
primACos : Float → Float
primATan : Float → Float
primATan2 : Float → Float → Float
primShowFloat : Float → String
```

The `primFloatEquality`

primitive is intended to be used for decidable
propositional equality. To enable proof carrying comparisons while preserving
consisteny, the following laws apply:

`primFloatEquality NaN NaN`

returns`true`

.`primFloatEquality NaN (primFloatNegate NaN)`

returns`true`

.`primFloatEquality 0.0 -0.0`

returns`false`

.

For numerical comparisons, use the `primFloatNumericalEquality`

and
`primFloatNumericalLess`

primitives. These are implemented by the
corresponding Haskell functions with the following behaviour and
exceptions:

`primFloatNumericalEquality 0.0 -0.0`

returns`true`

.`primFloatNumericalEquality NaN NaN`

returns`false`

.`primFloatNumericalLess NaN NaN`

returns`false`

.`primFloatNumericalLess (primFloatNegate NaN) (primFloatNegate NaN)`

returns`false`

.`primFloatNumericalLess NaN (primFloatNegate NaN)`

returns`false`

.`primFloatNumericalLess (primFloatNegate NaN) NaN`

returns`false`

.`primFloatNumericalLess`

sorts`NaN`

below everything but negative infinity.`primFloatNumericalLess -0.0 0.0`

returns`false`

.

Warning

Do not use `primFloatNumericalEquality`

to establish decidable
propositional equality. Doing so makes Agda inconsistent, see
Issue #2169.

## Lists¶

```
module Agda.Builtin.List
```

Built-in lists are bound using the `LIST`

, `NIL`

and `CONS`

built-ins:

```
data List {a} (A : Set a) : Set a where
[] : List A
_∷_ : (x : A) (xs : List A) → List A
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}
infixr 5 _∷_
```

Even though Agda could easily tell which constructor is `NIL`

and which is
`CONS`

you still have to bind them separately.

As with booleans, the only effect of binding the `LIST`

built-in is to let
you use primitive functions working with lists, such as `primStringToList`

and `primStringFromList`

.

## Characters¶

```
module Agda.Builtin.Char
```

The character type is bound with the `CHARACTER`

built-in:

```
postulate Char : Set
{-# BUILTIN CHAR Char #-}
```

Binding the character type lets you use character literals. The following primitive functions are available on characters (given suitable bindings for Bool, Nat and String):

```
primitive
primIsLower : Char → Bool
primIsDigit : Char → Bool
primIsAlpha : Char → Bool
primIsSpace : Char → Bool
primIsAscii : Char → Bool
primIsLatin1 : Char → Bool
primIsPrint : Char → Bool
primIsHexDigit : Char → Bool
primToUpper : Char → Char
primToLower : Char → Char
primCharToNat : Char → Nat
primNatToChar : Nat → Char
primShowChar : Char → String
```

These functions are implemented by the corresponding Haskell functions from
Data.Char (`ord`

and `chr`

for `primCharToNat`

and
`primNatToChar`

). To make `primNatToChar`

total `chr`

is applied to the
natural number modulo `0x110000`

.

## Strings¶

```
module Agda.Builtin.String
```

The string type is bound with the `STRING`

built-in:

```
postulate String : Set
{-# BUILTIN STRING String #-}
```

Binding the string type lets you use string literals. The following primitive functions are available on strings (given suitable bindings for Bool, Char and List):

```
postulate primStringToList : String → List Char
postulate primStringFromList : List Char → String
postulate primStringAppend : String → String → String
postulate primStringEquality : String → String → Bool
postulate primShowString : String → String
```

String literals can be overloaded.

## Equality¶

```
module Agda.Builtin.Equality
```

The identity type can be bound to the built-in `EQUALITY`

as follows:

```
infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}
```

This lets you use proofs of type `lhs ≡ rhs`

in the rewrite
construction.

### primTrustMe¶

```
module Agda.Builtin.TrustMe
```

Binding the built-in equality type also enables the `primTrustMe`

primitive:

```
primitive
primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
```

As can be seen from the type, `primTrustMe`

must be used with the utmost care
to avoid inconsistencies. What makes it different from a postulate is that if
`x`

and `y`

are actually definitionally equal, `primTrustMe`

reduces to
`refl`

. One use of `primTrustMe`

is to lift the primitive boolean equality
on built-in types like String to something that returns a proof
object:

```
eqString : (a b : String) → Maybe (a ≡ b)
eqString a b = if primStringEquality a b
then just primTrustMe
else nothing
```

With this definition `eqString "foo" "foo"`

computes to `just refl`

.
Another use case is to erase computationally expensive equality proofs and
replace them by `primTrustMe`

:

```
eraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
eraseEquality _ = primTrustMe
```

## Universe levels¶

```
module Agda.Primitive
```

Universe levels are also declared using `BUILTIN`

pragmas. In contrast to the `Agda.Builtin`

modules, the `Agda.Primitive`

module
is auto-imported and thus it is not possible to change the level built-ins. For
reference these are the bindings:

```
postulate
Level : Set
lzero : Level
lsuc : Level → Level
_⊔_ : Level → Level → Level
```

```
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}
```

## Sized types¶

```
module Agda.Builtin.Size
```

The built-ins for sized types are different from other
built-ins in that the names are defined by the `BUILTIN`

pragma. Hence, to
bind the size primitives it is enough to write:

```
{-# BUILTIN SIZEUNIV SizeUniv #-} -- SizeUniv : SizeUniv
{-# BUILTIN SIZE Size #-} -- Size : SizeUniv
{-# BUILTIN SIZELT Size<_ #-} -- Size<_ : ..Size → SizeUniv
{-# BUILTIN SIZESUC ↑_ #-} -- ↑_ : Size → Size
{-# BUILTIN SIZEINF ω #-} -- ω : Size
{-# BUILTIN SIZEMAX _⊔ˢ_ #-} -- _⊔ˢ_ : Size → Size → Size
```

## Coinduction¶

```
module Agda.Builtin.Coinduction
```

The following built-ins are used for coinductive definitions:

```
postulate
∞ : ∀ {a} (A : Set a) → Set a
♯_ : ∀ {a} {A : Set a} → A → ∞ A
♭ : ∀ {a} {A : Set a} → ∞ A → A
{-# BUILTIN INFINITY ∞ #-}
{-# BUILTIN SHARP ♯_ #-}
{-# BUILTIN FLAT ♭ #-}
```

See Coinduction for more information.

## IO¶

```
module Agda.Builtin.IO
```

The sole purpose of binding the built-in `IO`

type is to let Agda check that
the `main`

function has the right type (see Compilers).

```
postulate IO : Set → Set
{-# BUILTIN IO IO #-}
```

## Literal overloading¶

```
module Agda.Builtin.FromNat
module Agda.Builtin.FromNeg
module Agda.Builtin.FromString
```

The machinery for overloading literals uses built-ins for the conversion functions.

## Reflection¶

```
module Agda.Builtin.Reflection
```

The reflection machinery has built-in types for representing Agda programs. See Reflection for a detailed description.

## Rewriting¶

The experimental and totally unsafe rewriting machinery (not
to be confused with the rewrite construct) has a built-in
`REWRITE`

for the rewriting relation:

```
postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set a
{-# BUILTIN REWRITE _↦_ #-}
```

There is no `Agda.Builtin`

module for the rewrite relation since different
rewriting experiments typically want different relations.

## Strictness¶

```
module Agda.Builtin.Strict
```

There are two primitives for controlling evaluation order:

```
primitive
primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
```

where `_≡_`

is the built-in equality. At compile-time
`primForce x f`

evaluates to `f x`

when `x`

is in weak head normal form (whnf),
i.e. one of the following:

- a constructor application
- a literal
- a lambda abstraction
- a type constructor application (data or record type)
- a function type
- a universe (
`Set _`

)

Similarly `primForceLemma x f`

, which lets you reason about programs using
`primForce`

, evaluates to `refl`

when `x`

is in whnf. At run-time,
`primForce e f`

is compiled (by the GHC and UHC backends)
to `let x = e in seq x (f x)`

.

For example, consider the following function:

```
-- pow’ n a = a 2ⁿ
pow’ : Nat → Nat → Nat
pow’ zero a = a
pow’ (suc n) a = pow’ n (a + a)
```

At compile-time this will be exponential, due to call-by-name evaluation, and
at run-time there is a space leak caused by unevaluated `a + a`

thunks. Both
problems can be fixed with `primForce`

:

```
infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = primForce x f
-- pow n a = a 2ⁿ
pow : Nat → Nat → Nat
pow zero a = a
pow (suc n) a = pow n $! a + a
```