buka

Об универсальных языках программирования/моделирования 1

Ребята пишут про какой-то паттерн матчинг настоящий :-)
Про итеграцию и то, что это было в лиспах (ну не в лиспах, а в ACL2 — это все же не лисп). Ну и понятное дело все это пишут ебанаты, код которых так воняет по всему интернету что даже из гитхаба его удаляют :-) Невозможно понять как работает паттерн мачинг, если вы не поняли как раотает оператор J. Я написал за свою жизнь около 15 языков. И поверьте любые ваши попытки написать свой язык, в котором нет зависимых типов и бесконечного счетного количества вселенных — навсегда остануться костылями, которые никогда не будут восприниматься более-менее здоровыми психически людьми как нечно стоящее. Потратьте хотябы несколько лет в медитации, чтобы понять что А) мы (Групоид Инфинити) не занимается хуйней и Б) вы занимаетесь хуйней.

Originally posted by justy_tylor at Об универсальных языках программирования/моделирования 1
В начале века я ещё считал, что прогресс технологий работы с информацией сильно сдерживается существующими языками программирования, но достаточно заменить C++ чем-то более развитым по части функциональщины и метапрограммирования (но сохраняющим возможность генерации оптимального нативного кода), чтобы стало легко и удобно разрабатывать продукты любой сложности, уделяя внимание только проблемам предметной области, но не ограничениям предыдущего поколения инструментов. Был юный и тупой.

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

Можно сделать язык с полноценной реализацией pattern matching (а не как принято сейчас). С паттернами и комбинаторами в качестве первоклассных сущностей языка. И это уже польза. Однако.

Для определённых типов данных эффективнее создание индексов вместо полного перебора веток. Появляется выбор, либо через удобный pattern matching, либо через ручное решение с индексами. Ложный выбор. Средства метапрограммирования языка должны позволять создание подобных индексов в pattern matching, сочетая удобство написания и эффективность работы. И это ещё полезнее. Однако.

В реальном мире код работает не только с разными видами процессоров, памяти и периферии. Код работает с другим кодом. И существует множество информационных систем, где, например, выражения из паттернов/комбинаторов для регистрации на какие-то события указываются через XML-конфиг, а потом придумываются дублируемые идентификаторы, связывающие их с неким исполняемым кодом (часто тоже не нативным). И да, люди, создающие системы с ручным редактированием XML, достойны перерождения в виде жаб в Бангалоре. Но это не отменяет необходимости интеграции с такими системами. И здесь даже нет выбора. Только через конфиг. Хотя... Ведь и его можно сгенерировать. Ещё одна возможность трансляции pattern matching: что слева - в конфиг, что справа - в код.

То есть, язык, решающий проблемы разработки, должен решать проблемы интеграции. Поддерживать в процессе компиляции как пользовательские compile-time алгоритмы, так и описания таргетов из пользовательских библиотек. Здесь конфиг, там HTML, а кому-то вообще кусочек COBOL на мейнфрейм сгенерировать надо.

Но зачем тогда вообще писать что-то на COBOL (Java, C++, SQL, XML, bash, make, whatever...), если это можно сгенерировать из единой исполняемой спецификации, гарантируя отсутствие расхождений на стыках языков? Да, всё так, они оказываются лишь артефактами старых систем. Настоящий язык программирования должен быть универсальным, и заменить сразу все неуниверсальные. Что не значит, что он будет единственным (таким). Будут и другие универсальные, возможно (точнее: когда-то) лучше.

Что мне с этого? Вот уже несколько лет занимаюсь разработкой такого языка. И до представления работающего продукта ещё многое надо сделать. И сейчас, куда как лучше по сравнению с началом, я понимаю, почему никто ещё не создавал ничего подобного, хотя предпосылки были и десятилетия назад. Об этом (в частности) - в следующих постах серии.
Buy for 10 tokens
Buy promo for minimal price.
buka

Немного Мадхьямики в MLTT сеттинге



