# Literal Overloading

## 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.

Overloading does not work in patterns yet.