🤳🏿 💞 👨🏼‍🏭 Rustに数字を追加する 🎌 👰🏿 💟

ペアノ数を使用して自然数の算術を実装することは、プログラミングを教える際の一般的なタスクです。 Rustでそれらを実装することが可能かどうか疑問に思っていました。したがって、私のタスクは、型レベルのチェックを使用して自然数を記述および追加することです。

ウィキペディア「Paenoの公理-イタリアの数学者ジュゼッペペアノによってXIX世紀に導入された自然数の公理のシステムの1つ」を信じている場合。

そのうちの2つに興味があります。その助けを借りて、自然数を入力して使用できます。

次のように、ラストに逐語的に書きます。

enum Nat { Zero, Succ(Nat) }

Natは、ゼロまたは次の正の整数です。しかし、そのような記録には問題があります-私たちは無限に多くの自然数を得ました：

error: recursive type `Nat` has infinite size

明らかな解決策は、 Succ(Nat)

代わりに次の自然数へのポインタを格納することです。

ただし、タイプレベルでは、 Zero

とBox<Succ>

2つの値しかありません。良くありません：型のレベルで数値に関する情報はありません-5と7は同じ型です。

私たちは小さな友人に同じ数字を書きます：

 use std::marker::PhantomData; struct Zero; struct Succ<T> { _marker : PhantomData<T> }

ゼロは、1つの可能な値を持つデータ型です-ゼロ。 Succも1つの値を持つデータ型です-Succですが、データ型としてペイロードがあります。タイプはSucc<i32>

、 Succ<String>

、 Succ<Succ<_>>

などです。

これで、ゼロと次の数値が別々になりました。タイプSucc<Succ<Succ<Succ<Zero>>>>

が有効になりました。しかし、問題があります-ゼロはSuccに関連付けられていません。解決策は、Nat特性を導入することです。

 trait Nat { fn new() -> Self; }

Nat

は、自然数の一部である任意の型、つまりZeroおよびSuccを実装する必要がある型です。

関数new-値をタイプレベルからデータレベルに下げて、特定のインスタンスを作成できます。

ZeroおよびSuccに実装します。

 impl Nat for Zero { fn new() -> Self { Zero } } impl<T : Nat> Nat for Succ<T> { fn new() -> Self { Succ { _marker : PhantomData } } }

これで自然数を作成できます！

 let two : Succ<Succ<Zero>> = Nat::new(); let three : Succ<Succ<Succ<Zero>>> = Nat::new();

次の目標は、3番から4番を取得することです！ Incr特性を紹介します。

 trait Incr : Nat { type Result; }

関数だけでなく型も含むという点で、これまでのNatの特徴とは異なります。自然数の規則に従って、タイプTを1増やすことはSuccです。書き留める内容：

 impl<T : Nat> Incr for T { type Result = Succ<T>; }

したがって、Natを実装して、すべてのタイプTにIncrトレイトを実装しました。

これで、Incr型（すべての自然数に対して実装されます）で何かを受け入れ、Incr型実装で記述されたものを返す関数を作成できます。これは逐語的で、次のように記述します。

 fn incr<T : Incr, Res : Nat>(_ : T) -> Res where T : Incr<Result = Res> { Res::new() }

これで4を取得できます！

 let three : Succ<Succ<Succ<Zero>>> = Nat::new(); let four = incr(three);

そして、例えば、数字を扱うための関数を書いて、それがインクリメント以外の何もしないことを確認することができます：

 fn next<In : Nat, Out : Nat>(x : In) -> Out where In : Incr<Result = Out> { incr(x) }

役に立つ！数字を追加してみましょう。ペアノの公理によると、追加は次のように書くことができます。

 x + 0 = x x + Succ(y) = Succ(x + y)

これをラスタの観点から書きましょう。

 trait Sum<B> : Nat { type Result; }

タイプSumを紹介します。別の種類の構文が登場しました-型によってパラメーター化された型。この場合、 Sum<B>

とスタックできるのはSum<B>

です。

ゼロの追加を実装します。

 impl<A : Nat> Sum<A> for Zero { type Result = A; }

そして、加算はゼロではありません：

 impl<A : Nat, B : Nat, Res> Sum<A> for Succ<B> where B : Sum<A, Result = Res> { type Result = Succ<Res>; }

よく見ると、これはx + Succ(y) = Succ(x + y)

であることがわかります。

incrとの類推により、便利な関数を記述します。

 fn sum<A : Sum<B>, B : Nat, Res : Nat>(_ : A, _ : B) -> Res where A : Sum<B, Result = Res> { Res::new() }

これで数字を追加できます！

 let two : Succ<Succ<Zero>> = Nat::new(); let three : Succ<Succ<Succ<Zero>>> = Nat::new(); let four = incr(three); let six = sum(two, four);

しかし、これは明らかに十分ではありません。たとえば、結果を画面に表示したいです。最も簡単なオプションは、次のように記述することです。

 let six : () = sum(two, four)

コンパイラはエラーを報告し、「expected」フィールドに必要なタイプを美しく表示します。

 note: expected type `Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>` note: found type `()`

しかし、もっと正直な方法で数字を推測したい。表示タイプを使用します。

ゼロから始めましょう：

 use std::fmt::{Display, Result, Formatter}; impl Display for Zero { fn fmt(&self, f: &mut Formatter) -> Result { write!(f, "Zero") } }

ゼロは簡単に推測できます。

今少し再帰：

 impl<T : Nat + Display> Display for Succ<T> { fn fmt(&self, f: &mut Formatter) -> Result { write!(f, "(Succ {})", T::new()) } }

これで、6を印刷できます。

 (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))

全部やりました！乗算器を紹介するために読者に任せます。

 x * Zero = Zero x * Succ(y) = x * y + x

したがって、ラスタータイプの単相化の助けを借りて、コンパイル中に数値を追加できます。提示された解決策が正しいか慣用かはわかりませんが、私には興味がありました。

Rustに数字を追加する