В тибетской традиции есть такое понятие — Дхармадхату — пространтсво всех Дхарм. Это пространство всех мыслей которые существуют вне контекстов. Представить сложно — понятное дело. Но у нас есть MLTT теория которая поможет это представить.

Представьте себе пространство всех языков программирования — понятно дело все знают про лямбда исчисление. Но не многие же рубисты или ПХП программисты задумываются, что они пишут на языке пространства — которое с точностью до битов моделируется теорией типов Мартина Лефа (надо только вселенные правильно отконфигурировать, это научились делать в 2001 году, когда Coq все дружно писали). Конечно я сам в это по началу не верил, и думал что есть все-таки ограничения и что Данила Мастер, который вручную все сам делает вместо того чтобы экстрактить это из Инфинити Топоса делает ненапрасный труд. Мне пришлось написать прувер чтобы понять — таки да, каждый Данила Мастер, который считает себя инженером — производит временный и бесполезный труд, давая ярлыки феноменам не видя их сути.

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

У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.

Не многие знают, что имя линии передачи, которую мы официально представляем в Киеве, называется Лонгчен Ньингтик. KLONG по тибетски — это пространство, пространство всех феноменов, KLONG CHEN NYING THIG обширное пространство сердечной сущности. Так же как Инфинити Топос — это пространство всех MLTT типов, которое объединяет континуум и дискретное, а также проглатывает всю математику со всеми ее логиками и теориями, так как все математики разговаривают уже давно на этом языке кванторов и бесконеченых вселенных.

Так вот, точно также как все языки рождены из этого пространства, так же и мысли все рождаются из одного пространства, и все они проименованы, точно также, как проименованы все типы во всех вселенных. Рождаются тут условно, так как List не рождается, его можно обнаружить понять, но он всегда присуствует в Топосе во всех уровнях вселенных. Все типы являются несозданными, пока их не объявит программист в виде аксиом MLTT. Но если их рассматривать через призму нечистого видения — нетипизированного лямбда исчисления, то рассмотреть их не получится или очень сложно (Алонсо Черч и Боем с Берардуччи не смогли этого сделать). Ну а аналогия просветления — это выход в эту мандалу, где видны все типы сразу, или куда не кинешь взор, видишь везде похожие паттерны. Послушай функциональный программистов — натуральные же шизофреники, видят какие-то катаморфизмы там, где обычный человек видит while или for; видят группы, там где обычный человек видит record; чему обычные инженеры дали уже тысячу ярлыков. Знаете есть такое в духовных практиках быть остраненным и не вешать ярлыки на феномены, потому что это бессмылсенно. Это тоже самое что List/Cons и Stream/Mk — миллионы програмистов дали разныне названия этим штукам, но штуки эти существуют сами по себе и увидеть их можно при индуктивном рассмотрениии заполнения пространства типами начиная с Unit, и сделать это можно начиная уже с третьего шага.

Вообщем аналогии настолько прочные, что я могу в священных тибетских текстах заменять Дхармадхату на "Инфинити Топос", SEMS или Ум на "правила вывода" (кстати один из переводов SEMS — это вычислитель) или на "компютешинал аксиомы", CHOS или DHARMA (Феномен) на Тип и ничего почти не изменится. Процесс мышления — это то как вы конструируете теоремы, как вы выстраиваете рекурсивные цепочки, т.е. как вы композируете мысли (рекурсия и индукция). Если у типа нет рекурсора, значит вы не можете пустить мысль по этому феномену. А пустить мысль по феномену означет его осознание т.е. освобождение в дхармакае, что впринципе соотвествует этимологии слова элиминатор.

Пора положить конец спорам различных школ Мадхьямики (модели сватантрик) и описать все эти логики в виде MLTT программ.
buka

Erlang Killer Apps

