Про то как мне понравилось 3D-моделирование всё-таки позже расскажу, спать пора 🙂

До этого я моделировал максимум карты для Counter-Strike в далёком детстве и какие-то домики в SketchUp, не помню уже зачем.

А тут познакомился с параметрическим моделированием, что выглядит как очень приятная магия.

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

С каждым ограничением число степеней свободы уменьшается и двигая что-нибудь видим, что ещё нужно ограничить. Пока не получим зелёненькое Fully constrained. Меняя размеры/углы оно автоматически перестраивается как нужно.

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

Если бы интерфейсы верстались такими штуками, то жизнь бы стала налаживаться :)

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

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

Реализовал первую поддержку и json, и flatbuffers параметров запроса. Теперь могу формализировать один из хаков для победы над лайфтаймами. Совсем простенький, но в начале не сразу было очевидно.

Кейс такой: нужно читать и json, и flatbuffers. Очевидно, для этого нужно создавать owned-структуры и хотелось бы создать третью, которая будет ссылаться на одну из структур (json/flatbuffers). Если просто втупую в разных ветках if'ов попарсить и сделать эту третью структуру — то борроу чекер обоснованно скажет, что структуры будут уничтожены в блоках if.

Но нет никаких проблем хранить эти структуры снаружи в Option. Сделал себе функцию даже:

pub fn store_in_option<T>(opt: &mut Option<T>, value: T) -> &T {
    *opt = Some(value);
    opt.as_ref().expect("just stored")
}

Тогда снаружи делаем let mut some_value = None на все значения которые нам нужно хранить во всех ветках, в ветках спокойно создаём их, пересохраняем let value = store_in_option(&mut some_value, value), свободно пользуемся полученной ссылкой, лайфтайм у неё будет как у some_value.

Раньше тоже так делал, но как-то не так сильно в глаза бросался приём.

#rust

Попал вчера в засаду. У меня был трейт:

trait FlatbuffersType<'fbb>: flatbuffers::Follow<'fbb> + flatbuffers::Verifiable + 'fbb {}

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

И вдруг осознал, что мне всё не так нужно. Точнее что когда я сериализатор превращаю в OwnedSerialized<'fbb, F: FlatBuffersType<'fbb>> мне не нужен этот 'fbb больше, а нужен 'static, т.к. валидация сериализации уже не нужна, а валидность структур которые мы читаем легко получается т.к. у нас есть метод fn data<'a>(&'a self) -> SomeFlatbuffersType<'a> и уже 'a гарантирует что мы не потеряем структуру в которой лежит буффер.

Тупил-тупил, спрашивал гпт и никак не понял как мне написать функцию вида fn into_owned<'a, T: SomeTrait<'a>> -> impl SomeTrait<'static>, где реализация SomeTrait результата была бы той же, что и T, но с другим лайфтаймом. Скорее всего никак и нельзя.

Пришлось поплакать и сделать:

pub trait FlatbuffersGenericType {
    type FlatType<'a>: FlatbuffersType<'a>;
    fn name() -> &'static str;
}

Затем параметризировал все свои Serializer, deserialize(), OwnedSerialized просто этим F: FlatbuffersGenericType, а там где нужны были лайфтаймы — делал F::FlatType<'a> и всё сошлось, так у OwnedSerialized лайфтайма никакого нет, а у Serializer есть <'fbb, F: FlatbuffersGenericType> и все методы которые принимают FlatType зависят от 'fbb.

Но как-то это нехорошо, пришлось слишком много кода переделывать, плюс теперь необходима кодогенерация. Я не могу реализовать этот FlatbuffersGenericType для всех типов которые у меня есть (даже если бы там не было метода `name()`). У прошлого трейта всё было просто:

impl<'fbb, T: Follow<'fbb> + Verifiable + 'fbb> FlatbuffersType<'fbb> for T {}

(по сути мой трейт был просто алиасом). А теперь мне нужен макрос и вручную добавлять реализации для каждой flatbuffers-структуры которая у меня есть:

macro_rules! flatbuffers_generic {
    ($name:ident, $proto_name:ident) => {
        pub struct $proto_name;
        impl ::diffbelt_protos::FlatbuffersGenericType for $proto_name {
            type FlatType<'a> = $name<'a>;
            fn name() -> &'static str {
                stringify!($name)
            }
        }
    };
}

flatbuffers_generic!(Request, RequestProto);
flatbuffers_generic!(Response, ResponseProto);
flatbuffers_generic!(CreateCollectionRequest, CreateCollectionRequestProto);
// ...

