内建（Builtins）

自然数（Natural numbers）

Idris2 支持对自然数（非负整数）进行优化的运行时表示。这种优化是自动完成的，但仅在自然数以特定方式表示时才生效。

下面是一个会被优化的自然数示例：

data Natural
    = Zero
    | Succ Natural

自然数通常表示为零或另一个自然数的后继（即加一）。这种表示方式称为 Peano 数。

在运行时，Idris2 会自动将其表示为 Integer 类型，从而大幅减少内存占用。

该优化生效时有如下规则：

数据类型必须有两个构造子
- 在擦除运行时无关参数后：+ 一个构造子不能有参数 + 另一个必须有且仅有一个参数（通常命名为 Succ）
Succ 的参数类型必须与父类型具有相同的类型构造器。这意味着像 Fin 这样的索引数据类型也可以被优化。
Succ 的参数必须是严格的，即不能是 Lazy Natural。

要确保类型被优化为 Integer，请使用 %builtin Natural，例如：

data MyNat
    = Succ MyNat
    | Zero

%builtin Natural MyNat

自然数与整数之间的类型转换（Casting between natural numbers and integer）

Idris 会优化自然数与整数之间的转换函数，使其时间复杂度为常数而非线性。

这些函数必须以特定方式编写，以便 Idris 能检测并进行优化。

下面是一个将自然数转换为 Integer 的函数示例。

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

该优化在编译过程的后期应用，因此对一些看似微小的更改也可能很敏感。

但大致有如下规则控制此优化：

必须对且仅对一个参数进行模式匹配（允许其他参数为强制或点模式）
'Zero' 分支的右侧必须为 0
'Succ' 分支的右侧必须为 1 + cast k，其中 k 是被模式匹配参数的前驱。

将 Integer 转换为自然数稍微复杂一些。

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

目前你必须手动检查给定的整数是否为非负数。

如果你使用的是索引数据类型，可能很难以这种方式编写 Integer 到自然数的转换函数，此时可以用 %builtin IntegerToNatural 向编译器断言该函数是正确的。你需要自行保证其正确性。

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）

这可以与 %transform 配合使用，使许多其他操作也能达到 O(1) 复杂度。

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）

以下是自然数如何被编译为 Integer 的细节。注意：此处的数值字面量为 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