дыбр и типы

Давненько я тут ничего не писал. Помнится, некоторые ЖЖ-френды после переезда в Америку или Европу с работой в больших компаниях начинали писать в ЖЖ все реже, а потом и вовсе переставали. Мне еще было любопытно, почему так получается и что с ними. Этого я так и не узнал, но и сам чуть не стал таким же. Может, потому что на работе довольно интересный проект, о котором много не расскажешь, а на другие занятия либо остается мало времени, либо хобби-проекты сейчас получаются довольно длинные, преждевременно о них рассказывать не хочется, а созревают не быстро. Может, еще потому что больше общения стало в телеграм-чатах, с телефона, сюда стал реже заглядывать.

Продолжаю работать в той же компании, для которой приехал в Лондон, но в офисе не был с марта 2020-го, мы с той поры все на удаленке. Жена нашла работу и в своем офисе не была вообще ни разу, ей прислали технику домой, так и работает.

Проект мой на работе далеко не опен-сорсный, но совсем уж секретным тоже не является, на конференциях про него немного рассказывали и упоминали не раз. Делаем мы свой небольшой in-house функциональный язык программирования, чтобы отойти от традиционных для финансового мира Экселя с SQL-ем и выражать все в коде, с гитом, тестами, код ревью и прочими полезными практиками.
Изначально язык был динамически типизирован, просто потому что так было проще сделать. Но потом решили двигаться к статическим типам, и мне довелось заняться навешиванием системы типов, тайпчекинга и вывода типов на существующий недотипизированный язык. К счастью, там все иммутабельное и без ООП (кроме нативных объектов и их полей/методов), монстр а-ля TypeScript не нужен. Поскольку уже сколько-то реального кода на нем было написано без типов, хотелось сделать хороший вывод типов, чтобы не добавлять аннотации в каждую функцию, чтобы можно было мигрировать с минимальными правками. И хотелось сохранить duck typing, но проверять его статически, т.е. нужна структурная типизация. Чтоб без лишних аннотаций можно было структуру с десятком полей передать в функцию, которой нужны лишь парочка из них. Ну и гетерогенные коллекции мне хотелось тоже разрешить, т.е. нужны union types. Перефразируя местного поэта, if you can't infer sum types and structs then I don't wanna hear no chat about typing.
Думал быстро управиться, делов-то. Начал с доволько наивного Хиндли-Милнера, но быстро наткнулся на проблемы. Вспомнил про окамловские polymorphic variants и объекты, которые казалось бы так близки к тому, что мне нужно, особенно если их использовать не только для алгебраиков, но более простые типы туда засунуть, получив union types. Сделал, но опять уткнулся в проблемы.
Напомню, что polymorphic variants в окамле это такие алгебраики, которые не нужно предварительно описывать, он сам выводит где какой набор строится или ожидается. Так, например, для

let f = function `A -> `B | `B -> `A

let g x = [x; f x; `B]

let lst = [`A; f `A; `C]

компилятор окамла выведет сам, что f принимает `A | `B и возвращает `A | `B,
функция g принимает `A | `B и возвращает список из `A | `B,
а lst это список из `A | `B | `C.

Но стоит нам попытаться добавить `C в результат g:

let g x = [x; f x; `B; `C]

то тут окамл уже ругается и не пущает. Потому что недалеко ушел от ХМ, для каждой типо-переменной он отслеживает множества верхних и нижних границ (upper & lower bounds), но когда из значений мы строим список, все элементы списка должны иметь один тип, их верхние и нижние границы нужным образом пересекаются/объединяются, в итоге из-за того, что x передается в f, у него верхняя граница `A | `B (ничего другого f не принимает), и эта верхняя граница влияет на все другие элементы списка, потому `B туда поместить можно, а `C уже нельзя.
Пошел учиться дальше, видел HM(X) Одерского, где про сабтайпинг умеют, но не разобрался.
Зато нашел работы Долана про Algebraic Subtyping и вдохновился. Главная идея там - отказаться в тайпчекере от уравнений про равенства типов, и везде использовать неравенства: "А подтип Б".
Тогда в списке могут быть значения с разными и даже несовместимыми верхними границами, и это ок, т.к. результирующий тип элементов списка отличен от каждого из них и связан с ними неравенствами, он для них супертип. (`A | `B это подтип `A | `B | `C, и `C это подтип `A | `B | `C).
Нагенерить неравенств-то сравнительно несложно (хотя местами было о чем подумать, все же язык у нас отличается от тех, что в статьях), а вот решить их - уже сложнее. Подход к решению со всякими бисубституциями и автоматами у Долана мне тогда показался каким-то сложным, стал делать свое решение, думал, получится проще. В итоге, правда, если прищуриться, те же бисубституции и получились, но без захода в конечные автоматы. Потом уже в 20-м году вышли статьи про CubiML и Simple-sub, там тоже довольно похожие на мое решения, они может и выглядят разными, а суть похожа.
Некоторое время назад я делал презентацию о том, что получилось, там видно в целом, как язык выглядит и как туда типы добавляются, и есть пример, как тайпчекер думает, выводя типы для

foo(o) => {
  a = o.fred |> toStr
  b = o.toto
  a = a.length
  in if b then a else o.fred + 2
}

Еще скриншоты REPL'a с примерами про вывод типов и сочетание структурной и номинальной типизации. Типы можно описывать прямо в репле, и в отличие от всяких тайпскриптов типы параметров функций тоже выводятся, насколько возможно, вывод не локальный.
( Read more... )

Things that make me happy

За пару недель до самого первого локдауна в прошлом году я себе купил игровой ноут для работы из дома, потому что в нем было 32 гига памяти, а мне как раз было столько нужно, чтобы собирать рабочий проект. Все потому что Уолтер Брайт в свое время ловко ускорил компилятор D за счет того, что аллокация памяти делается самым простым и быстрым способом, а деаллокация не делается вовсе, и GC не включен тоже. Т.е. компилятор просто жрет память, надеясь, что быстро завершится и слишком много не выжрет. Потом мы задействовали чуть другую систему сборки, которая умеет собирать разные части параллельно, но 32 гигов для этого уже было маловато, поэтому мне приходилось компилить в один поток. К тому же на ноуте у меня была предустановленная винда, и там мы используем LDC (LLVM-based D compiler), который работает медленнее референсного DMD (который компилит быстро, но хуже). В общем, все вроде бы было хорошо, пока я не осознал, что можно лучше. Большой подстольный ящик брать домой не хотелось, вспомнил, что есть же сейчас такие маленькие коробочки, например Intel NUC. Раздобыл себе такой, размером меньше ладони:

Там внутри 64 ГБ памяти, быстрый большой SSD и i7 10-го поколения (сейчас есть и новее, но их надо долго ждать) с 12 логическими ядрами. До чего дошел прогресс!
Снес оттудова винду, поставил свежий Manjaro Linux, который с одной стороны Arch-based и потому не протухает, а с другой стороны не требует PhD по установке и настройке. Раньше у меня линуксы были с KDE и Cinnamon'ом, надоели, тут поставил вариант с GNOME 40. Такая красота!




Работает все идеально, видимо, год линукса на десктопе уже давно был. Комбинация нескольких изменений (Win -> Lin, 32 -> 64 GB, LDC -> DMD, single-threaded -> parallel) дала ускорение сборки на порядок. Теперь если после переключения ветки надо с нуля собрать, это делается за пару минут вместо былых 15-20. Щастье!
Параллельная сборка, конечно, все равно всю память выедает, выглядит это весело:

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