Имитируем функционал зависимых типов в системе типов Rust

Системы типов — это настоящее безумие.

Некоторое время назад я уже отметился здесь со статьёй, в которой пытался разобрать, какие гарантии в compile-time может дать система типов Rust. Кое-какие интересные моменты удалось выловить уже тогда, однако больше всего меня зацепил весьма развёрнутый комментарий, описывающий некоторые вещи, доступные в зависимо-типизированном Idris.
Разумеется, я не мог остаться в стороне. Результат исследований доступен на github, а детальный разбор — под катом.

Сразу должен оговориться: само собой, настоящие зависимые типы в Rust, скорее всего, не реализуемы. Однако мы можем определить псевдозависимые, или квазизависимые (отсюда и название репозитория) типы, например, следующим образом:

Пусть у нас имеется некоторое семейство типов, состоящее из отдельных типов, далее — тип-экземпляр. Назовём это семейство квазизависимым типом, если для каждого типа-экземпляра при использовании в безопасном коде гарантируется поддержание некоторого инварианта, полностью определяемого конкретным типом-экземпляром.

Заметим, что формально под это определение подходит достаточно большое количество уже существующих типов — так, если мы рассмотрим "семейство", состоящее из одного типа str, мы формально можем сказать, что это семейство является квазизависимым типом — ведь тип str гарантирует, что его содержимое — валидный UTF-8. Но такие случаи нам, очевидно, не интересны, поэтому мы немного уточним определение:

Семейством типов назовём одно из двух:

• либо набор всевозможных типов, реализующих некоторый типаж (trait);
• либо набор всевозможных типов, получаемых подстановкой параметров в обобщённый тип.

С такой поправкой у нас, безусловно, всё ещё остаётся пространство для манёвра — я, например, не исключаю, что под это определение с определённой точки зрения подпадает даже банальный Vec<T>, но для дальнейшего изучения оно нам вполне подойдёт.

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

реализовать квазизависимый тип массива фиксированной длины (вектора) Vect<N, T>, инвариант которого — неизменная длина при неизменном значении параметра N.

Первая попытка: ложный след

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

Первое и основное: в качестве искомого семейства типов мы выберем семейство т.н. "непрозрачных" типов, удовлетворяющих некоторому типажу. Иначе говоря, единственным способом создать значение искомого квазизависимого типа должен быть возврат его из функции, возвращающей impl Trait. Однако, прежде чем мы перейдём к собственно типажу, нужно сделать несколько промежуточных шагов.

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

pub struct Vect<Item>(Vec<Item>);

Обратите внимание, что внутреннее поле структуры объявлено приватным — ни у кого извне права напрямую что-то сделать с этим стандартным вектором нет, даже если у них есть изменяемая ссылка на Vect.

Во-вторых, неизменяемый тип — это, конечно, хорошо, но какая-то возможность заглянуть внутрь у нас всё-таки должна быть (только так, чтобы не сломать инвариант). В этом месте я задумался о том, что неплохо было бы заранее заготовить возможность расширения, и написал следующее:

// Этому типажу обязаны удовлетворять все типы, которые мы размещаем внутри
// наших квазизависимых типов.
// А именно:
pub trait DependentInner: Sized {
    // должна существовать "замороженная" версия этого типа, которая
    // не позволяет сломать искомый инвариант;
    type Frozen: ?Sized;
    // должна быть возможность из уникальной ссылки на сам тип получить
    // уникальную ссылку на "замороженную" версию;
    fn freeze(&mut self) -> &mut Self::Frozen;
    // и должна быть возможность воссоздать тип из "замороженной" версии.
    fn recreate(_: &Self::Frozen) -> Self;
}

// А ещё для каждого такого типа мы автоматически реализуем два действия:
pub trait DependentInnerOperate: DependentInner {
    // трансформацию, т.е. генерацию нового объекта как изменённого старого,
    fn transform(mut self, f: impl FnOnce(&mut Self::Frozen)) -> Self {
        let mut tmp = Self::recreate(self.freeze());
        f(tmp.freeze());
        tmp
    }
    // и изменение in-place.
    fn operate(&mut self, f: impl FnOnce(&mut Self::Frozen)) {
        f(self.freeze());
    }
}
impl<T: DependentInner> DependentInnerOperate for T {}

Думаю, достаточно очевидно, как они реализуются для стандартного вектора — он тривиально преобразуется в срез, длина которого гарантированно неизменна, что нам, собственно, и требуется:

impl<Item: Clone> DependentInner for Vec<Item> {
    type Frozen = [Item];
    fn freeze(&mut self) -> &mut Self::Frozen {
        self.as_mut_slice()
    }
    fn recreate(frozen: &Self::Frozen) -> Self {
        frozen.iter().cloned().collect()
    }
}

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

Как мы и обещали, нам требуется создать типаж, который будет реализовывать наш Vect<T>. Окей, действуем:

pub trait DependentVec<Inner: DependentInnerOperate>: Sized {
    // тут определения методов
}
impl<Item: Clone> DependentVec<Vec<Item>> for Vect<Item> {
    // тут их реализация
}

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

{
    fn local<Item>() -> impl DependentVec<Vec<Item>> {
        // тут тело исходной функции
    }
    local()
}

Это одно из важных свойств impl Trait: даже если реально возвращаемый тип в разных случаях один и тот же, каждая такая функция будет рассматриваться как возвращающая уникальный анонимный тип. Теперь, чтобы сделать с этими типами что-то полезное, нам надо реализовать метод на Vect<T> и на соответствующем типаже:

impl<Item: Clone> DependentVec<Vec<Item>> for Vect<Item> {
    fn try_unify<T: DependentVec<Vec<Item>>>(self, other: T) -> Result<(Self, Self), (Self, T)> {
        if self.len() == other.len() {
            let other = Self(other.into_inner());
            Ok((self, other))
        } else {
            Err((self, other))
        }
    }
}

Таким образом, если try_unify вернула Ok, мы знаем — и, главное, знает компилятор! — что два значения внутри Ok на самом деле одного и того же типа.

Ну и, наконец, напишем простенькую тестовую функцию:

pub fn zip_add<Item, T>(first: &T, second: &T) -> T
where
    Item: AddAssign<Item> + Clone,
    T: DependentVec<Vec<Item>> {
    first.map_ref(|v1| 
        second.consume_ref(|v2| 
            v1.iter_mut()
                .zip(v2.iter())
                .for_each(|(i1, i2)| *i1 += i2.clone())
        )
    )
}

