みなさん、自然数というと、何を思い浮かべますか?
まずは、ゼロですよね。(本記事では自然数はゼロを含むものとします。異論は認めません)

他にどんな自然数があるのか、よく分からないんですが、ゼロの次にくる自然数があるような気がします。その次にくる自然数もあるような気がします。
もっと言うと、どんな自然数に対しても、それの次の自然数があるような気がします。

これを、Rustのenum型で表すと次のようになります。

#![allow(dead_code)]
use std::rc::Rc;

#[derive(Clone, Debug)]
enum Nat {
    O,
    S(Rc<Nat>),
}

ここで、ゼロをO, なにかの次の自然数をSで表しました。

つまり、

アラビア数字	Nat
0	`Nat::O`
1	`Nat::S(Rc::new(Nat::O))`
2	`Nat::S(Rc::new(Nat::S(Rc::new(Nat::O))))`
...	...

と表せています。

Nat::S(Rc::new(...)) はめんどくさいので、succというメソッドを生やしましょう。

impl Nat {
    fn succ(n: Nat) -> Nat {
        Nat::S(Rc::new(n))
    }
}

アラビア数字	Nat
0	`Nat::O`
1	`Nat::succ(Nat::O)`
2	`Nat::succ(Nat::succ(Nat::O))`
...	...

と書けるようになりました。Nat::も外せるようにimplの外に書きたい、とか、いろいろ思うところはあるかもしれませんが。とりあえずこれでいきましょう。

さらに、succをいっぱい書くのもめんどくさいので、もっとメソッドを生やしてみましょう。

impl Nat {
    fn from_u32(n: u32) -> Nat {
        if n == 0 {
            Nat::O
        } else {
            Nat::succ(Nat::from_u32(n - 1))
        }
    }
}

再帰的にsuccをする関数です。

我々はu32型には詳しいので、u32型でこうやれば再帰ができることを知っていて、こういうコードが書けました。
Natでも再帰ができる気がするので、ちょっと考えてみます。

u32での再帰と同様、Natでも、再帰をどこかで止めたいです。具体的にはNat::Oのとき、何かを返すようにしたいです
Nat::Oじゃないとき、先ほどのelse節Nat::succ(Nat::from_u32(n - 1))のような雰囲気の形にしたいです
n - 1 ←こんな計算しらない。けど、Natでは、Nat::S(m)のmの部分を使えばよさそうです。

これらを考えたとき、例えば次のような実装ができます。

impl Nat {
    fn rec<T>(c0: T, cs: &dyn Fn(&Nat, T) -> T, n: &Nat) -> T {
        match n {
            Nat::O => c0,
            Nat::S(m) => cs(m, Nat::rec(c0, &cs, m)),
        }
    }
}

これで、再帰ができるようになりました。
再帰によって、Natをu32に戻すには、次のようにすればいいですね。

impl Nat {
    fn to_u32(&self) -> u32 {
        Nat::rec(0, &|_, cnt: u32| cnt + 1, self)
    }
}

以下を動かすと、動作が確認できます。

fn main() {
    println!("Except: 100, Actual: {}", Nat::to_u32(&Nat::from_u32(100)));
}

最後に、足し算を定義してみます。

use std::ops::Add;

impl Add for Nat {
    type Output = Self;
    fn add(self, other: Self) -> Self {
        Self::rec(other.clone(), &|_, n: Nat| Nat::succ(n), &self)
    }
}

これは、u32での再帰風に書くと

fn add(this: u32, other: u32) -> u32 {
    if this == 0 {
        other
    } else {
        1 + add(this - 1, other)
    }
}

です。とても愚直ですが、確かに、足し算になっていることが分かります。
以下のコードで動作確認してみましょう。

fn main() {
    println!("Except: 7, Actual: {}",
             Nat::to_u32(&(Nat::from_u32(3) + Nat::from_u32(4))));
    println!("Except: 100, Actual: {}",
             Nat::to_u32(&(Nat::from_u32(43) + Nat::from_u32(57))));
}

続く……のか?

続けたいのですが、Rustだと、高階関数を作ろうと思うと、関数自体の置き場所、クロージャに渡すものの所有権やライフタイムなどが問題になってきて、非常につらいです。

余力のある方は、例えば、recの定義に適当に参照をつけたりとったり、あるいはrecの定義をCurry化してもコンパイルが通るかどうか、試してみて下さい。非常に苦労されると思います。

そのため「進捗が出たら続きを書く」という方式を取ります。

参考文献

HoTT bookの最初の方