В Эрланг среде принятно считать, что RabbitMQ и Riak, или по крайней мере riak_core — являются киллер приложениями Erlang. Я сам помню на начале своей карьеры тоже поставил на эти продукты и еще на Nitrogen. С нитрогеном я разобрался быстро (он уже история — все используют N2O уже давно). Настала очередь Riak или RabbitMQ, не знал за что взяться. Взялся сразу за распределенную базу, но так быстро на распределенные алгоритмы не наскочишь, а тестами покрывать распределенные системы — это не в этой жизни, может в следующей, если плохо себя вести буду. Вообщем исследование Chain Replication завело меня в тупик зависимых типов и я начал пить™.

Расскажу какие мысли у меня были во-первых по Riak. Riak после всего что я видел до него поверг меня в шок стоимостью обслуживания продакшина. Я с легкостью строил кластера пока не понял что они мне совершенно не нужны. Из riak нужно реально только riak_kv, riak_core и riak_pipe. Причем я даже собирал Riak без bitcask полностью (он вшитый в ядро) и многие другие штуки делал типа порт Riak под Windows 8. Собственно KVS появился как штука чтобы не ебаться с голым riak. В Riak вы храните бинари, а в KVS типы-рекорды описаные в схемах. Это потом в KVS появились бекенды.

Паралельно у меня был кластер из трех RabbitMQ. Тогда уже я понял что производительность RabbitMQ высокая только если они работают в шардах (не кластер, потому что интерконнет хуйовый у эрланга). Т.е. реально RabbitMQ используют все просто как ETS с красивым дашбордом для админов. Забейте хуй на RabbitMQ, эта штука покрыта кольцами как и Riak. Счас есть гораздо емкостные MQ типа emqtt.io (gproc в качестве деливери, mnesia — для дюрабилити), тоже причем с красивыми дашбордами. У меня кстати есть заказ от Остинелли на порт emqtt.io с gproc на syn.

Но я не об этом.

Спросите себя почему MQ и KV сервера в вашем окружении (а они у вас все равно есть, какое бы вы приложение не писали) находятся в разных приложениях. Ведь в вашем приложении MQ обслуживает клиентов, и KV обслуживает клиентов. Поэтому тут работатет data locality, а значит можно посадить это на одни и теже воркеры vnode. Но почему у всех ПОГОЛОВНО MQ и KV сервера — это разные продукты? Почему так? Ответа не нашел. Продуктов нет (разве что redis). Поэтому я подумал написать (еще два года назад) MQ + KV сервер работающий на одном ядре. И ядро это KVS.

KVS отвечает за durability, MQ должен хранить сабскрипшин меш своих подписок а также все сообщения (если очередь скажем персистента или нужны ACK или нужна транзакционность). Вполне очевидно что это можно хранить в том же KVS. Уверен что все люди которые используют RabbitMQ (илии другие MQ продукты) дублируют и синхронизируют свой сабскрипшин меш приложения и состояние подписок в mnesia таблицах RabbitMQ. Нахуя? Незнаю, в моем MQ такого дублирования не будет.

Какие я могу обеспечить показатели MQ сервера на KVS:

1) ну я могу выжать из мнезии 40K RPS на данных которые помещаются в RAM, и 20K RPS на данных которые не ограничиваются ничем. async_dirty естественно.

2) Data Locality. И серверы очередей и серверы данных будут обслуживать на одних и тех же vnode (по 64 или 128 на ноду), т.е. вычислятся хешом по идентификатору пользователя, а значит исчезает необходимость в синхронизации, так как все сообщения от MQ и KV протокола будут помещены в одну и туже очередь пользователя (линеаризация во имя консистентности).

3) Благодаря KVS, и MQ сервер и KV сервер будут поддерживать все бекенды которые поддерживает KVS: mongoDB, SQL, Riak, mnesia, redis.

4) доступ к очередям можно получать напрямую читая их из базы, если нужно. Еще был план написать универсальный REST эндпойнт к KVS как в Riak и CouchDB, и чтобы этот же эндпойнт был API для MQ сервера.

Ну и этот конструктор не имеет ограничений. На KVS можно лепить уже более сложные API и системы. Пример CR хоть и заезженный, но рабочий.

