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
Buy for 10 tokens
Buy promo for minimal price.
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. Вот вам пока, языческий хендмейд арт тематический, православные, живую традицию которого я держу уже не один пятый год:

buka

Вопросы на Подкаст

Друзья, перед Первым Категорным Митапом (где Groupoid Infinity будет презентовать свой тайпчекер языка с зависимыми типами и базовой рантайм библиотекой, где все это компилируется в Эрланг) мы решили сделать разогревочный подкаст.

В подкасте планируются такие учасники:
0. Влад Кириллов (@darkproger) — Lagrange Inversion, модератор
1. zeit_raffer — Groupoid Infinity
2. maxim — Groupoid Infinity
3. nponeccop — HNC

1. Знакомство. Все обсуждают текущие свои проекты. Чем они занимались до этого. Я рассказываю про приватбанк, распределенные алгоритмы и их доказательства. Как я через CR пришел к EXE и нашел Пашу. Паша рассказывает про себя. Влад про себя, Процессор про себя.

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

3. Дальше мы обсуждаем архитектуру OM/EXE. Тут все рассказывают со своей стороны, Андрей рассказывает про HNC, мы рассказываем про кодировки, рассказываем про HIT, HoTT и обсуждаем тему божественности MLTT. Готовим людей к тому чтобы слушать доклад про кодировки.

4. Обсуждаем приложения OM/EXE: распределенные алгоритмы, как кафедральный прувер для лабораторных работ. Не забываем что основной задачей подкаста найти людей которые хотят хачить OM/EXE.

Если кто хочет перевести эту беседу или добавить ручайков в русло — пишите, или учавствуйте в подкасте. Или просто оставляйте вопросы к посту, на которые хотите услышать ответ.
buka

pema.guru (http://pema.guru)

Сделали сайтик, напоминалочка про затвор:



Там на странице традиция есть ссылка на nying.ma и структуры всех тибетских терма, в которых есть куча ошибок (так как переводил я, а не лама), но думаю, что многим будет интересно заглянуть в структуру терма Дуджома и сравнить их с Лонгчен Ньинтик (обширное пространство сердечной сущности) и новых терма, такие как терма Апама Тертона.

А для Лонгчен Ньингтик я хочу сделать полное цифровое собрание текстов и собрание всех русскоязычные переводов. Но только по Лонгчен Ньингтик, остальные переводы, будут только наши, никакие другие переводы приниматься не будут. Жирным текстом на странице обработанные тексты.

Напоминаю, что проект nying.ma — волонтерский, это по сути монастырского уровня проект без монастыря, без финансовой поддержки, вся работа была сделана за свой счет. Что сделано:



* Оцифровка изображений SVG
* Система публикации PDF, HTML из TeX
* Система управления каталогами тибетских собраний
* Электронный реестр текстов с мультиязычной структурой
* Полностью публичные карчаки (оглавления) всех терма (откровений)
* Тибетский Wylie UTF-8 конвертор (120 LOC :-)
* Ситема каталогизации тибетских текстов и PDF файлов
* Проект открытый (open source)

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

Будущие подпроекты:

* Онлайн редактор (JavaScript) тибетских табличек (печа)
* Планирование составление карчагов по 120 ГБ текстов старых и новых терма

__________
[1]. https://github.com/pemadudul/pema.guru
[2]. https://github.com/5HT/wylie
[3]. https://github.com/5HT/nying.ma
[4]. https://github.com/5HT/pub
buka

Покрой консистентность тестами!

http://highload.guide/blog/saga-cluster.html

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


Чуваки за 15 лет не смогли написать распределенный координатор транзакций, я уже молчу про горизонтальное масштабирование. Если добавить к этому утверждению коре разработчика (который думает что в XA чтение не может быть целостным) то, что у них вместо теорем — покрытие кода тестами, то получится что Постгрес пишут три долбоеба, что и говорить про остальных?

P.S. Даже если я допишу свой CR через 15 лет, все равно я буду на шаг впереди индустрии. Да, на самом деле, EXE/OM появился как продукт необходимый для доказательства распределенных алгоритмов и их экстрактов.