Не сильно прям страшно, кажется что я могу или flatc который генерирует код парсеров как-нибудь подкрутить (пока не смотрел в его настройки), либо, кхм, в build.rs после генерации парсеров распарсить их код, найти реализации Follow для структур и сгенерировать ещё своего кода, который добавит этих моих реализаций. Но что-то в этой колокольне явно не так, может на неделе пойду куда-нибудь ишью создам и послушаю, что про это думают другие. Может быть вообще есть какой-то хитрый способ, с которым можно было бы обойтись малой кровью.

#rust

Ну нет, пожалуйста, не надо https://paulbutler.org/2025/smuggling-arbitrary-data-through-an-emoji/

Пришлось немного пооптимизировать, чтобы wasm-модуль компилировался только один раз, забодало ждать секунд десять, пока тесты прогонятся (сейчас всё равно две секунды в дебаг-сборке, пробовал даже [profile.dev.package."*"] opt-level = 3, почему-то не помогает). Плюс добавил подсчёт времени на прогон кейса, красивое:

Loaded wasm file example in 137.924947ms
[ OK ] transforms.parsed_lines_1d.map > basic, 2.251365ms
[ OK ] transforms.parsed_lines_1d.map > empty, 59.34µs
[ OK ] transforms.parse_lines.map_filter > with props and no extras, 3.084386ms
[ OK ] transforms.parse_lines.map_filter > with props and one extra, 220.157µs
[ OK ] transforms.parse_lines.map_filter > with props and two extras, 146.782µs
[ OK ] transforms.parse_lines.map_filter > with no props and no extras, 127.173µs
[ OK ] transforms.parse_lines.map_filter > with no props and two extras, 134.486µs
[ OK ] transforms.parse_lines.map_filter > not matches start, 72.015µs
[ OK ] transforms.parse_lines.map_filter > with stack extra, 179.017µs
[ OK ] transforms.parsed_lines_1d.reduce > basic, 442.891µs
[ OK ] transforms.parsed_lines_1d.merge_accumulators > basic, 472.15µs
[ OK ] transforms.parsed_lines_1d.apply > basic, 350.193µs
[ OK ] transforms.parsed_lines_1d.apply > empty, 58.245µs
[ OK ] transforms.parsed_lines_1d.apply > mismatched count, 59.165µs
[ OK ] transforms.parsed_lines_1d.apply > negative count, 59.606µs
[ OK ] transforms.parsed_lines_1d.apply > mismatched negative count, 57.78µs
[ OK ] transforms.updateMs_1d_intermediate.map_filter > should not match, 800.988µs
[ OK ] transforms.updateMs_1d_intermediate.map_filter > should match, 263.128µs
[ OK ] transforms.parsed_lines_1d.initial_accumulator > empty, 82.186µs
[ OK ] transforms.parsed_lines_1d.initial_accumulator > few, 445.984µs

Никогда не мерял ещё скорость запуска какого-либо кода в микросекундах 😃

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

#diffbelt

Посмотрю как совсем нечего делать будет — https://www.youtube.com/watch?v=ArQNyOU1hyE

Насколько я понял по интернету — существующие хеш-таблицы слишком хороши из-за simd-приседаний, которые умеют сразу на кучу бакетов смотреть и они могут спокойно класть на теорию которую прокачали в видео выше.

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

Прокачал свой OwnedAlignedBytes этот, радуюсь RAII или около того. До этого передавал из васма через ffi указатель на структуру в которой лежат кишки из которых можно собрать Vec<u8> (указатель на него, капасити и длина), хост знал сколько байт нужно записать, вызывал у васма функцию которой передавал указатель на эту структуру, оно там в памяти васма восстанавливало вектор, подкручивало на сколько нужно capacity, деконструировало вектор обратно в эту структуру, хост записывал байты и менял length у структуры, передавало васму управление и он мог восстановить вектор в котором находятся нужные байты. После чего возможно нужно было двигать байты, чтобы выровнять для парсинга flatbuffers.

Теперь так: у OwnedAlignedBytes есть метод unsafe fn write_bytes(&mut self, len: usize) -> WriteAlignedBytes<'_, ALIGN>. У структуры WriteAlignedBytes два метода — as_mut(&mut self) -> &mut [u8], который выдаёт слайс размера len, который берёт из вектора который лежит в OwnedAlignedBytes и capacity которого расширили в write_bytes(). Функция unsafe, т.к. мы должны требовать что весь слайс будет записан, т.к. в дропе WriteAlignedBytes мы вызываем ансейф метод вектора set_len(), требующий чтобы байты были проинициализированы.

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

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