Вообщем надо соединять MQ и KV сервера, мое мнение, а вы делайте как хотите :-)
buka

Xi Editor

Вот казалось бы взяли самые новые и свежие языки (Swift и Rust) чтобы понизить латенси и все технологично было, и сново вылазит GC и его пики (или что это?). Представьте себе, что этот пик произошел, когда вы нажали на клавишу :-)



Собирается просто (надо только Xcode и rust), можно хачить, все равно это лучшее что есть из известного.
buka

Орнаменты

На меня снизошел очередной микро-инсайт-просветление и я сразу же спешу с вами ним поделиться. Абсоюлтно очевидная и прекрасная вещь. Признаюсь честно, что я в глаза формулировок не видел, но вот система сразу нарисовалась перед глазами. Кто читал МакБрайда поправит меня, я уверен.

Как вы знаете, все конструкторы (ко)-индуктивных типов могут состоять из параметров и типа результата конструктора. Последний может и не находиться во вселенной этого типа, а быть типом Path. Так вот параметры этого типа могут быть всего трех видов:

1) Unit, как в типе Lazy A: () -> A или ленивом Nil: () -> List A.
2) Fixed Type как в типе первого параметра коснтруктора Cons: A -> List A -> List A.
3) Recursive Type, как в типе второго параметра tail конструктора Cons, или второго поля tail рекорда коиндуктивного Stream (они равны в MLTT).

Это называется три орнамента. Они все задаются разными профункторами P_{1,2,3}, которые описаны у Паши в блоге. Из этих орнаментов мы конструируем тела термов в наших кодировках (всех их модификациях). Круто да? Это еще не все, суть орнаментов не в этом, а в том что вы можете транзакционно добавлять новые параметры в существующие конструкторы. В современных пруверах и в ООП в операции extend применимое к структурам или рекордам действует на уровне добавления новых конструкторов только, а не модификации (версионировании) существующих. Орнаменты же позволяют делать версионирование типовых интерфейсов и структур, и позволяют избежать случает когда приходится называть линковочные интерфейсы DirectDraw2. С помощью орнаментов вы можете добавлять аргументы в существующие конструкторы или менят их тип. Я привел только три орнамента, которых достаточно чтобы покрыть все существующие базовые библиотеки всех языков программирования :-) А представьте что орнаментов может быть больше!

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

Как вам такой "внутренний лисп" пространства типов?

_______________
[1]. https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf
buka

Лев тоже вкурсе про то, что ядро должно быть компактным

Лев называет это принципом де Брейна, хотя я такое не встречал в литературе, если кто видел где, покажите, я буду цитировать. Того самого де Брейна, учителя Барендрехта, который первый в мире автоматический прувер сделал AUTOMATH 1967 — голандская школа логиков (они еще записывали самые известные 100 теорем математики для всех систем на то время — http://www.cs.ru.nl/~freek/100 ); HOL/LCF 1972 это второй большой проект — британская школа, который дал миру ML и Хаскель тоже по сути британская школа, как и Агда и Идрис; и первый из современных пруверов Coq (инфинити предикативные вселенные и одна импредикативная внизу aka pCIC) — французкая школа.

https://youtu.be/c_S_bAdv4A0?t=719

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

Андрей Байер тоже за минимальные ядра

Вот тут Андрей Байер (может быть известный программистам по Programming Languages Zoo — сборнике имплементаций ML вариаций), в лекции посвященной элиминатору индукции и равенству выраженному в чистой лямбде, в секции ответов на вопросы, говорит, что критически важно иметь простое ядро прувера:

https://youtu.be/IlfQjWqrK6I?t=3690
buka

Подкаст

Подкаст записали. Виктора правда не было, были только мы четвером. Писали в Хенгауте, уже впринципе запись доступна, но выложим после того как "эканье" Маша повырезает. Где-то в понедельник. Stay tuned. Вот вам пока, языческий хендмейд арт тематический, православные, живую традицию которого я держу уже не один пятый год: