Складываем числа на Rust21.09.2016 10:33

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

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

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

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

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

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

enum Nat { 
  Zero,
  Succ(Nat)
}

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

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

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

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

use std::marker::PhantomData;

struct Zero;
struct Succ {
    _marker : PhantomData
}

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

Теперь у нас есть отдельно ноль и отдельно следующее число. Теперь тип Succ>>> — валиден.
Но есть проблема — Zero не связан c Succ.
Решение — введём типаж Nat:

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

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

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

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

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

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

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

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

trait Incr : Nat { type Result; }

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

impl Incr for T { type Result = Succ; }

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

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

fn incr(_ : T) -> Res where T : Incr {
    Res::new()
}

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

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

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

fn next(x : In) -> Out where In : Incr {
    incr(x)
}

Полезно!

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

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

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

trait Sum : Nat { type Result; }

impl Sum for Zero  { type Result = A; }

impl Sum for Succ where B : Sum { type Result = Succ; }

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

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

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

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

use std::fmt::{Display, Result, Formatter};

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

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

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

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