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
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 Fin n
can then be defined as follows:
data IsTrue : Bool → Set where
itis : IsTrue true
instance
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)
instance
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
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 #-}
Other types¶
Currently only integer and string literals can be overloaded.