Builtins

Idris2 supports an optimised runtime representation of some types, using the %builtin pragma. For now only Nat-like types has been implemented.

%builtin Natural

I suggest having a look at the source for Nat (in Prelude.Types) before reading this section.

The %builtin Natural pragma converts recursive/unary representations of natural numbers into primitive Integer representations. This massively reduces the memory usage and offers a small speed improvement, for example with the unary representation the Nat 1000 would take up about 2000 * 8 bytes (1000 for the tag, 1000 for the pointers) whereas the Integer representation takes about 8 to 16 bytes.

Here’s an example:

data Nat
    = Z
    | S Nat

%builtin Natural Nat

Note that the order of the constructors doesn’t matter. Furthermore this pragma supports GADTs so long as any extra arguments are erased.

For example:

data Fin : Nat -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

%builtin Natural Fin

works because the k is always erased.

This doesn’t work if the argument to the S-like constructor is Inf (sometime known as CoNat) as these can be infinite or is Lazy as it wouldn’t preserve laziness semantics.

During codegen any occurance of Nat will be converted to the faster Integer implementation. Here are the specifics for the conversion:

Z => 0

S k => 1 + k

case k of
    Z => zexp
    S k' => sexp

=>

case k of
    0 => zexp
    _ => let k' = k - 1 in sexp

%builtin NaturalToInteger

The %builtin NaturalToInteger pragma allows O(1) conversion of naturals to Integer s. For example

natToInteger : Nat -> Integer
natToInteger Z = 0
natToInteger (S k) = 1 + natToInteger k

%builtin NaturalToInteger natToInteger

For now, any NaturalToInteger function must have exactly 1 non-erased argument, which must be a natural.

%builtin IntegerToNatural

The %builtin IntegerToNatural pragma allows O(1) conversion of Integer s to naturals. For example

integerToNat : Integer -> Nat
integerToNat x = if x <= 0
    then Z
    else S $ integerToNat (x - 1)

Any IntegerToNatural function must have exactly 1 unrestricted Integer argument and the return type must be a natural.

Please note, NaturalToInteger and IntegerToNatural only check the type, not that the function is correct.

This can be used with %transform to allow many other operations to be O(1) too.

eqNat : Nat -> Nat -> Bool
eqNat Z Z = True
eqNat (S j) (S k) = eqNat j k
eqNat _ _ = False

%transform "eqNat" eqNat j k = natToInteger j == natToInteger k

plus : Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S $ plus x y

%transform "plus" plus j k = integerToNat (natToInteger j + natToInteger j)