Builtins

Natural numbers

Idris2 supports an optimized runtime representation of natural numbers (non-negative integers). This optimization is automatic, however it only works when natural numbers are represented in a specific way

Here is an example of a natural number that would be optimized:

data Natural
    = Zero
    | Succ Natural

Natural numbers are generally represented as either zero or the successor (1 more than) of another natural number. These are called Peano numbers.

At runtime, Idris2 will automatically represent this the same as the Integer type. This will massively reduce the memory usage.

There are a few rules governing when this optimization occurs:

The data type must have 2 constructors
- After erasure of runtime irrelevant arguments + One must have no arguments + One must have exactly 1 argument (called Succ)
The type of the argument to Succ must have the same type constructor as the parent type. This means indexed data types, like Fin, can be optimised.
The argument to Succ must be strict, ie not Lazy Natural

To ensure that a type is optimized to an Integer, use %builtin Natural ie

data MyNat
    = Succ MyNat
    | Zero

%builtin Natural MyNat

Casting between natural numbers and integer

Idris optimizes functions which convert between natural numbers and integers, so that it takes constant time rather than linear time.

Such functions must be written in a specific way, so that idris can detect that it can be optimised.

Here is an example of a natural to Integer function.

cast : Natural -> Integer
cast Z = 0
cast (S k) = cast k + 1

This optimization is applied late in the compilation process, so it may be sensitive to seemingly insignificant changes.

However here are roughly the rules governing this optimisation:

Exactly one argument must be pattern matched on (any other forced or dotted patterns are allowed)
The right hand side of the ‘Zero’ case must be 0
The right hand side of the ‘Succ’ case must be 1 + cast k where k is the predecessor of the pattern matched argument

Casting from an Integer to a natural is a little more complex.

castNonNegative : Integer -> Natural
castNonNegative x = case x of
    0 => Zero
    _ => Succ $ castNonNegative (x - 1)

cast : Integer -> Natural
cast x = if x < 0 then Zero else castNonNegative x

For now you must manually check the given integer is non-negative.

If you are using an indexed data type it may be very hard to write your Integer to natural cast in such a way, so you can use %builtin IntegerToNatural to assert to the compiler that a function is correct. It is your responsibility to make sure this is correct.

module ComplexNat

import Data.Maybe

data ComplexNat
    = Zero
    | Succ ComplexNat

integerToMaybeNat : Integer -> Maybe ComplexNat
integerToMaybeNat _ = ...

integerToNat :
    (x : Integer) ->
    {auto 0 prf : IsJust (ComplexNat.integerToMaybeNat x)} ->
    ComplexNat
integerToNat x {prf} = fromJust (integerToMaybeNat x) @{prf}

%builtin IntegerToNatural ComplexNat.integerToNat

Other operations

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)

Compilation

Here are the details of how natural numbers are compiled to Integer s. Note: a numeric literal here is an Integer.

Zero => 0

Succ k => 1 + k

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

=>

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