Реализация арифметики натуральных чисел с помощью чисел Пеано — популярная задача в обучение программированию. Мне было интересно, можно ли реализовать их на Rust. Таким образом моя задача: записать и сложить натуральные числа с проверкой на уровне типов.

Если верить википедии "Аксио?мы Пеа?но — одна из систем аксиом для натуральных чисел, введённая в XIX веке итальянским математиком Джузеппе Пеано."

Нас интересуют две из них — с помощью которых можно ввести и использовать натуральные числа:

• 1 является натуральным числом
• Число, следующее за натуральным, тоже является натуральным.

Дословно запишем на расте с помощью:

enum Nat { 
  Zero,
  Succ(Nat)
}

Nat — это либо ноль, либо следующее натуральное число. Но у такой записи есть проблема — мы получили бесконечно много натуральных чисел:

error: recursive type `Nat` has infinite size

Очевидным решением было бы вместо Succ(Nat) хранить какой-нибудь указатель на следующее натуральное число.
Но тогда на уровне типов будет всего два значения — Zero и Box<Succ>. Не годится: нет информации о числах на уровне типов — 5 и 7 имеют один тип.

Запустить код на play.rust-lang.org

Запишем те же числа немного подругому:

use std::marker::PhantomData;

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

Zero — это тип данных с одним возможным значением — Zero. Succ — это тип данных также с одним значением — Succ, но с полезной нагрузкой в виде типа данных. Может быть тип Succ<i32>, Succ<String>, Succ<Succ<_>> и т.д.

Теперь у нас есть отдельно ноль и отдельно следующее число. Теперь тип Succ<Succ<Succ<Succ<Zero>>>> — валиден. Но есть проблема — Zero не связан c 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
        }
    }
}

Теперь мы уже можем создать натуральное число!

Запустить код на play.rust-lang.org

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

Наше следующая цель — получить число 4 из числа 3! Введём типаж Incr:

trait Incr : Nat { type Result; }

От нашего прошлого типажа Nat он отличается тем, что содержит не только функции, но и тип. Инкремент типа T на 1 согласно нашим правилам натуральных чисел — это Succ. Что мы и запишем:

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

Таким образом мы реализовали типаж Incr для всех типов T с реализованным Nat.

Теперь можно написать функцию, которая принимает что-нибудь с типом 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> — это всё, что может быть сложено с 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)

Компилятор сообщит об ошибке и красиво покажет нужный нам тип в поле "ожидаемый":

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

Но хочется вывести наше число более честным способом. Воспользуемся типажом Display.

Начнём с Zero:

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())
    }
}

Запустить код на play.rust-lang.org

Теперь можно напечатать нашу 6:

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

У нас всё получилось! Оставлю читателю ввести умножение:

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

Вот так с помощью мономорфизации растовых типажей можно во время компиляции складывать числа. Я не уверен что представленное решение является правильным или идиоматичным, но оно показалось мне любопытным.