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 ⊤ : Type 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.

The Σ-type 

module Agda.Builtin.Sigma

The built-in Σ-type of dependent pairs is defined as follows:

record Σ {a b} (A : Type a) (B : A → Type b) : Type (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

{-# BUILTIN SIGMA Σ #-}

Lists 

module Agda.Builtin.List

Built-in lists are bound using the LIST built-in:

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

The constructors are bound automatically when binding the type. Lists are not required to be level polymorphic; List : Type → Type is also accepted.

As with booleans, the effect of binding the LIST built-in is to let you use primitive functions working with lists, such as primStringToList and primStringFromList, and letting the GHC backend know to compile the List type to Haskell lists.

Maybe 

module Agda.Builtin.Maybe

Built-in maybe type is bound using the MAYBE built-in:

data Maybe {a} (A : Type a) : Type a where
  nothing : Maybe A
  just    : A → Maybe A
{-# BUILTIN MAYBE Maybe #-}

The constructors are bound automatically when binding the type. Maybe is not required to be level polymorphic; Maybe : Type → Type is also accepted.

As with list, the effect of binding the MAYBE built-in is to let you use primitive functions working with maybes, such as primStringUncons that returns the head and tail of a string (if it is non empty), and letting the GHC backend know to compile the Maybe type to Haskell maybes.

Booleans 

module Agda.Builtin.Bool where

Built-in booleans are bound using the BOOL, TRUE and FALSE built-ins:

data Bool : Type 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 effect of binding the boolean type is that you can then use primitive functions returning booleans, such as built-in NATEQUALS, and letting the GHC backend know to compile the type to Haskell Bool.

Natural numbers 

module Agda.Builtin.Nat

Built-in natural numbers are bound using the NATURAL built-in as follows:

data Nat : Type 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 _*_ #-}

infixl 30 _*_
infixl 20 _+_

_==_ : 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 : Type 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
module Agda.Builtin.Float.Properties

Floating point numbers are bound with the FLOAT built-in:

postulate Float : Type
{-# 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, Int, Maybe_):

primitive
  -- Relations
  primFloatIsInfinite        : Float → Bool
  primFloatIsNaN             : Float → Bool
  primFloatIsNegativeZero    : Float → Bool

  -- Conversions
  primNatToFloat             : Nat → Float
  primIntToFloat             : Int → Float
  primFloatToRatio           : Float → (Σ Int λ _ → Int)
  primRatioToFloat           : Int → Int → Float
  primShowFloat              : Float → String

  -- Operations
  primFloatPlus              : Float → Float → Float
  primFloatMinus             : Float → Float → Float
  primFloatTimes             : Float → Float → Float
  primFloatDiv               : Float → Float → Float
  primFloatPow               : Float → Float → Float
  primFloatNegate            : Float → Float
  primFloatSqrt              : Float → Float
  primFloatExp               : Float → Float
  primFloatLog               : Float → Float
  primFloatSin               : Float → Float
  primFloatCos               : Float → Float
  primFloatTan               : Float → Float
  primFloatASin              : Float → Float
  primFloatACos              : Float → Float
  primFloatATan              : Float → Float
  primFloatATan2             : Float → Float → Float
  primFloatSinh              : Float → Float
  primFloatCosh              : Float → Float
  primFloatTanh              : Float → Float
  primFloatASinh             : Float → Float
  primFloatACosh             : Float → Float
  primFloatATanh             : Float → Float

The primitive binary relations implement their IEEE 754 equivalents, which means that primFloatEquality is not reflexive, and primFloatInequality and primFloatLess are not total. (Specifically, NaN is not related to anything, including itself.)

The primFloatIsSafeInteger function determines whether the value is a number that is a safe integer, i.e., is within the range where the arithmetic operations do not lose precision.

in the Properties module. These primitives can be used to define a safe decidable propositional equality with the --safe option.

The rounding operations (primFloatRound, primFloatFloor, and primFloatCeiling) return a value of type Maybe Int, and return nothing when applied to NaN or the infinities:

primitive
  primFloatRound             : Float → Maybe Int
  primFloatFloor             : Float → Maybe Int
  primFloatCeiling           : Float → Maybe Int

The primFloatDecode function decodes a floating-point number to its mantissa and exponent, normalised such that the mantissa is the smallest possible integer. It fails when applied to NaN or the infinities, returning nothing. The primFloatEncode function encodes a pair of a mantissa and exponent to a floating-point number. It fails when the resulting number cannot be represented as a float. Note that primFloatEncode may result in a loss of precision.

primitive
primFloatDecode : Float → Maybe (Σ Int λ _ → Int) primFloatEncode : Int → Int → Maybe Float

Characters 

module Agda.Builtin.Char
module Agda.Builtin.Char.Properties

The character type is bound with the CHARACTER built-in:

postulate Char : Type
{-# 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. Furthermore, to match the behaviour of strings, surrogate code points are mapped to the replacement character U+FFFD.

Converting to a natural number is the obvious embedding, and its proof:

primitive
  primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b

can be found in the Properties module.

Strings 

module Agda.Builtin.String
module Agda.Builtin.String.Properties

The string type is bound with the STRING built-in:

postulate String : Type
{-# 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):

primitive
  primStringUncons   : String → Maybe (Σ Char (λ _ → String))
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primShowString     : String → String

String literals can be overloaded.

Converting to and from a list is injective, and their proofs:

primitive
  primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b
  primStringFromListInjective : ∀ a b → primStringFromList a ≡ primStringFromList b → a ≡ b

can found in the Properties module.

Strings cannot represent unicode surrogate code points (characters in the range U+D800 to U+DFFF). These are replaced by the unicode replacement character U+FFFD if they appear in string literals.

Equality 

module Agda.Builtin.Equality

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

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

This lets you use proofs of type lhs ≡ rhs in the rewrite construction.

Other variants of the identity type are also accepted as built-in:

data _≡_ {A : Type} : (x y : A) → Type where
  refl : (x : A) → x ≡ x

Sorts 

The primitive sorts used in Agda’s type system are declared using BUILTIN pragmas in the Agda.Primitive module. These pragmas should not be used directly in other modules, but it is possible to rename these builtin sorts when importing Agda.Primitive.

{-# BUILTIN PROP           Prop      #-}
{-# BUILTIN TYPE           Type      #-}
{-# BUILTIN STRICTSET      SSet      #-}

{-# BUILTIN PROPOMEGA      Propω     #-}
{-# BUILTIN TYPEOMEGA      Typeω     #-}
{-# BUILTIN STRICTSETOMEGA SSetω     #-}

{-# BUILTIN LEVELUNIV      LevelUniv #-}

The primitive sort Type is automatically imported at the top of every top-level Agda module, unless the --no-import-sorts flag is enabled.

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 : LevelUniv
  lzero : Level
  lsuc  : Level → Level
  _⊔_   : Level → Level → Level

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

Note that if the flag --level-universe is not set, then LevelUniv will be Type.

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.

Strictness 

module Agda.Builtin.Strict

There are two primitives for controlling evaluation order:

primitive
  primForce      : ∀ {a b} {A : Type a} {B : A → Type b} (x : A) → (∀ x → B x) → B x
  primForceLemma : ∀ {a b} {A : Type a} {B : A → Type 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 (Type _)

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 backend) 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)

There is a space leak here (both for compile-time and run-time evaluation), caused by unevaluated a + a thunks. This problem can be fixed with primForce:

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Type a} {B : A → Type 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