Числа Пеано на системе типов Rust

• Fedor Logachev • обучение • поддержите на Patreon

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

Таким образом моя задача: записать и сложить натуральные числа с проверкой на уровне типов.

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

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

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

1
2
3
4
enum Nat {
  Zero,
  Succ(Nat)
}

Nat — это либо ноль, либо следующее натуральное число.

Но у такой записи есть проблема — мы получили бесконечно много натуральных чисел: error: recursive type `Nat` has infinite size

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

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

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

1
2
3
4
5
6
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:

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

Nat — типаж который должен реализовать любой тип, являющийся частью натуральных чисел, то есть Zero и Succ. Функция new — позволяет спустить значение с уровня типов на уровень данных, создав конкретный экземпляр. Реализуем его для Zero и Succ:

1
2
3
4
5
6
7
8
9
10
11
12
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

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

Наше следующая цель — получить число 4 из числа 3!

Введём типаж Incr:

1
trait Incr : Nat { type Result; }

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

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

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

Теперь можно написать функцию, которая принимает что-нибудь с типом Incr (который реализован для всех натуральных чисел) и возвращает то, что написано в реализации типажа Incr. Это дословно и запишем:

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

Теперь мы можем получить 4!

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

И можем, например, написать функцию по работе с числами и быть уверенным, что она не сделает ничего кроме инкремента:

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

Полезно!

Теперь попробуем сложить числа: Согласно аксиоматике Пеано сложение можно записать вот так:

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

Попробуем записать это в терминах Rust:

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

Введём типаж Sum. Появился ещё один вид синтаксиса — типаж, параметризированный типом. В данном случае Sum<B> — это всё, что может быть сложено с B.

Реализуем сложение нуля:

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

и сложение не нуля:

1
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 напишем удобную функцию:

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

Теперь мы можем складывать числа!

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

Но этого явно не достаточно. Хочется, например, вывести результат на экран. Самый простой вариант — написать так:

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

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

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

Но хочется вывести наше число более честным способом.

Воспользуемся типажом Display.

Начнём с Zero:

1
2
3
4
5
6
7
use std::fmt::{Display, Result, Formatter};

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

Ноль просто вывести.

Теперь немного рекурсии:

1
2
3
4
5
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:

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

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

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

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

patreon Поддержите на Patreon