Overloaded literals

Overloaded literals#

The compiler provides directives for literals overloading, respectively %stringLit <fun> and %integerLit <fun> for string and integer literals. During elaboration, the given function is applied to the corresponding literal. In the Prelude these functions are set to fromString and fromInteger.

The interface FromString ty provides the fromString : String -> ty function, while the Num ty interface provides the fromInteger : Integer -> ty function for all numerical types.

Restricted overloads#

Although the overloading of literals can be achieved by implementing the interfaces described above, in principle only a function with the correct signature and name is enough to achieve the desired behaviour. This can be exploited to obtain more restrictive overloading such as converting literals to Fin n values, where integer literals greater or equal to n are not constructible values for the type. Additional implicit arguments can be added to the function signature, in particular auto implicit arguments for searching proofs. As an example, this is the implementation of fromInteger for Fin n.

public export
fromInteger : (x : Integer) -> {n : Nat} ->
              {auto prf : (IsJust (integerToFin x n))} ->
              Fin n
fromInteger {n} x {prf} with (integerToFin x n)
  fromInteger {n} x {prf = ItIsJust} | Just y = y

The prf auto implicit is an automatically constructed proof (if possible) that the literal is suitable for the Fin n type. The restricted behaviour can be observed in the REPL, where the failure to construct a valid proof is caught during the type-checking phase and not at runtime:

Main> the (Fin 3) 2
FS (FS FZ)
Main> the (Fin 3) 5
(interactive):1:13--1:14:Can't find an implementation for IsJust (integerToFin 5 3) at:
1   the (Fin 3) 5
Contents