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)