Плюс есть ещё другая проблема — когда-нибудь нужно будет отказаться от Vec<u8> внутри, т.к. я не могу писать внутрь него байты кусками, т.к. после реаллокации весь мой префикс дающий выравнивание может оказаться неправильным. В итоге, например, при чтении байт из http-запроса они сначала пишутся в голый Vec и затем мы всё ещё двигаем байты, создавая OwnedAlignedBytes. Было бы хорошо самому управлять реаллокацией, чтобы при переносе в новую память могли сразу скопировать всё правильно. Но до такого тоже далеко (да и найдутся более важные вещи и места сильно более профитных оптимизаций).

#rust

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

Штука довольно прикольно выглядит. Я задумывал это как возможность писать интеграционные тесты, но по сути если назвать чуть иначе, то там уже практически можно демонов обработки этих потоков данных делать. Там уже доступен запрос «жди пока у коллекции Х не изменится id поколения», есть возможность попросить запустить трансформацию. Т.е. уже можно сделать цикл который следит за тем, что данные были изменены и чтобы оно пересчитало их в следующую коллекцию. Параллельно можно запустить ещё таких штук, которые будут следить за изменениями следующих коллекций и перекладывать дальше. Это и так будет отдельной командой (и по задумке оно будет умным, видя что таких команд запущено больше одной на разных хостах и будет делить работу в тех трансформациях где это возможно), но мне нравится, что это уже физически реализуемо.

Ну и на самом деле это полукостыль, потому что такой агент на самом деле должен выполняться не внутри васма, а быть самостоятельным бинарником, который просто ходит в апи (чтобы он мог и сайд-эффекты относительно внешнего мира совершать). Но сейчас для тестирования всего этого васм-взаимодействия полезнее такой вариант, уже отловил пачку заляп ансейфных (благо в дебаге оно даже в unchecked-операциях обложено проверками на валидность и довольно понятно говорит что пошло не так; а без unsafe там не получится, т.к. всё общение идёт через `extern "C"`).

Вряд ли на этой неделе закончу с proof-of-concept потокового вычисления перцентилей, там нужно разбираться в мёртвом коде трёхлетней давности. Но очень хочется доделать, даже если затем просто выкину. Выкину потому что не так уж они и нужны скорее всего. Ко мне пришла довольно логичная мысль, что для такого кейса использования проще использовать мою балалайку как source of truth относительно данных и затем имея механизмы обеспечения консистентных преобразований наладить синхронизацию части лежащих у меня данных с каким-нибудь clickhouse, где производить вычисления, где они определённо будут сильно быстрее из-за правильной укладки данных, а затем выдавать результаты в итоговые коллекции, где их заберёт тот кому они нужны. А всё что я делаю просто даст возможность всегда знать, актуальны ли данные лежащие в итоговой коллекции, насколько они отстают от исходных, иметь гарантии консистентности входа и выхода.

#diffbelt

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

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

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

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

А теперь plot twist — в конце месяца пользователь получает отчёт, где машина, судя по пробегу, съездила на луну, потому что GPS половину месяца уносило непонятно куда. И определение поездок он криво настроил. В итоге он берёт, меняет настройки, удаляет/редактирует кривые сообщения, просит переделать отчёт. Здесь мы ловим проблему инвалидации кеша. Мы точно предпросчитывали какие-то данные, чтобы строить отчёты быстрее, т.к. люди жаловались, что они слишком долгие. Какие из этих данных нужно выбросить?

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

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

Вот что-то такое я хочу. Посмотрим, в общем, как пойдёт и дойдёт ли куда-нибудь 🙂

#diffbelt

Недавно обнаружил, что use можно писать не только в начале файла, но и прям внутри функций.

RustRover почему-то очень плохо в no_std крейте включённом в workspace работает и постоянно то вместо alloc импортирует из std, то extern crate core мне в lib.rs добавляет по четыре штуки. Так вот и добавляю руками импорты, чтобы не бесило.

Как написал, понял, что нужно просто свой макрос-обёртку сделать, который сам внутри себя ::alloc::format!() дёрнет, так жизнь попроще станет. А я сижу мучаюсь :)

#rust

Написал что-то около 45% реализации этой агрегации злополучной, аккумуляторы сериализируются и десериализируются, ключи вокруг старых перцентилей почти получаются (пока todo!() вставил, нужно посмотреть на порядок ключей слева/справа, а то подзабыл, а в реализацию влом смотреть, давно там не был уже).

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

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

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

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

#diffbelt

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

Смотрите, есть всего шесть основных семейств типов:

