Имитируем функционал зависимых типов в системе типов Rust06.06.2020 18:17

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pub struct Vect(Vec);

Обратите внимание, что внутреннее поле структуры объявлено приватным — ни у кого извне права напрямую что-то сделать с этим стандартным вектором нет, даже если у них есть изменяемая ссылка на 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 DependentInnerOperate for T {}

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

impl DependentInner for Vec {
    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. Окей, действуем:

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

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

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

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

impl DependentVec> for Vect {
    fn try_unify>>(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(first: &T, second: &T) -> T
where
    Item: AddAssign + Clone,
    T: DependentVec> {
    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 DependentVec> for Vect {
    fn inner(&self) -> &Vec {
        &self.0
    }
    fn map_ref(&self, f: impl FnOnce(&mut  as DependentInner>::Frozen)) -> Self {
        let mut inner = self.inner().clone();
        f(inner.freeze());
        Self(inner)
    }
    fn consume_ref(&self, f: impl FnOnce(&mut  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
}А теперь - сам `Nat`. Заодно мы немного расширим API наших натуральных чисел, а именно:
- добавим возможность создавать объект, имея только тип, но не значение - это может пригодиться в обобщённом коде (хотя в нынешнем проекте эти методы не используются, но удалить их всё равно рука не поднялась);
- добавим возможность получить число, соответствующее типу, не имея самого объекта - это нам пригодится чуть позже.

Собственно:
```rust
pub trait Nat: Sized + NatInner + Clone + Copy {
    fn get_usize() -> Option;
    fn as_usize(self) -> usize;
    fn from_usize(s: usize) -> Result;
    fn get() -> Self;
    fn try_get() -> Option;
}

#[macro_export]
macro_rules! with_n {
    ($($inner:tt)*) => {{
        // пропуск
        impl $crate::Nat for N {
            fn get_usize() -> Option {
                HOLDER.read()
            }
            fn as_usize(self) -> usize {
                // Этот вызов никогда не должен проваливаться,
                // т.к. раз объект создан, Holder должен быть уже инициализирован
                HOLDER.read().unwrap();
            }
            fn from_usize(s: usize) -> Result {
                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::get_usize().map(|_| Self)
            }
        }
        $($inner)*
    }};
}

impl DependentOperate for T {}

Вскоре, однако, стало ясно, что наличие нескольких отдельных типажей только создаёт дополнительные сложности, никак при этом не упрощая нам жизнь. Мы можем избавиться от них, переместив тип `Frozen` непосредственно в типаж `Dependent` и устранив автоматически реализованные методы:
```rust
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(PhantomData<(T1, T2)>);

impl Equiv {
    pub fn rev(self) -> Equiv {
        Equiv(PhantomData)
    }
}

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

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

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

pub struct Vect(Vec, PhantomData);
impl Dependent for Vect {
    type Native = Vec;
    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>(iter: I) -> (N, Vect) {
    let inner: Vec<_> = iter.into_iter().collect();
    (N::from_usize(inner.len()), Vect(inner, PhantomData))
}

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

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

fn zip_sum, N: Nat>(
    first: Vect,
    second: Vect,
) -> Vect {
    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)`
  --> ${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)`, where the type parameter `N` is specified
   | 
  ::: ${MODULE}/src/lib.rs:28:32
   |
28 | pub fn collect>(iter: I) -> (N, Vect) {
   |                                --- required by this bound in `collect`
   |
   = note: cannot satisfy `_: Nat`
help: consider specifying the type arguments in the function call
   |
7  |     let _ = collect::(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 {
        // skipped
    }
}

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

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

Собственно:

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

#[macro_export]
macro_rules! with_n {
    ($($inner:tt)*) => {{
        // пропуск
        impl $crate::Nat for N {
            fn get_usize() -> Option {
                HOLDER.read()
            }
            fn as_usize(self) -> usize {
                // Этот вызов никогда не должен проваливаться,
                // т.к. раз объект создан, Holder должен быть уже инициализирован
                HOLDER.read().unwrap();
            }
            fn from_usize(s: usize) -> Result {
                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::get_usize().map(|_| Self)
            }
        }
        $($inner)*
    }};
}

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

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

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

impl Equiv {
    pub fn check() -> Option {
        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::try_create()
    }
}

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

fn accepts_pair(n1: N1, n2: N2, _proof: Equiv) {
    // этот 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.

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

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

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

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

impl Vect {
    pub fn retag(self, _proof: Equiv) -> Vect {
        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(usize, PhantomData);

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

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

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

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

pub struct IterUntil(usize, PhantomData);
impl Iterator for IterUntil {
    type Item = Fin;
    fn next(&mut self) -> Option> {
        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 Iterator for IterUntil {
    type Item = Fin;
    fn next(&mut self) -> Option> {
        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 Iterator for IterUntil {
    // пропуск
    #[inline]
    fn nth(&mut self, n: usize) -> Option> {
        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 {
        IterUntil(0, PhantomData)
    }
    fn iter_until_this(self) -> IterUntil {
        Self::iter_until()
    }
}
impl NatIterUntil for N {}

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

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

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

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

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

impl Index> for Vect {
    type Output = Item;
    fn index(&self, index: Fin) -> &Item {
        // Безопасность: Fin::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 NatInner for T {}
impl Nat for T {
    fn get_usize() -> Option {
        Some(Self::USIZE)
    }
    fn as_usize(self) -> usize {
        Self::USIZE
    }
    fn from_usize(s: usize) -> Result {
        if s == Self::USIZE {
            Ok(Self::default())
        } else {
            Err(NatStoreError::AlreadyStored(Self::USIZE, s))
        }
    }
    fn get() -> Self {
        Self::default()
    }
    fn try_get() -> Option {
        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). Это, безусловно, интересно, но мы можем сделать больше —, а именно, мы можем организовать арифметику для таких чисел.

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

© Habrahabr.ru