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

{-# 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
    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 Fin n can then be defined as follows:

data IsTrue : Bool  Set where
  itis : IsTrue true

  indeed : IsTrue true
  indeed = itis

_<?_ : Nat  Nat  Bool
zero <? zero = false
zero <? suc y = true
suc x <? zero = false
suc x <? suc y = x <? y

natToFin :  {n} (m : Nat) {{_ : IsTrue (m <? n)}}  Fin n
natToFin {zero} zero {{()}}
natToFin {zero} (suc m) {{()}}
natToFin {suc n} zero {{itis}} = zero
natToFin {suc n} (suc m) {{t}} = suc (natToFin m)

  NumFin :  {n}  Number (Fin n)
  Number.Constraint (NumFin {n}) k = IsTrue (k <? n)
  Number.fromNat    NumFin       k = natToFin k

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
    Constraint : Nat  Set a
    fromNeg : (n : Nat) {{_ : Constraint n}}  A

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


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
    Constraint : String  Set a
    fromString : (s : String) {{_ : Constraint s}}  A

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

Other types

Currently only integer and string literals can be overloaded.