Natural numbers¶

By default natural number literals are mapped to the built-in natural number type. This can be changed with the FROMNAT built-in, which binds to a function accepting a natural number:

{-# BUILTIN FROMNAT fromNat #-}

This causes natural number literals n to be desugared to fromNat n, whenever fromNat is in scope unqualified (renamed or not). Note that the desugaring happens before implicit argument are inserted so fromNat can have any number of implicit or instance arguments. This can be exploited to support overloaded literals by defining a type class containing fromNat:

module number-simple where

record Number {a} (A : Set a) : Set a where
field fromNat : Nat  A

open Number {{...}} public
{-# BUILTIN FROMNAT fromNat #-}

This definition requires that any natural number can be mapped into the given type, so it won’t work for types like Fin n. This can be solved by refining the Number class with an additional constraint:

record Number {a} (A : Set a) : Set (lsuc a) where
field
Constraint : Nat  Set a
fromNat : (n : Nat) {{_ : Constraint n}}  A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

This is the definition used in Agda.Builtin.FromNat. A Number instance for Nat is simply this:

instance
NumNat : Number Nat
NumNat .Number.Constraint _ = ⊤
NumNat .Number.fromNat    m = m

A Number instance for Fin n can be defined as follows:

_≤_ : (m n : Nat)  Set
zero  ≤ n     = ⊤
suc m ≤ zero  = ⊥
suc m ≤ suc n = m ≤ n

fromN≤ :  m n  m ≤ n  Fin (suc n)
fromN≤ zero    _       _  = zero
fromN≤ (suc _) zero    ()
fromN≤ (suc m) (suc n) p  = suc (fromN≤ m n p)

instance
NumFin :  {n}  Number (Fin (suc n))
NumFin {n} .Number.Constraint m         = m ≤ n
NumFin {n} .Number.fromNat    m {{m≤n}} = fromN≤ m n m≤n

test : Fin 5
test = 3

It is important that the constraint for literals is trivial. Here, 3 5 evaluates to whose inhabitant is found by unification.

Using predefined function from the standard library and instance NumNat, the NumFin instance can be simply:

open import Data.Fin using (Fin; #_)
open import Data.Nat using (suc; _≤?_)
open import Relation.Nullary.Decidable using (True)

instance
NumFin :  {n}  Number (Fin n)
NumFin {n} .Number.Constraint m         = True (suc m ≤? n)
NumFin {n} .Number.fromNat    m {{m<n}} = #_ m {m<n = m<n}

Negative numbers¶

Negative integer literals have no default mapping and can only be used through the FROMNEG built-in. Binding this to a function fromNeg causes negative integer literals -n to be desugared to fromNeg n, where n is a built-in natural number. From Agda.Builtin.FromNeg:

record Negative {a} (A : Set a) : Set (lsuc a) where
field
Constraint : Nat  Set a
fromNeg : (n : Nat) {{_ : Constraint n}}  A

open Negative {{...}} public using (fromNeg)
{-# BUILTIN FROMNEG fromNeg #-}

Strings¶

String literals are overloaded with the FROMSTRING built-in, which works just like FROMNAT. If it is not bound string literals map to built-in strings. From Agda.Builtin.FromString:

record IsString {a} (A : Set a) : Set (lsuc a) where
field
Constraint : String  Set a
fromString : (s : String) {{_ : Constraint s}}  A

open IsString {{...}} public using (fromString)
{-# BUILTIN FROMSTRING fromString #-}

Restrictions¶

Currently only integer and string literals can be overloaded.