Где функции map_ref и consume_ref определены, соответственно, так:

impl<Item: Clone> DependentVec<Vec<Item>> for Vect<Item> {
    fn inner(&self) -> &Vec<Item> {
        &self.0
    }
    fn map_ref(&self, f: impl FnOnce(&mut <Vec<Item> as DependentInner>::Frozen)) -> Self {
        let mut inner = self.inner().clone();
        f(inner.freeze());
        Self(inner)
    }
    fn consume_ref(&self, f: impl FnOnce(&mut <Vec<Item> as DependentInner>::Frozen)) {
        f(self.inner().clone().freeze())
    }
}

(Названия объясняются тем, что в ходе работы также имелись функции map и consume, принимающие self)

Не стану скрывать, конструкция получилась весьма громоздкая, к тому же сильно отталкивала необходимость дублировать описания функций и в типаже, и в реализации — привет, Си, привет, файлы заголовков, давно не виделись!

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

Полезная часть

Что, всё-таки, удалось извлечь из этой первой реализации?

Во-первых, это идея "замороженного типа", которая в итоге, после всех упрощений и корректировок, преобразовалась в описанный ниже типаж Dependent.

Во-вторых, это, разумеется, первая тестовая функция — та самая zip_add, которая компилируется только тогда, когда ей переданы два вектора гарантированно одинаковой длины. Она также была неоднократно переработана в процессе дальнейшей разработки, но сама идея осталась прежней.

Вторая попытка: шаги реализации

Сразу выделим три ключевых изменения, которые было решено внести при переработке.

Во-первых, как уже было сказано выше, семейство типов Vect на самом деле должно иметь не один, а два параметра, один из которых, как и ранее, характеризует содержание вектора, другой — отвечает за длину. Как будет показано ниже, такой тип можно просто вернуть из обобщённой функции, не генерируя в явном виде множество её копий, а вместо этого меняя только собственно обобщённый параметр; как следствие, макрос (который при таком подходе тоже необходим) можно сделать существенно более простым.

Во-вторых, для описания длины вектора — а, на самом деле, для описания любых натуральных чисел, — мы вводим новый типаж Nat, которому можем заранее прописать все необходимые свойства.

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

qd_core: типаж Dependent

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

pub trait Dependent {
    type Inner: DependentInnerOperate;
    fn from_inner(_: Self::Inner) -> Self
    where
        Self: Sized;
    fn into_inner(self) -> Self::Inner;
    fn inner(&self) -> &Self::Inner;
}
pub trait DependentOperate: Dependent {
    // здесь содержатся реализации методов map, consume и т.д.
    // в терминах from_inner/into_inner/inner
}
impl<T: Dependent> DependentOperate for T {}

Вскоре, однако, стало ясно, что наличие нескольких отдельных типажей только создаёт дополнительные сложности, никак при этом не упрощая нам жизнь. Мы можем избавиться от них, переместив тип Frozen непосредственно в типаж Dependent и устранив автоматически реализованные методы:

pub trait Dependent {
    type Native;
    type Frozen: ?Sized;
    fn freeze(&self) -> &Self::Frozen;
    fn freeze_mut(&mut self) -> &mut Self::Frozen;
    fn into_native(self) -> Self::Native;
    fn as_native(&self) -> &Self::Native;
}

На этом этапе может возникнуть вопрос, а зачем нам, собственно, этот типаж? Я на это отвечу так: технически, да, на этом этапе он уже перестал быть нужен. Я сохранил его в коде в основном в качестве своеобразной документации — описания того, что мы ждём от любого квазизависимого типа. Теоретически, мы могли бы написать какие-нибудь методы, способные принимать любой квазизависимый тип и совершать с ним некоторые операции, аналогично монадическим конструкциям, но на нынешнем этапе единственный содержательный элемент этого типажа — явно задекларированные типы Native и Frozen, которые, если бы Rust это позволил, спокойно могли бы быть добавлены непосредственно на тип.

qd_nat: длина вектора

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

Недолго думая, создадим для этого новый типаж:

pub trait Nat: Sized {
    fn as_usize(&self) -> usize;
    fn from_usize(s: usize) -> Self;
}

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

use std::marker::PhantomData;

#[derive(Copy, Clone, Debug)]
pub struct Equiv<T1: Nat, T2: Nat>(PhantomData<(T1, T2)>);

impl<T1: Nat, T2: Nat> Equiv<T1, T2> {
    pub fn rev(self) -> Equiv<T2, T1> {
        Equiv(PhantomData)
    }
}

pub trait NatEq: Nat {
    fn eq<N: Nat>(this: Self, other: N) -> Option<Equiv<Self, N>> {
        if this.as_usize() == other.as_usize() {
            Some(Equiv(PhantomData))
        } else {
            None
        }
    }
}
impl<T: Nat> NatEq for T {}

qd_vect: собственно вектор

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

pub struct Vect<T, N: Nat>(Vec<T>, PhantomData<N>);
impl<Item: Clone, N: Nat> Dependent for Vect<Item, N> {
    type Native = Vec<Item>;
    type Frozen = [Item];
    fn freeze(&self) -> &Self::Frozen {
        self.0.as_slice()
    }
    fn freeze_mut(&mut self) -> &mut Self::Frozen {
        self.0.as_mut_slice()
    }
    fn into_native(self) -> Self::Native {
        self.0
    }
    fn as_native(&self) -> &Self::Native {
        &self.0
    }
}

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

pub fn collect<Item: Clone, N: Nat, I: IntoIterator<Item = Item>>(iter: I) -> (N, Vect<Item, N>) {
    let inner: Vec<_> = iter.into_iter().collect();
    (N::from_usize(inner.len()), Vect(inner, PhantomData))
}

Как видим, эта функция, помимо самого вектора, возвращает ещё и некоторый объект с типажом Nat, описывающий его длину.

Попробуем протестировать полученную конструкцию, для этого воспользуемся уже знакомой функцией zip_sum, переписав её под новый интерфейс:

