Арифметика первого класса в системе типов Rust

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

▍ Математика

Начнём с кодирования Чёрча. В основе функционального программирования лежит идея о том, что функции – это хорошо, и специалисты по теории типов развили эту идею настолько, что порой определяют числа как функции, которые выглядят так:

0 = |f, x| x # f, применённая 0 раз
1 = |f, x| f(x) # f, применённая 1 раз
2 = |f, x| f(f(x)) # f, применённая 2 раза
3 = |f, x| f(f(f(x))) # f, применённая 3 раза
... # f, применённая ... раз
n = |f, x| f( .. n - 2 more f's .. f(x)) # f, применённая n раз

n-ное натуральное число буквально определяется как функция, которая получает значение и функцию, применяя эту функцию n раз.

В математике есть ещё один принцип, называемый аксиомы Пеано. Они представляют очень эффективный способ описания натуральных чисел, по сути, следующим образом (некоторые детали опущены):

0. 0 – это натуральное число.
1. Число, следующее за натуральным числом, <code>S(n)</code>, также является натуральным.

Из этого следует, что натуральные числа определяются как:

0 = 0
1 = S(0)
2 = S(1) = S(S(0))
3.= S(2) = S(S(S(0)))
...
n = S( .. n - 2 дополнительных S .. S(0))

Где S называется функцией следования. Но нас не интересует, что она конкретно из себя представляет, так как мы будем рассматривать всё более абстрактно.

Заметили сходства с кодированием Чёрча?

Основная идея в том, что мы можем представить число как повторяющееся применение функции.

▍ Подключаем Rust

Как же реализовать всё это в Rust, ещё и производительно? Можно просто использовать стандартные лямбды, но такой подход окажется медленным. Основная причина в том, что замыкания размещаются в куче (boxed clojure), но есть и другие.

Наша конечная цель – выступить в роли бога и при компиляции вычислять только числа. В конце концов, это путь Rust. Но как мы будем вызывать функции во время компиляции? Для этого можно позаимствовать ещё одну идею из теории типов и обратить внимание на то, что обобщённая структура подобна функции.

Взгляните сюда: struct Wrapper<T>(PhantomData<T>). Инстанцирование T аналогично вычислению функции для типов, начиная с типа T и заканчивая типом Wrapper<T>. При этом теоретически можно построить тип Wrapper <Wrapper<Wrapper<T>>>...

Здесь мы сталкиваемся с повторением. Определим следующие типы:

struct Zero;
struct Succ<T>(PhantomData<T>);

Да, я знаю, что слово Succ звучит смешно (подразумевается созвучие с англ. suck – сосать, — прим. пер.) но это просто условное сокращение для Successor. Теперь мы можем определить натуральные числа:

type One = Succ<Zero>;
type Two = Succ<Succ<Zero>>;
type Three = Succ<Succ<Succ<Zero>>>;
...

Это будет утомительный процесс, поэтому давайте напишем небольшой вспомогательный макрос:

#[macro_export]
macro_rules! encode {
() => {
Zero
};
($_a:tt $($tail:tt)*) => {
Succ<encode!($($tail)*)>
};
}

По сути, мы передаём в этот механизм токены, и он обрабатывает их по одному, каждый раз добавляя к создаваемому им типу новый слой Succ. Вот пример:

 encode!(* ***)
^ these tokens correspond to $tail
= Succ<encode!(* **)>
= Succ<Succ<encode!(* *)>>
= Succ<Succ<Succ<encode!(*)>>>
= Succ<Succ<Succ<Succ<encode!()>>>>
^ input is empty, so encode!() expands to Zero
= Succ<Succ<Succ<Succ<Zero>>>>

Теперь мы можем создавать очень крупные числа, используя encode!(***** ... *****), хотя компилятор вследствие рекурсии будет переполнять стек примерно при 3200 токенах.

▍ Вычисление

Напомню, что наша задача – использовать эти числа для арифметики, поэтому нам нужна возможность в определённый момент извлекать их из закодированной формы. Надеюсь, нам удастся все вычисления проделывать во время компиляции (мгновенно?), а затем извлекать числа в виде констант в итоговый двоичный файл. Выходит, нам нужна функция для получения значений из типов? Хмм… если посмотреть внимательно, то такими функциями являются трейты.

trait SpecialNumber {
const MAGIC: usize;
}

impl SpecialNumber for Foo {
const MAGIC: usize = 13;
}

impl SpecialNumber for Bar {
const MAGIC: usize = 29;
}

По сути, мы отобразили тип Foo в 13, а тип Bar – в 29. Следуя тому же принципу, определим трейт Value:

trait Value {
const VALUE: usize;
}

impl Value for Zero {
const VALUE: usize = 0;
}

impl<T> Value for Succ<T> where T: Value {
const VALUE: usize = 1 + T::VALUE;
}

Теперь мы можем рекурсивно «вычислять» тип – то есть определять, сколько раз был применён Succ, поскольку второй кейс с каждой итерацией снимает по одному слою Succ.

▍ Сложение и вычитание

Хорошо. Мы подошли к более интересному приёму, хотя основная идея остаётся прежней. Мы будем использовать эту странную рекурсию типов для построения новых типов. Вместо использования трейтов для отображения типов в значения мы можем также использовать их для отображения типов в другие типы, задействуя связанные с ними константы. Давайте определим трейт Add таким образом:

trait Add {
type Sum;
}

Далее пропишем для нашей рекурсии несколько базовых кейсов:

impl Add for (Zero, Zero) { // 0 + 0 = 0
type Sum = Zero;
}

impl<T> Add for (Succ<T>, Zero) { // x + 0 = x
type Sum = Succ<T>;
}

impl<T> Add for (Zero, Succ<T>) { // 0 + x = x
type Sum = Succ<T>;
}

А теперь для нашего рекурсивного правила:

impl<T, U> Add for (Succ<T>, Succ<U>)
where
(T, Succ<Succ<U>>): Add,
{
type Sum = <(T, Succ<Succ<U>>) as Add>::Sum;
}

Разберём этот фрагмент. Сначала мы берём два ненулевых числа – поскольку оба параметра типов обёрнуты в Succ и могут оказаться Succ<..> сами. Идея этого правила в том, чтобы снимать один слой Succ с первого параметра типа и прикреплять ко второму. Тогда в конечном счёте второй параметр типа будет иметь всё Succ – общее число Succ, с которым они оба начинали – представляя сумму двух начальных количеств. Рассмотрим небольшой пример (я не буду делать это для всех слоёв):

 Add<Succ<Succ<Zero>>, Succ<Succ<Zero>>>
= Add<Succ<Zero>, Succ<Succ<Succ<Zero>>>> // перемещаем один Succ вправо
= Add<Zero, Succ<Succ<Succ<Succ<Zero>>>>> // повтор
= Succ<Succ<Succ<Succ<Zero>>>>> // базовый кейс :)

Наконец, у нас есть границы трейта – мы сообщаем rustc, что будем вызывать этот трейт (странная идея, не так ли?), только для типов, которые могут быть добавлены.

Вычитание работает аналогичным образом (реальное безумие начинается при делении). Определим базовые кейсы:

trait Sub {
type Diff;
}

impl Sub for (Zero, Zero) { // 0 - 0 = 0
type Diff = Zero;
}

impl<T> Sub for (Succ<T>, Zero) { // x - 0 = x
type Diff = Succ<T>;
}

impl<T> Sub for (Zero, Succ<T>) { // 0 - x = 0, достигаем насыщения
type Diff = Zero;
}

Здесь интересно лишь то, что мы определяем вычитание как насыщение. Это поможет реализовать деление. Если вы исключите это правило, компилятор избавит вас от возникновения отрицательного переполнения.

Как бы то ни было, вот наше рекурсивное правило:

impl<T, U> Sub for (Succ<T>, Succ<U>)
where
(T, U): Sub,
{
type Diff = <(T, U) as Sub>::Diff;
}

По сути, мы просто снимаем один слой Succ с каждого параметра типа, пока один из них не окажется нулевым. В итоге оставшийся и будет разностью. Наглядно это можно представить так:

5 [***] **
-
3 [***]
=
2 [ ] **

Здесь мы избавились от общих членов в скобках по одному.

▍ Умножение

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

trait Mul {
type Product;
}

impl<T> Mul for (T, Zero) { // x * 0 = 0
type Product = Zero;
}

impl<T> Mul for (Zero, Succ<T>) { // 0 * x = 0
type Product = Zero;
}

Теперь нам нужно быть чуть осторожнее с тем, для чего мы реализуем Mul. Если бы мы делали вторую реализацию для (Zero, T), у нас получилось бы две реализации, охватывающие (Zero, Zero). Поэтому мы реализуем её для (Zero, Succ<T>), поскольку Succ<T> никогда не равен Zero.

И теперь в качестве рекурсии у нас получается такой небольшой монстр:

impl<T, U> Mul for (Succ<T>, Succ<U>)
where
(T, Succ<U>): Mul,
(Succ<U>, <(T, Succ<U>) as Mul>::Product): Add,
{
type Product = <(
Succ<U>, // y
<(T, Succ<U>) as Mul>::Product // (x - 1) * y
) as Add>::Sum;
}

Здесь мы используем тот факт, что x * y = y + (x - 1) * y. Мы рекурсивно вычисляем второй член, после чего прибавляем его к первому множителю. Напомню, если Succ<T> представляет T + 1, тогда T представляет Succ<T> - 1.

И, наконец...

▍ Деление

Вот тут у нас получится уже конкретный монстр. Сначала нам нужно определить GreaterThanEq, чтобы проверять x >= y, поскольку некоторые операции деления будут с остатком, например 7 / 3. Объясню подробнее чуть позднее. Мы проделаем это по аналогии с тем, как проделывали Subtraction:

trait GreaterThanEq {
type Greater;
}

impl GreaterThanEq for (Zero, Zero) { // 0 >= 0
type Greater = Succ<Zero>;
}

impl<T> GreaterThanEq for (Zero, Succ<T>) { // 0 >!= { 1 .. }
type Greater = Zero;
}

impl<T> GreaterThanEq for (Succ<T>, Zero) { // { 1 .. } >= 0
type Greater = Succ<Zero>;
}

impl<T, U> GreaterThanEq for (Succ<T>, Succ<U>)
where
(T, U): GreaterThanEq, // x >= y -> x - 1 >= y - 1
{
type Greater = <(T, U) as GreaterThanEq>::Greater;
}

Разобравшись с этим, мы обработаем деление. Начнём с идеальных сочетаний, таких как 6 / 3. Вот наш бойлерплейт:

trait Div {
type Quotient;
}

impl<T> Div for (Zero, T) { // 0 / x = 0
type Quotient = Zero;
}

impl<T> Div for (Succ<T>, Succ<Zero>) { // x / 1 = x
type Quotient = Succ<T>;
}

Опять же, нам нужно быть осторожными с аргументами типов. Вместо выполнения второй реализации для (T, Succ<Zero>), мы проделываем её для (Succ<T>, Succ<Zero>), чтобы избежать наложения с первой реализацией для (Zero, Succ<Zero>). Теперь можно задействовать тождество x / y = 1 + (x - y) / y. По логике это означает, что мы просто отнимаем из x одну копию y, после чего рекурсивно отсчитываем другие. В коде это выглядит так:

type RawQuotient<T, U> = <(
Succ<Zero>, // 1
<(
<(Succ<T>, Succ<Succ<U>>) as Sub>::Diff,
Succ<Succ<U>> 
) as Div>::Quotient, // (x - y) / y
) as Add>::Sum;

Единственная проблема в том, что это выражение окажется неверным при x < y и вернёт 1. Вычитание насыщается при достижении 0, и мы получаем 1 + 0 / y = 1 + 0 = 1.

Нам лишь нужно совместить этот RawQuotient с тем фактом, что x / y равно 0, если x < y. Поскольку у нас это число представляет логическое значение, мы можем использовать приём с заменой условного перехода умножением (или cmov на ассемблере). Взгляните на следующую таблицу:

 Case Boolean of Gte RawQuotient Desired
+--------+ +----------------+ +-------------+ +---------+ 
| x >= y |: | 1 | x | nonzero | = | nonzero |
+--------+ +----------------+ +-------------+ +---------+ 
| x < y |: | 0 | x | ??? | = | 0 |
+--------+ +----------------+ +-------------+ +---------+ 

Можно просто умножить RawQuotient, опираясь на значение x. Если x >= y, у нас останется наш RawQuotient. Если же x < y, то мы будем умножать на нуль и в любом случае получим нуль, что и требуется.

Всё это ведёт к заключительной форме деления:

impl<T, U> Div for (Succ<T>, Succ<Succ<U>>)
where
(T, Succ<U>): Sub,
(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>): Div,
(
Succ<Zero>,
<(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
): Add,
(
<(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
<(
Succ<Zero>,
<(<(T, Succ<U>) as Sub>::Diff, Succ<Succ<U>>) as Div>::Quotient,
) as Add>::Sum,
): Mul,
(Succ<T>, Succ<Succ<U>>): GreaterThanEq,
{
// Привет! Я важная часть!
type Quotient = <(
<(Succ<T>, Succ<Succ<U>>) as GreaterThanEq>::Greater,
RawQuotient<T, U>,
) as Mul>::Product;
}

У нас есть много границ трейта, так как присутствует много подвыражений, для которых необходимо обеспечить возможность вычисления. Тем не менее в итоге всё это сводится к простой передаче цепочек Succ с Zero внизу.

Вы также можете заметить, что мы реализуем для (Succ <T>, Succ<Succ<U>>) рекурсивный кейс Div. Это означает, что знаменатель больше 1, и эта реализация не пересекается ни с какой другой.

В истинном стиле Rust, эта реализация, по сути, не позволит нам делить на 0, поскольку мы не реализовывали Div для (*, Zero).

Ну вот, собственно, и всё! Не знаю, как передать восторг, который я испытал при виде зелёных точек, сигнализирующих об успешном прохождении тестовых кейсов. Так что предлагаю вам проделать это самим, используя код из «Arithmetic in Rust's Type System».

▍ Примечание

Должен отметить, что я не первый, кто проделал подобное, хотя изначально думал, что это так. Справочную информацию можете найти в описании крейтов typenum и peano. typenum намного быстрее, и на практике обычно используется именно он.

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

На этом у меня всё. Приятного дня :)