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.