◾️ 0 — пустой тип без значений, так же известный как ложь, void, bottom (⊥)
◾️ 1 — тип с единственным значением *
◾️ A + B — тип-сумма двух типов, значения которого принимают либо левый тип, либо правый. Например, тип 1 + 1 будет по сути boolean'ом, где левый тип будет false, а правый true (или наоборот). А тип A + 0 будет содержать только левые значения типа A.
◾️ Σ — тип пар. В простейшем случае это (A, B), где имеются значения обоих типов. В общем случае тип B может зависеть от значения типа A. Т.е. например, может быть тип (1 + 1, f), где f принимает значение 1 + 1 и если оно левое, то возвращает один тип, а если правое — то другой. Такие типы называются зависимыми.
◾️ Π — тип функций/стрелок. Его значениями являются лямбды и он похож на предыдущий тип. В простом случае выглядит как A → B, принимает значение типа A, возвращает значение типа B. В общем — тип B может зависеть от значения типа A. Т.е. например, если бы у нас был тип чисел (мы можем, например, построить u32 вложив много раз пары друг в друга вида (1 + 1, (1 + 1, 1 + 1, ...)) и интерпретировать их как биты), то может быть тип, который для чисел меньше N возвращает значение одного типа, а для остальных другого (хочется сразу рассказать, зачем это нужно, но когда-нибудь потом).
◾️ U — universum, тип значения которого являются типами. The HoTT Book говорит, что сам U не является значением этого типа, а они вкладываются друг в друга, т.е. есть бесконечное количество этих U-типов, где U0 содержит типы, сам U0 принадлежит U1, U1 в U2 и так далее. Иначе если его положить самого в себя всё разваливается.

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

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

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

#triangle

Это было введение, дальше собственно что хотел сохранить. Можно делать свои типы, например, вот тип натуральных чисел:

Nat = 1 + Nat

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

G = G → 0

Я легко могу описать его значение: (λ f . f f). Это функция, которая принимает саму себя, вызывает её и передаёт её же в аргументы. Видите тип 0 в результате? Мы не должны иметь возможности получать элементы этого типа по его определению (в нём нет элементов), но эта функция его «возвращает». Что плохо, т.к. принцип индукции (объяснения этого мы опустим) выглядит как 0 → T для любого T. Т.е. получив ложь, мы можем получать значение любых типов, что полностью разрушает всю нашу теорию.

Этому нужно как-то противодействовать, давайте введём понятие рекуррентности типа:

◾️ Тип R рекуррентен относительно G если показывает на него ( R = Rec(G) ). Жидкое описание, Rec(G) читать как «от типа R есть цепочка алиасов, которые если развернуть, то встретится тип G в случаях описанных ниже». Не знаю пока, как это нормально описать
◾️ Лежит внутри пары ( R = (Rec(G), ?), R = (?, Rec(G)) )
◾️ Содержится в обоих сторонах суммы ( R = Rec(G) + Rec(G) )
◾️ Может быть возвращён из функции ( R = ? → Rec(G) ), кроме случая когда аргумент функции это 0 ( R = 0 → Rec(G) это валидный тип )

Далее с этим так себе определённым понятием мы запрещаем принимать эти рекуррентные типы в аргументах функций. Т.е. нельзя делать типы R = Rec(G) -> ?, где G = Rec(R).

Самое веселье начинается вот с такими определениями:

A = 1 + B
B = 1 + A

Это валидный тип, т.к. явно видно, что рекурсивные типы не содержатся в обоих сторонах суммы. Да и функциями тут не пахнет. Даже если сделаем B = (B -> 0) + A — хуже не станет, A не рекуррентен относительно B, т.к. имеет левый вариант суммы без него. А вот следующий тип невалидный:

A = (B, 1 + 1)
B = (1, A → 0)

У B будет значение (*, (((_, f), _) => f (*, f))) (простите, у меня нотации лямбд всегда разные, это псевдокод). Функция A → 0 достаёт из левой стороны пары в A функцию самой себя, передаёт туда легко собираемое значение B и получаем бесконечную рекурсию и снова ломаем теорию.

#triangle

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

А хотелось бы иметь такие функции в качестве аксиом, чтобы можно было иметь значения которые описывают типы, чтобы стало понятнее, как должен выглядеть тайпчекер этого добра. Хочется когда-нибудь сделать свой Coq/Adga/Idris, но непонятно сколько времени на это нужно закопать и вот мозг перегружается каждый раз, как пытаюсь сделать даже маленький подходик.

Type Theory should eat itself (but so far, it’s too big to swallow).

#triangle

Прикольно, штуковина натравила LLM'ок на репозиторий, потупила в код и накидала высокоуровневых объяснений что там происходит и как оно устроено. И даже картинок нарисовало. Technolojia, однако.

https://deepwiki.com/anfivewer/diffbelt