fn zip_sum<T: Clone + Add<T, Output = T>, N: Nat>(
    first: Vect<T, N>,
    second: Vect<T, N>,
) -> Vect<T, N> {
    let mut v1 = first.clone();
    let v2 = second.freeze();
    v1.freeze_mut().iter_mut()
        .zip(v2.iter())
        .for_each(|(i1, i2)| *i1 = i1.clone() + i2.clone())
    v1
}

Теперь, соответственно, перед нами встаёт вопрос, как нам получить объект Vect — а точнее, как вызвать определённую выше функцию collect, поскольку попытка это сделать "в лоб" приведёт к ошибке вроде такой:

error[E0283]: type annotations needed for `(N, Vect<u32, N>)`
  --> ${MODULE}/tests/test.rs:7:13
   |
7  |     let _ = collect(vec![1u32]);
   |         -   ^^^^^^^ cannot infer type for type parameter `N` declared on the function `collect`
   |         |
   |         consider giving this pattern the explicit type `(N, Vect<u32, N>)`, where the type parameter `N` is specified
   | 
  ::: ${MODULE}/src/lib.rs:28:32
   |
28 | pub fn collect<Item: Clone, N: Nat, I: IntoIterator<Item = Item>>(iter: I) -> (N, Vect<Item, N>) {
   |                                --- required by this bound in `collect`
   |
   = note: cannot satisfy `_: Nat`
help: consider specifying the type arguments in the function call
   |
7  |     let _ = collect::<Item, N, I>(vec![1u32]);
   |                    ^^^^^^^^^^^^^^

Первый — и кажущийся очевидным — вариант состоит в том, чтобы просто сгенерировать новый тип непосредственно перед вызовом функции, а затем передать его в качестве обобщённого параметра:

#[derive(Copy, Clone)]
struct N(usize);
impl Nat for N {
    fn as_usize(&self) -> usize {
        self.0
    }
    fn from_usize(s: usize) -> Self {
        Self(s)
    }
}
let _ = collect::<_, $n, _>($v);

Однако с таким подходом возникает достаточно очевидная проблема: у нас нет никакого способа поддержать инвариант для типа N. Нет никаких гарантий, что кто-то не попытается определить этот тип, а затем вызвать N::from_usize с двумя разными аргументами.

qd_timestamp_marker: де-факто приватный типаж

Выход из этой ситуации простой: типаж Nat должен быть реализован строго подконтрольным образом. Каким именно образом — мы опишем чуть ниже, а здесь разговор пойдёт о том, как добиться этой самой подконтрольности. Строго говоря — никак, но есть один относительно несложный трюк, о сути которого можно догадаться из названия модуля.

Допустим, мы подготовили реализацию нашего типажа Nat и предоставили возможность сгенерировать эту реализацию для нового типа через некоторый макрос:

#[macro_export]
macro_rules! n {
    () => {
        #[derive(Copy, Clone)]
        struct N(usize);
        impl $crate::Nat for N {
            // реализация
        }
    };
}

Вопрос: что может помешать пользователю написать ровно тот же самый код от руки? В процессе работы над этим проектом я задал этот вопрос на форуме Rust (применительно к первому варианту реализации, но это не сильно что-то изменило), и получил на него в числе прочего такой вот ответ, сводящийся к достаточно простой идее: написать процедурный макрос, который некоторым случайным (или не случайным, но и не постоянным) образом поменяет как определение типажа, так и реализующий его макрос. В этом случае реализовать типаж вручную будет невозможно — его имя будет генерироваться заново при каждой компиляции пакета.

Что ж, пишем:

extern crate proc_macro;

use proc_macro::TokenStream;
use quote::{format_ident, quote, ToTokens};
use std::time::{SystemTime, UNIX_EPOCH};
use syn::*;

#[proc_macro_attribute]
pub fn timestamp_marker(attr: TokenStream, input: TokenStream) -> TokenStream {
    // Макрос будет преобразовывать модуль целиком, со всем содержимым
    let mut input = parse_macro_input!(input as ItemMod);

    // Идентификатор, который мы будем заменять, передадим как параметр
    let replaced = parse_macro_input!(attr as Ident);
    // А в качестве замены возьмём его же, но с приделанным текущим timestamp-ом
    let replacement = format_ident!(
        "{}{}",
        replaced,
        SystemTime::now()
            .duration_since(UNIX_EPOCH)
            .expect("Time went backwards")
            .as_millis()
    );

    // Извлекаем содержимое модуля
    let content = input
        .content
        .as_mut()
        // Если его нет (т.е. модуль в отдельном файле) - паникуем, получим ошибку компиляции
        .expect("Only the inline modules can be labeled with timestamp");
    // И прогоняем каждый элемент через функцию замены (см. ниже)
    content.1.iter_mut().for_each(|item| {
        *item = parse2(update(item.to_token_stream(), &replaced, &replacement)).unwrap()
    });

    let output = quote! { #input };
    output.into()
}

fn update(item: proc_macro2::TokenStream, from: &Ident, to: &Ident) -> proc_macro2::TokenStream {
    use proc_macro2::*;
    item.into_iter()
        // Нас здесь интересует два основных варианта:
        // либо перед нами группа (т.е. нечто в скобках),
        // либо перед нами идентификатор.
        .map(|tok| match tok {
            TokenTree::Group(group) => {
                // Группу мы обрабатываем рекурсивно,
                let mut new_group = Group::new(group.delimiter(), update(group.stream(), from, to));
                // не забывая указать новой группе корректное местоположение
                new_group.set_span(group.span());
                TokenTree::Group(new_group)
            }
            TokenTree::Ident(ident) if &ident == from => {
                // Идентификатор мы меняем, только если он совпадает с заменяемым.
                let mut to = to.clone();
                // И, опять же, не забываем про местоположение.
                to.set_span(ident.span());
                TokenTree::Ident(to)
            }
            // Всё прочее оставляем как есть.
            tok => tok,
        })
        .collect()
}

qd_nat: квазизависимые числа

Так как типаж Nat используется во внешнем коде, непосредственно его пометить мы не можем. Обходится проблема очень просто:

#[timestamp_marker(NatInner)]
pub mod nat {
    pub unsafe trait NatInner {}
    pub trait Nat: Sized + NatInner + Clone + Copy {
        fn as_usize(&self) -> usize;
        fn from_usize(s: usize) -> Self;
    }
}

Реализовать типаж Nat по-прежнему можно где угодно, и мы этим воспользуемся. А вот типаж NatInner — уже нет, и, следовательно, все реализации типажа Nat становятся нам подконтрольны. Также типаж NatInner сделан "небезопасным" — чтобы мы позже имели право рассчитывать на свойства типажа Nat в другом небезопасном коде, даже если кто-то ухитрится обойти нашу подставу с маркировкой.

Теперь вернёмся к предложенному ранее варианту с макросом. Немного скорректируем его определение, а именно, будем принимать на вход последовательность выражений, в пределах которой искомый тип существует под именем N:

macro_rules! with_n {
    ($($inner:tt)*) => {{
        #[derive(Copy, Clone, Debug)]
        struct N;
        unsafe impl $crate::NatInner for N {}
        impl $crate::Nat for N {
            // тут реализация
        }
        $($inner)*
    }};
}

Обратите внимание, правая часть макроса содержит двойные фигурные скобки. За счёт этого генерируемый макросом код становится блоком и, во-первых, может использоваться как выражение — в частности, стоять в правой части оператора присваивания, — во-вторых, ограничивает область видимости определённых в нём элементов, в том числе и типа N, благодаря чему несколько вызовов with_n подряд не вызовут конфликтов, а тип N нельзя будет использовать вне макроса.

Пора заниматься самой реализацией. В нынешнем проекте она была построена следующим образом: каждый такой макрос создаёт статическую структуру определённого типа — по сути, write-only вариант для AtomicUsize, которая будет хранить однажды записанное значение и выдавать его по запросу. Не будем разбирать реализацию структуры — просто скажем, что она по большей части опирается на код, приведённый здесь, ограничимся только интерфейсом:

use thiserror::Error;

#[derive(Debug, Error)]
pub enum NatStoreError {
    // Ошибка для случая, когда несколько вызовов `store()` были запущены одновременно
    #[error("Attempted to concurrently create multiple instances of N: Nat")]
    Concurrent,
    // Ошибка для случая, когда мы попытались затереть уже сохранённое значение
    #[error("Attempted to override already stored value {0} with {1}")]
    AlreadyStored(usize, usize),
}

pub struct NatHolder { /* skipped */ }
impl NatHolder {
    pub const fn new() -> Self {
        // skipped
    }
    pub fn store(&self, value: usize) -> Result<(), NatStoreError> {
        // skipped
    }
    pub fn read(&self) -> Option<usize> {
        // skipped
    }
}

А теперь — сам Nat. Заодно мы немного расширим API наших натуральных чисел, а именно:

• добавим возможность создавать объект, имея только тип, но не значение — это может пригодиться в обобщённом коде (хотя в нынешнем проекте эти методы не используются, но удалить их всё равно рука не поднялась);
• добавим возможность получить число, соответствующее типу, не имея самого объекта — это нам пригодится чуть позже.

Собственно:

pub trait Nat: Sized + NatInner + Clone + Copy {
    fn get_usize() -> Option<usize>;
    fn as_usize(self) -> usize;
    fn from_usize(s: usize) -> Result<Self, crate::NatStoreError>;
    fn get() -> Self;
    fn try_get() -> Option<Self>;
}

#[macro_export]
macro_rules! with_n {
    ($($inner:tt)*) => {{
        // пропуск
        impl $crate::Nat for N {
            fn get_usize() -> Option<usize> {
                HOLDER.read()
            }
            fn as_usize(self) -> usize {
                // Этот вызов никогда не должен проваливаться,
                // т.к. раз объект создан, Holder должен быть уже инициализирован
                HOLDER.read().unwrap();
            }
            fn from_usize(s: usize) -> Result<Self, $crate::NatStoreError> {
                HOLDER.store(s).map(|_| Self)
            }
            fn get() -> Self {
                Self::try_get().expect("Trying to `get` the number which is yet undefined")
            }
            fn try_get() -> Option<Self> {
                Self::get_usize().map(|_| Self)
            }
        }
        $($inner)*
    }};
}

И ещё, забегая немного вперёд, во-первых, добавим небольшую функцию-утилиту — фактически, чуть более приятный вариант обычного Result::unwrap:

pub fn expect_nat<N: Nat>(s: usize) -> N {
    N::from_usize(s).unwrap_or_else(|err| panic!(format!("{}", err)))
}

А во-вторых, скорректируем определение Equiv с использованием нового API:

impl<N1: Nat, N2: Nat> Equiv<N1, N2> {
    pub fn check() -> Option<Self> {
        N1::get_usize().and_then(|n1| {
            N2::get_usize().and_then(|n2| {
                if n1 == n2 {
                    Some(Self(PhantomData))
                } else {
                    None
                }
            })
        })
    }
    pub fn try_prove_for(_: N1, _: N2) -> Option<Self> {
        Self::try_create()
    }
}

Кроме того, уже сейчас мы можем накидать небольшой тест. А именно, задать вот такую функцию:

fn accepts_pair<N1: Nat, N2: Nat>(n1: N1, n2: N2, _proof: Equiv<N1, N2>) {
    // этот assertion никогда не должен проваливаться
    assert_eq!(n1.as_usize(), n2.as_usize());
}

Она принимает два числа (точнее, объекта с типажом Nat), которые должны быть гарантированно равны. Убедимся, что проверки действительно работают:

#[test]
fn checked() {
    use qd_nat::with_n;

    let n = with_n!(N::from_usize(1).unwrap());
    let n1 = with_n!(N::from_usize(1).unwrap());
    let n2 = with_n!(N::from_usize(2).unwrap());

    match Equiv::try_prove_for(n, n1) {
        Some(proof) => accepts_pair(n, n1, proof),
        None => panic!("1 != 1, WTF?"),
    };
    match Equiv::try_prove_for(n1, n2) {
        None => {}
        Some(_) => panic!("1 == 2, WTF?"),
    }
}

Что ж, похоже, здесь всё хорошо. Пора возвращаться к нашим векторам!

qd_vect: наконец-то создаём

Для создания вектора мы используем совершенно тривиальную обёртку над with_n:

#[macro_export]
macro_rules! vect {
    ($data:expr) => {
        ::qd_nat::with_n! {
            let v = $data;
            $crate::collect::<_, N, _>(v)
        }
    };
}

Работает эта конструкция предельно грубо и прямолинейно: запрашиваем свежий тип N, передаём его через "турборыбу" функции collect, в качестве аргумента ей скармливаем входные данные. На выходе получаем искомый Vect<N, T>.

Так как интерфейс типажа Nat изменился, немного поменяется и функция collect:

pub fn collect<Item, N: Nat, I: IntoIterator<Item = Item>>(
    iter: I,
) -> (N, Vect<Item, N>) {
    let inner: Vec<_> = iter.into_iter().collect();
    // Nat::from_usize теперь возвращает Result -
    // воспользуемся вспомогательной функцией и распакуем его
    (expect_nat(inner.len()), Vect(inner, PhantomData))
}

Теперь вспомним про нашу тестовую функцию zip_sum. Она ожидает на входе два вектора одного и того же типа, с одним и тем же параметром N; в противном случае она не скомпилируется. Следовательно, нам нужна возможность каким-то образом приводить два вектора к одному типу, при условии, что они имеют равную длину — иначе мы эту операцию просто не вправе проводить.

Условие, как мы помним, выражается через существование объекта типа Equiv<N1, N2>. Задействуем это:

impl<Item, N: Nat> Vect<Item, N> {
    pub fn retag<New: Nat>(self, _proof: Equiv<N, New>) -> Vect<Item, New> {
        Vect(self.0, PhantomData)
    }
}

И теперь, наконец-то, можем написать первый реальный тест для вектора:

fn summing() {
    let (_, v1) = vect!(vec![1]);
    let (_, v2) = vect!(vec![1]);

    assert_eq!(
        // Пробуем создать объект Equiv, и, если получилось...
        Equiv::check()
            // ...передаём его в retag, меняя тип v2...
            .map(|proof| v2.retag(proof))
            // ...суммируем два вектора - теперь они оба одного типа...
            .map(|v2| zip_sum(v1, v2))
            // ...превращаем квазизависимый вектор в обычный...
            .map(Vect::into_native),
        // ...и убеждаемся, что действительно всё получилось.
        Some(vec![2])
    );
}

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

Абсолютно аналогичным образом мы можем убедиться, что сложить два вектора разной длины нам не дадут:

#[test]
fn summing_mismatch() {
    let (_, v1) = vect!(vec![]);
    let (_, v2) = vect!(vec![1]);

    assert_eq!(
        Equiv::check()
            .map(|proof| v2.retag(proof))
            .map(|v2| zip_sum(v1, v2))
            .map(Vect::into_native),
        None
    );
}

В принципе, программа-минимум на этом уже выполнена. Тем не менее, у нас есть в запасе ещё пара идей.

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

#[test]
fn runtime_size() {
    macro_rules! parse_i64_discarding {
        ($string:literal) => {
            vect! {{
                use std::str::FromStr;
                let string: &str = &*$string;
                // vect! принимает произвольный итерируемый объект - воспользуемся этим
                string.split(",").map(i64::from_str).filter_map(Result::ok)
            }}
        };
    }

    let (_, v1) = parse_i64_discarding!("1,2,3,four,5");
    let (_, v2) = parse_i64_discarding!("1,two,3,4,5");
    assert_eq!(
        Equiv::check().map(|proof| zip_sum(v1.retag(proof), v2).into_native()),
        Some(vec![2, 5, 7, 10])
    );
}

Далее, вернёмся снова к нашим натуральным числам.

qd_nat: тип "число меньше N"

Снова вспомним наш источник вдохновения: при индексации вектора мы могли использовать тип Fin n, означающий буквально "какое-то — неизвестно, какое — натуральное число, гарантированно меньшее, чем n" (а следовательно, гарантированно подходящее в качестве индекса).

Попробуем реализовать этот тип в Rust. Выглядеть он будет следующим образом:

#[derive(Copy, Clone, Debug)]
pub struct Fin<N: Nat>(usize, PhantomData<N>);

Как и раньше, любой способ создать объект этого типа оказывается ограничен рамками его собственного модуля.

Способов мы предусмотрим два: из числа (с рантаймовой проверкой) и из итератора. Начнём с первого, как более простого, и заодно дадим возможность извлекать число из объекта:

impl<N: Nat> Fin<N> {
    pub fn from_usize(s: usize) -> Option<Self> {
        if s < N::get_usize()? {
            Some(Self(s, PhantomData))
        } else {
            None
        }
    }
    pub fn as_usize(self) -> usize {
        self.0
    }
}

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

pub struct IterUntil<N: Nat>(usize, PhantomData<N>);
impl<N: Nat> Iterator for IterUntil<N> {
    type Item = Fin<N>;
    fn next(&mut self) -> Option<Fin<N>> {
        if self.0 < N::get_usize().unwrap() {
            let ret = Some(Fin(self.0, PhantomData));
            self.0 += 1;
            ret
        } else {
            None
        }
    }
}

Заметим, что использование этого итератора с ещё не определённым конечным числом — ошибка, и попытка получить очередное значение приведёт к панике. Лично я считаю, что это вполне разумное поведение, но, технически, можно заставить его в этом случае возвращать None — просто завернув всю логику в N::get_usize().and_then().

impl<N: Nat> Iterator for IterUntil<N> {
    type Item = Fin<N>;
    fn next(&mut self) -> Option<Fin<N>> {
        let ret = if self.0 < N::get_usize().unwrap() {
            Some(Fin(self.0, PhantomData))
        } else {
            None
        };
        self.0 += 1;
        ret
    }
}

#[test]
fn overflow() {
    let n = with_n! { N::from_usize(usize::MAX).unwrap() };
    // пропустим все элементы, кроме последнего
    let mut iter = n.iter_until_this().skip(usize::MAX - 1);
    // получим этот последний...
    assert_eq!(iter.next().map(Fin::as_usize), Some(usize::MAX - 1));
    // ...убедимся, что за ним ничего нет...
    assert_eq!(iter.next().map(Fin::as_usize), None);
    // ...но при этом получим переполнение, и следующий next() вернёт Some(0)
    assert_eq!(iter.next().map(Fin::as_usize), None);
}

impl<N: Nat> Iterator for IterUntil<N> {
    // пропуск
    #[inline]
    fn nth(&mut self, n: usize) -> Option<Fin<N>> {
        let max_value = N::get_usize().unwrap();
        if let Some(plus_n) = self.0.checked_add(n) {
            if plus_n < max_value {
                self.0 = plus_n + 1;
                return Some(Fin(plus_n, PhantomData));
            }
        }
        self.0 = max_value;
        None
    }
}

Наконец, нам нужен способ создавать этот итератор, для чего мы реализуем типаж-расширение поверх типажа Nat:

pub trait NatIterUntil: Nat {
    fn iter_until() -> IterUntil<Self> {
        IterUntil(0, PhantomData)
    }
    fn iter_until_this(self) -> IterUntil<Self> {
        Self::iter_until()
    }
}
impl<N: Nat> NatIterUntil for N {}

И, вооружившись этим инструментом, снова возвращаемся к векторам.

qd_vect: гарантированно корректный индекс

Как уже было сказано выше, Fin<N> нам может пригодиться как гарантированно корректный индекс в Vect<N, T>. К примеру, мы можем реализовать следующий метод:

impl<Item, N: Nat> Vect<Item, N> {
    pub fn find_index(&self, mut predicate: impl FnMut(&Item) -> bool) -> Option<Fin<N>> {
        N::iter_until().find(|&n| predicate(&self[n]))
    }
}

Прелесть ситуации заключается в том, что теперь мы вправе написать небольшой unsafe-код, который будет корректен благодаря гарантиям, даваемым типом Fin и самим типом вектора:

impl<Item, N: Nat> Index<Fin<N>> for Vect<Item, N> {
    type Output = Item;
    fn index(&self, index: Fin<N>) -> &Item {
        // Безопасность: Fin<N>::as_usize(fin) < N::get_usize() == self.0.len() 
        unsafe { self.0.get_unchecked(index.as_usize()) }
    }
}

Это, пожалуй, не слишком интересно на практике — цена проверки на попадание в границы вектора в тех случаях, где можно применить Fin, обычно невелика, но сам факт, что можно на уровне типов гарантировать получение элемента вектора, занятен.

И это пока ещё не всё.

qd_nat: фиксированные числа

В прошлой статье мы для финальной стадии наших разработок использовали чёрную магию типов на основе typenum. Почему бы не вспомнить о нём и здесь? В конце концов, типаж Unsigned из typenum формально тоже является квазизависимым натуральным числом — с той маленькой поправкой, что значение каждого такого числа известно на этапе компиляции.

И, действительно, мы можем реализовать наш типаж Nat для чисел из typenum:

use typenum::Unsigned;

unsafe impl<T: Unsigned> NatInner for T {}
impl<T: Unsigned + Default + Copy + Clone> Nat for T {
    fn get_usize() -> Option<usize> {
        Some(Self::USIZE)
    }
    fn as_usize(self) -> usize {
        Self::USIZE
    }
    fn from_usize(s: usize) -> Result<Self, NatStoreError> {
        if s == Self::USIZE {
            Ok(Self::default())
        } else {
            Err(NatStoreError::AlreadyStored(Self::USIZE, s))
        }
    }
    fn get() -> Self {
        Self::default()
    }
    fn try_get() -> Option<Self> {
        Some(Self::default())
    }
}

Единственное условно-тонкое место здесь — как получить объект обобщённого типа. Тут мы воспользовались тем простым фактом, что типаж Unsigned требует наличия типажа Default.

qd_vect: generic array на новый лад

Используя реализацию выше, мы можем создавать векторы, длина которых известна во время компиляции. Пока что не совсем понятно, зачем это может пригодиться, когда у нас есть generic_array, но тем не менее:

#[test]
fn fixed_size() {
    use qd_vect::collect;
    use typenum::consts::*;
    let (_, v) = collect::<_, U2, _>(vec![1u32, 2]);
    assert_eq!(v.into_native(), vec![1u32, 2]);
}

#[test]
#[should_panic(expected = "Attempted to override already stored value 2 with 1")]
fn fixed_size_mismatch() {
    use qd_vect::collect;
    use typenum::consts::*;
    let _ = collect::<_, U2, _>(&[1]);
}

Но и это ещё не всё.

qa_nat: операции над числами

Вернёмся снова к нашим квазизависимым числам. До сих пор всё, что мы умели с ними делать, — создавать и проверять на равенство (с помощью типа Equiv). Это, безусловно, интересно, но мы можем сделать больше — а именно, мы можем организовать арифметику для таких чисел.

В текущем проекте мы ограничимся только сложением — во-первых, это наиболее простая операция, во-вторых, в нынешнем контексте (работы с векторами) она имеет вполне ясный смысл (конкатенация). Заведём отдельный тип для суммы двух натуральных чисел:

#[derive(Copy, Clone)]
pub struct Add<N1: Nat, N2: Nat>(PhantomData<(N1, N2)>);

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

impl<N1: Nat, N2: Nat> Nat for Add<N1, N2> {
    fn get_usize() -> Option<usize> {
        N1::get_usize().and_then(|n1| N2::get_usize().map(|n2| n1 + n2))
    }
    fn as_usize(self) -> usize {
        Self::get_usize().expect("`Add` was created and queried before its components were set")
    }
    fn from_usize(s: usize) -> Result<Self, NatStoreError> {
        if let Some(inner) = Self::get_usize() {
            if inner == s {
                Ok(Self(PhantomData))
            } else {
                Err(NatStoreError::AlreadyStored(inner, s))
            }
        } else {
            todo!("Needs fix to NatStoreError")
        }
    }
    fn get() -> Self {
        Self::try_get().expect("Trying to create `Add` instance which is yet undefined")
    }
    fn try_get() -> Option<Self> {
        Self::get_usize().map(|_| Self(PhantomData))
    }
}

Единственное место, с которым есть вопросы, — todo в from_usize. Дело в том, что на начальном этапе мы не предусмотрели такой возможности — мы рассматривали только "простые" натуральные числа, непосредственно соответствующие тому или иному обычному числу, а не собираемые из нескольких компонентов.

Добавим третий вариант в NatStoreError:

#[derive(Debug, Error)]
pub enum NatStoreError {
    // пропуск
    #[error("Attempted to create composite number {0} before its components")]
    UnknownCompositeParts(&'static str),
}

И соответствующим образом исправим from_usize:

fn from_usize(s: usize) -> Result<Self, NatStoreError> {
    if let Some(inner) = Self::get_usize() {
        // пропуск
    } else {
        Err(NatStoreError::UnknownCompositeParts(std::any::type_name::<Self>()))
    }
}

Теперь попытка создать объект Add раньше времени будет корректно проваливаться. Например, такая:

#[test]
#[should_panic]
fn add_unknown() {
    with_n! {
        let _: Add<N, N> = Add::from_usize(0).unwrap();
    }
}

Стабильного сообщения об ошибке мы, к сожалению, не получим, поскольку метод std::any::type_name не даёт никаких гарантий относительно результатов работы, кроме того, что это будет человекочитаемое представление типа; поэтому на этом тесте мы ставим просто should_panic, без указания конкретного сообщения об ошибке.

qd_vect: конкатенация

Ну что ж, теперь мы можем рассмотреть строго типизированную конкатенацию квазизависимых векторов. Добавим ещё один метод к Vect:

impl<Item, N: Nat> Vect<Item, N> {
    fn concat<N2: Nat>(mut self, vect: Vect<Item, N2>) -> Vect<Item, Add<N, N2>> {
        self.0.extend(vect.into_native());
        Vect(self.0, PhantomData)
    }
}

И, что называется, чтоб два раза не вставать — заодно и ещё один:

impl<Item, N: Nat> Vect<Item, N> {
    pub fn push(mut self, item: Item) -> Vect<Item, Add<N, typenum::consts::U1>> {
        self.0.extend(std::iter::once(item));
        Vect(self.0, PhantomData)
    }
}

Конкретно push нам сейчас не слишком интересен, впрочем, а вот с concat мы можем добавить ещё кое-что.

А именно — учесть свойства сложения.

qd_core: статически выводимые факты

Но, прежде чем мы займёмся конкретными примерами, попробуем прикинуть в более общем виде, что мы хотим получить. А хотим мы в данном случае следующее.

Во-первых, возможность указать для некоторых свойств, выраженных в виде доказательства (как Equiv), что это свойство гарантированно выполняется, а следовательно, доказательство можно сгенерировать во время компиляции. Простейший пример — равенство числа самому себе: нам не нужно никаких проверок, чтобы создать Equiv<N, N>.

Во-вторых, возможность указать для некоторых свойств, что они могут быть выведены во время компиляции из других свойств. Опять же, простейший пример — если мы доказали, что N1 = N2, т.е. получили объект типа Equiv<N1, N2>, нам не нужны дополнительные проверки, чтобы получить Equiv<N2, N1>.

Сформулируем эти две возможности в виде типажей:

pub trait StaticallyProvable {
    // Нам ничего не нужно, чтобы вывести доказательство, - оно уже выражено в типах.
    fn proof() -> Self;
}

pub trait Deducible<Reason> {
    // Мы используем уже доказанный факт, чтобы вывести доказательство следующего факта.
    fn deduce(_: Reason) -> Self;
}

qd_nat: фиксируем свойства чисел и операций

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

impl<N: Nat> Equiv<N, N> {
    pub fn refl() -> Self {
        Self(PhantomData)
    }
}
impl<N: Nat> StaticallyProvable for Equiv<N, N> {
    fn proof() -> Self {
        Self::refl()
    }
}

Здесь понятие refl опять-таки позаимствовано из Idris — считайте это лёгкой попыткой выехать на уже известных понятиях.

Также мы можем зафиксировать понятия о симметричности и транзитивности равенства:

// Вспомогательный тип - объединяет два доказанных ранее равенства
type Transit<N1, N2, N3> = (Equiv<N1, N2>, Equiv<N2, N3>);

impl<N1: Nat, N2: Nat, N3: Nat> Deducible<Transit<N1, N2, N3>> for Equiv<N1, N3> {
    fn deduce(_: Transit<N1, N2, N3>) -> Self {
        Self(PhantomData)
    }
}

impl<N1: Nat, N2: Nat> Deducible<Equiv<N1, N2>> for Equiv<N2, N1> {
    fn deduce(_: Equiv<N1, N2>) -> Self {
        Self(PhantomData)
    }
}

Попробуем теперь подсказать компилятору, что определённая ранее операция сложения симметрична:

impl<N1: Nat, N2: Nat> StaticallyProvable for Equiv<Add<N1, N2>, Add<N2, N1>> {
    fn proof() -> Self {
        Self(PhantomData)
    }
}

И немедленно получим ошибку:

error[E0119]: conflicting implementations of trait `qd_core::StaticallyProvable` for type `eq::Equiv<ops::Add<_, _>, ops::Add<_, _>>`:
  --> qd_nat/src/ops.rs:42:1
   |
42 | impl<N1: Nat, N2: Nat> StaticallyProvable for Equiv<Add<N1, N2>, Add<N2, N1>> {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `eq::Equiv<ops::Add<_, _>, ops::Add<_, _>>`
   | 
  ::: qd_nat/src/eq.rs:40:1
   |
40 | impl<N: Nat> StaticallyProvable for Equiv<N, N> {
   | ----------------------------------------------- first implementation here

Причина проста: в случае, если N1 и N2 — это один и тот же тип, мы получим две формально разные реализации одного типажа. Здесь неважно, что в обоих случаях метод proof будет возвращать одно и то же значение одного и того же типа: Rust всё равно не допустит наличия неоднозначности.

Мне здесь удалось найти три варианта решения проблемы.

Вариант первый — просто исключить одну из реализаций. Вариант, очевидно, нежелательный, поскольку сильно ограничивает наши возможности.

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

• создать новый типаж Primitive, реализованный только для "обычных" натуральных чисел, создаваемых через макрос;
• реализовать <N: Primitive> StaticallyProvable for Equiv<N, N>. Так как Add не является Primitive, и компилятор это может проверить, в этом случае конфликта не будет.

Метод, в принципе, хороший, однако он всё равно ограничивает наши возможности. Так, Equiv<Add<N1, N2>, Add<N1, N2>> в этом случае является статически недоказуемым, и добавить соответствующую реализацию мы в явном виде не можем — она точно так же будет конфликтовать с доказательством симметричности сложения.

Вариант третий, который в итоге и был реализован, требует от нас снова вернуться в qd_core.

qd_core: доказательства по правилам

Всё, что нам нужно, — немного скорректировать определение типажа StaticallyProvable:

pub trait StaticallyProvable<Rule> where Self: Sized {
    fn proof() -> Self;
    fn prove_by_rule(_: Rule) -> Self {
        Self::proof()
    }
}

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

Добавим заодно общую реализацию для Deducible:

impl<Rule, T: StaticallyProvable<Rule>> Deducible<Rule> for T {
    fn deduce(_: Rule) -> Self {
        Self::proof()
    }
}

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

qd_nat: свойства чисел и операций, дубль 2

Рефлексивность равенства теперь будет описана так:

pub struct Refl;
impl<N: Nat> StaticallyProvable<Refl> for Equiv<N, N> {
    fn proof() -> Self {
        Self::refl()
    }
}

Единственное, что поменялось, — мы добавили новый тип Refl и использовали его в качестве параметра типажа.

Для симметричности сложения, в свою очередь, используется другой параметр:

pub struct Symmetric;
impl<N1: Nat, N2: Nat> StaticallyProvable<Symmetric> for Equiv<Add<N1, N2>, Add<N2, N1>> {
    fn proof() -> Self {
        Self(PhantomData)
    }
}

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

Абсолютно аналогично мы можем ввести понятие об ассоциативности сложения:

pub struct Associative;
impl<N1: Nat, N2: Nat, N3: Nat> StaticallyProvable<Associative>
    for Equiv<Add<N1, Add<N2, N3>>, Add<Add<N1, N2>, N3>>
{
    fn proof() -> Self {
        Self(PhantomData)
    }
}

Добавим ещё небольшую функцию для создания объектов типа Add:

impl<N1: Nat, N2: Nat> Add<N1, N2> {
    pub fn sum(_: N1, _: N2) -> Self {
        Self::get()
    }
}

И, используя три полученных доказательства и подготовленную ранее функцию accepts_pair, напишем вот такой тест:

#[test]
fn proved() {
    use qd_nat::with_n;
    use qd_core::StaticallyProvable;

    let n1 = with_n!(N::from_usize(1).unwrap());
    // Равенство рефлексивно - n1 == n1.
    accepts_pair(n1, n1, Equiv::proof());

    let n2 = with_n!(N::from_usize(2).unwrap());

    // Убеждаемся, что рефлексивность равенства используется и для "сложных" чисел.
    accepts_pair(Add::sum(n1, n2), Add::sum(n1, n2), Equiv::proof());
    // Сложение симметрично = n1 + n2 == n2 + n1.
    accepts_pair(Add::sum(n1, n2), Add::sum(n2, n1), Equiv::proof());

    let n3 = with_n!(N::from_usize(3).unwrap());
    // Сложение ассоциативно: n1 + (n2 + n3) == (n1 + n2) + n3.
    accepts_pair(Add::sum(n1, Add::sum(n2, n3)), Add::sum(Add::sum(n1, n2), n3), Equiv::proof());
}

Обратите внимание, что в этой функции нет ни одного ветвления (за исключением неизбежных unwrap-ов при создании чисел). Нам не требуется ни одной проверки на равенство: они все выражаются через заданные нами правила.

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

#[test]
fn proved() {
    // пропуск
    accepts_pair(
        Add::sum(Add::sum(n1, n2), n3),
        Add::sum(n1, Add::sum(n2, n3)),
        Equiv::deduce(Equiv::proof()),
    );
}

А вот в этом случае требуется не только построить цепочку, но и явно указать одно из правил:

#[test]
fn proved() {
    // пропуск
    accepts_pair(
        Add::sum(n1, Add::sum(n2, n3)),
        Add::sum(n3, Add::sum(n1, n2)),
        Equiv::deduce((
            Equiv::prove_by_rule(Associative),
            Equiv::proof()
        )),
    );
}

Сама цепочка строится следующим образом:

• Во втором аргументе меняем местами порядок слагаемых. Этот шаг Rust может вывести сам.
• Приравниваем первый аргумент к полученному результату. Здесь компилятору потребовалась помощь — и мы её предоставили, явно указав, что нам надо воспользоваться ассоциативностью сложения.
• Из двух полученных ранее равенств выводим третье, искомое.

Тем не менее, в рантайме никаких проверок по-прежнему нет.

qd_vect: конкатенация со статической проверкой

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

// Вспомогательная функция - сравнивает два вектора доказанно равной длины
fn equiv<T: Clone + PartialEq<T>, N: Nat>(first: Vect<T, N>, second: Vect<T, N>) -> bool {
    first
        .freeze()
        .iter()
        .zip(second.freeze())
        .all(|(i1, i2)| i1 == i2)
}

#[test]
fn concats() {
    let (_, v1) = vect!(vec![1]);
    let (n2, v2) = vect!(vec![2, 3]);

    // Сначала просто сконкатенируем два вектора в прямом и обратном порядке.
    let v12 = v1.clone().concat(v2.clone());
    let v21 = v2.clone().concat(v1.clone());

    // Их длина будет гарантированно совпадать - доказательство доступно статически.
    let sum = zip_sum(v12, v21.retag(Equiv::proof()));
    assert_eq!(sum.into_native(), vec![3, 5, 4]);

    let (n3, v3) = vect!(vec![4, 5]);
    let v12 = v1.clone().concat(v2);
    let v13 = v1.concat(v3);

    // Проверим, что v2 и v3 имеют равную длину
    match Equiv::try_prove_for(n2, n3) {
        Some(proof) => {
            // ...а если это так, значит, мы можем добавлять хоть v2, хоть v3 -
            // результирующая длина будет одинаковой, и это опять-таки известно статически
            let sum = zip_sum(v12.retag(Equiv::deduce(proof)), v13);
            assert_eq!(sum.into_native(), vec![2, 6, 8]);
        }
        None => panic!("2 != 2, WTF?"),
    }

    // Ну и, наконец, тест на ассоциативность
    // Первый вариант: конкатенация вида ((v1, v2), v3)
    let v_12_3 = v1.clone().concat(v2.clone()).concat(v3.clone());
    // Второй вариант: конкатенация вида (v1, (v2, v3))
    let v_1_23 = v1.concat(v2.concat(v3));
    // Результат должен быть одинаков - и по длине, и по содержанию
    assert!(equiv(v_1_23.retag(Equiv::proof()), v_12_3));
}

Заключение

Разумеется, ни о каком практическом приложении этих материалов речи не идёт — по крайней мере, в нынешнем виде. Тем не менее, разобраться в этом было интересно, и, возможно, какие-то из показанных здесь методов работы с типами окажутся полезными и в прикладных задачах.