Russian Lambda Planet

2020-01-24T13:13:38+00:00

cl-maxminddb

В общем, нужно было делать запрос к базам MaxMind. Не нашёл ничего вменяемого под CL. Хотел было быстренько сделать биндинги к си библиотеке, но там были передачи значений на стеке, что-то я запутался и подумал, что можно и нативно налабать. В общем, накидал. Читает, правда без всякой обработки ошибок в том плане, что версия БД и т.д. прочие вещи, которые можно было бы сделать. Но он работает. :) Вот код. Собственно, небольшой пример:

> (with-mmdb (mmdb "/var/lib/GeoIP/GeoLite2-City.mmdb")
    (mmdb-query mmdb "8.8.8.8"))

(("continent" ("code" . "NA") ("geoname_id" . 6255149)
  ("names" ("de" . "Nordamerika") ("en" . "North America")
   ("es" . "Norteamérica") ("fr" . "Amérique du Nord") ("ja" . "北アメリカ")
   ("pt-BR" . "América do Norte") ("ru" . "Северная Америка")
   ("zh-CN" . "北美洲")))
 ("country" ("geoname_id" . 6252001) ("iso_code" . "US")
  ("names" ("de" . "USA") ("en" . "United States") ("es" . "Estados Unidos")
   ("fr" . "États-Unis") ("ja" . "アメリカ合衆国") ("pt-BR" . "Estados Unidos")
   ("ru" . "США") ("zh-CN" . "美国")))
 ("location" ("accuracy_radius" . 1000) ("latitude" . 37.751d0)
  ("longitude" . -97.822d0) ("time_zone" . "America/Chicago"))
 ("registered_country" ("geoname_id" . 6252001) ("iso_code" . "US")
  ("names" ("de" . "USA") ("en" . "United States") ("es" . "Estados Unidos")
   ("fr" . "États-Unis") ("ja" . "アメリカ合衆国") ("pt-BR" . "Estados Unidos")
   ("ru" . "США") ("zh-CN" . "美国"))))

Guile 2.0 и парсинг xml в несколько потоков

2019-04-05T11:46:26+00:00

Вчера столкнулся с ещё одной странностью в guile. При использовании библиотеки sxml для парсинга xml, соотвественно, всё кажется нормальным, пока парсинг идёт в одном потоке. Но как только потоков несколько, то сразу начинается веселье - xml не парсятся, жалуются на отсутствие нужных закрывающих тегов и прочая ерунда, которая говорит о том, что входные данные неправильные. Это в версии 2.0. Версию 2.2 не проверял из-за того, что её как-то геморнее устанавливать и непонятно надо ли. Пришлось на процесс парсинга делать мютекс и захватывать его на время парсинга. Но что-то какое ощущение, что поделка сугубо студенческая.

2019-02-27T11:02:06+00:00

Если хочется какой-то вменяемой разработки на схеме, то лучше брать Racket. Он значительно удобнее и проще. Опыт использования guile показал мне только боль и печаль. Причём сам он неплох, но нужно использовать свежие версии, а свежих версий в Debian Stable нет. Там 2.0 только. А в 2.0 guile, грёбаный стыд, нельзя сделать https запрос. И с 2.0 версией не работает емаксовый плагин. :( В общем, кто будет что начинать на схеме - только Racket. Там всё более развито. А если так смотреть, то вместо схемы лучше взять Common Lisp. Он как-то ближе и проще. :)

arXiv:1808.06351 [cs.LO]

2018-08-21T04:58:01+00:00

https://arxiv.org/abs/1808.06351

Lambda Calculus with Explicit Read-back

This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its properties. Namely, we verify that it correctly represents the lambda calculus. Further, we show that there is exactly one reduction sequence that starts with any term in our term rewriting system. Finally, we represent the leftmost strategy which is known to be normalizing.

comments

Missing equivalence in the interaction calculus

2018-07-04T08:55:19+00:00

Configuration

<... | x = α(...y...), y = β(...x...)>

can be reduced to both

<... | x = α(...β(...x...)...)>

and

<... | y = β(...α(...y...)...)>,

which syntactically appears as a counterexample to strong confluence, while essentially representing the same configuration.

Is there a way to formalize equivalence between those two normal forms?

I think there is:

comments

arXiv:1806.07275 [cs.LO]

2018-06-29T04:35:31+00:00

https://arxiv.org/abs/1806.07275

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, one of counterexamples being known due to Plotkin. This paper explores upward confluence in the interaction calculus. Can an interaction system have this property? We positively answer this question and also provide a necessary and sufficient condition for stronger one-step upward confluence. However, the provided condition is not necessary for upward confluence as we prove that the interaction system of the linear lambda calculus is upward confluent.

comments

Обратное свойство ромба

2018-06-03T09:40:36+00:00

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

Пока у меня ничего толком не устоялось, рабочее определение обратимой системы взаимодействия такое: 1) для любой подсети Ν должно быть не более одной активной пары α><β, которая редуцируется к N, и 2) если две подсети M и N - результы взаимодействия активных пар α><β и γ><δ, соответственно, то M и N не пересекаются. Речь идет лишь о подсетях и активных парах, так как об обратимости конфигураций говорить нельзя, когда в сети больше одной активной пары. Не уверен, что это исчерпывающий список условий, но уже их достаточно, чтобы заметить пару-тройку следствий.

Одно из следствий такого определения немедленно накладывает ограничения на правила взаимодействия. В частности, правая часть каждого правила обязана быть связной сетью. Доказательство от противного: строим простой контрпример с двумя одинаковыми активными парами, взаимодействие которых приводит к двум неразличимым сверткам для каждой активной пары, нарушая условие (2). Также потребуется асимметрия правой части правила для α><β, если α и β различны. Продолжу думать в этом направлении позже, хотя уже предчувствую трудности с интерпретацией обратимых систем взаимодействия в исчислении взаимодействия. Например, придется как-то выкручиваться с разыменованием (indirection), применение которого сугубо неоднозначно.

Но самое интересное свойство обратимых систем взаимодействия - это, наверное, обратное свойство ромба. Получается, если такие системы вообще существуют, они одновременно будут обладать и прямым (strong confluence), и обратным (strong upward confluence) свойствами ромба. Это, конечно, мне напомнило об упражнении 3.5.11 (vii) у Барендрегта. Когда я бегло проходил по упражнениям к нескольким главам три года назад, мне не удалось быстро его решить. Было обидно.

Задача была показать, что для термов (λx.b x (b c)) c и (λx.x x) (b c), принадлежащих Плоткину, не существует общей β-экспансии, хотя они оба редуцируются к b c (b c). Эти два терма служат контрпримером для "обратного свойства Черча-Россера" β-редукции. Сегодня я решил поискать, как именно выводить противоречие из существования их общей β-экспансии, и нашел "An Easy Expansion Exercise" (Vincent van Oostrom). Там предлагается использовать теорему о стандартизации. Правда, я не очень понял, как ограничиться материалом конкретно третьей главы.

Update. In a reversible interaction system (RIS), the right-hand side (RHS) of each rule needs to include at least one agent, that is RHS cannot be a wiring: RHS of α[x, x]><β is ambiguous, α[x]><α[x] violates condition (1) in the definition of RIS, and more than one wire make a disconnected net, violating condition (2). As a consequence, in the interaction calculus, each name in an interaction rule needs to have at least one of its two occurrences in a term that is not a name; otherwise we have a disconnected subnet in its RHS. Now it is easy to see strong upward confluence in RIS.

comments

Cofree Will Tear Us Apart

2018-05-23T00:00:00+00:00

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

Haskell + Raspberry Pi Zero W = шаг в embedded-мир

2018-05-19T00:00:00+00:00

Haskell универсален, не так ли? А запустим-ка его на новеньком Raspberry Pi Zero W.

Слышь, у тебя функциональщина в репе есть? А если найду?!

2018-03-12T19:37:55+00:00

What are the criteria for a programming to be called functional?

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

Тьюринг-полнота говно и у неё нет пиписьки

2018-03-03T23:30:28+00:00

Теперь и на кворе: http://qr.ae/TU8m84

Попытался там насрать своими старыми идеями о том что тьюринг-полнота — это совершенно бесполезное свойство. Интересно, кстати, что если налетят любители идеи, что С неполон (я считаю, что он неполон "на самом деле"), у меня для них есть домашняя заготовка.

Лекции по функциональному программированию на Haskell

2018-03-03T19:33:18+00:00

В этом году наконец решил, как давно планировал, не просто писать лекции по Haskell на доске, а сделать нормальные слайды.

Первые 4 лекции выложены на https://github.com/alexeyr/miet-haskell-course/, остальные будут по ходу семестра.

Полезным идиотам хуёиды нинужны!

2018-02-16T23:38:11+00:00

https://www.quora.com/Why-do-people-count-from-0-in-computer-science-Is-that-a-natural-choice

Exhausting Combinators

2018-02-08T18:06:50+00:00

Early this year, I made a post on LtU about the experimental "abstract" algorithm in MLC. Soon after that, Gabriel Scherer suggested doing exhaustive search through all possible inputs up to a particular size. Recently, I decided to conduct such an experiment. Here are

Some results

I managed to collect some results [1]. First of all, I had to pick a particular definition for "size" of a λ-term, because there are many. I chose the one that is used in A220894 [2]:

size(x) = 0;
size(λx.M) = 1 + size(M);
size(M N) = 1 + size(M) + size(N).

For sizes from 1 to 9, inclusively, there exist 5663121 closed λ-terms. I tested all of them against both "abstract" [3] and "optimal" [4] algorithms in MLC, with up to 250 interactions per term. The process took almost a day of CPU time. Then, I automatically compared them [5] using a simple awk(1) script (also available in [1]), looking for terms for which normal form or number of β-reductions using "abstract" would deviate from "optimal".

No such terms have been found this way. Surprisingly, there have been identified apparent Lambdascope counterexamples instead, the shortest of which is λx.(λy.y y) (λy.x (λz.y)) resulting in a fan that reaches the interaction net interface. I plan to look into this in near future.

As for sizes higher than 9, testing quickly becomes unfeasible. For example, there are 69445532 closed terms of sizes from 1 to 10, inclusively, which takes a lot of time and space just to generate and save them. [6] is a 200MB gzip(1)'ed tarball (4GB unpacked) with all these terms split into 52 files with 1335491 terms each. In my current setting, it is unfeasible to test them.

I may come up with optimizations at some point to make it possible to process terms of sizes up to 10, but 11 and higher look completely hopeless to me.

[1] https://gist.github.com/codedot/3b99edd504678e160999f12cf30da420
[2] http://oeis.org/A220894
[3] https://drive.google.com/open?id=1O2aTULUXuLIl3LArehMtwmoQiIGB62-A
[4] https://drive.google.com/open?id=16W_HSmwlRB6EAW5XxwVb4MqvkEZPf9HN
[5] https://drive.google.com/open?id=1ldxxnbzdxZDk5-9VMDzLvS7BouxwbCfH
[6] https://drive.google.com/open?id=1XjEa-N40wSqmSWnesahnxz6SXVUzzBig

comments

ну всё теперь

2018-01-29T05:18:14+00:00

(сам внезапно набирающий популярность ответ здесь)

State of the Haskell ecosystem

2018-01-27T22:42:38+00:00

Гонзалес тут написал мегаобзор того, что в х-е работает, а что написано академиками и школотой:

https://github.com/Gabriel439/post-rfc/blob/master/sotu.md

Шлите ему PRs если он чего упустил!

В копилку универсальных шаблонов

2018-01-24T15:25:10+00:00

https://nponeccop.livejournal.com/585243.html?thread=5156123#t5156123

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

https://nponeccop.livejournal.com/585243.html?thread=5159707#t5159707

> почему X не относится к легаси?

На нём делают новые проекты - т.е. он не из серии «я не помню статей "для нашего нового проекта мы выбрали X...."»

Обзор языков - 2018

2018-01-23T20:04:18+00:00

Если писать не о чем - напишите обзор ЯП на основе какого-нибудь измерения пиписек в попугаях!

Берем Tiobe index и группируем "по семействам". Получаем:

- Нестыдные языки для промышленных зрелых практиков с кредитом и детьми. На собеседовании ничего объяснять не надо: Java/C++/С/C#/Python/Javascript/PHP/Ruby/SQL

- Нишевые языки, надо объяснять что это за язык и что за ниша и что это не такая и экзотика: R/ Swift/Objective-C/Matlab/Scratch/asm/Go
- Лигаси языки: VB.net, Perl, Delphi

Из нестыдных можно вычеркнуть языки, вместо которых можно учить аналогичные: C, C#, PHP, Ruby учить не нужно. Получается, что нужно: Java, C++, Python, Javascript, SQL. Причём имеет смысл учить комплектами:

- С++ самодостаточен
- Java+Javascript
- Python+Javascript

SQL это как бы не "язык", а "технология", наряду с noSQL и ORM и даже (с натяжкой) мессаджингом и прочим миддлваре. Аналогично HTML/CSS/DOM. Короче они в отдельном от языков списке изучения идут, примерно в том же, где и алгоритмы с проектированием.

В-общем, ничего нового, этот список (С++, Java, Python, Javascript, SQL) не менялся наверное последние лет 10. В 1998 был бы скорее С++, Perl, Scheme, SQL.

Кроме этого списка есть список 9 языков, на которых можно начинать новые проекты в 2018, который я составил, используя modulecounts.com:

Первый эшелон (либ больше чем в перле): Java, C#, Python, Ruby, NodeJS, PHP
Второй эшелон (либ меньше чем в перле): Clojure, Go, Rust
Эшелон упоротых (либ меньше чем в расте но хоть сколько-то): Haskell, R и Erlang.
Эшелон альтернативно упоротых (там совсем по-другому): С, C++

Причём Раст догнал и перегнал хаскель (идущий в ногу с R) за последний год. А в Эрланге в 3 раза меньше пекеджей чем в х-е ("по версии modulescount")

Ещё можно составить список "почётных провалов":
- idris, coq/ocaml, ats
- elm, purescript, typescript
- D, lua, scala, kotlin, julia

Если вычесть из списка топ-50 языков тиобе вышеперечисленные, то останутся:

Странные "проприетарные" языки: Apex, SAS, Codesys
Матерые старички: Lisp, Bash, Prolog, Tcl, VHDL, ActionScript, COBOL, ABAP, Logo, Ada, REXX, Fortran, LabVIEW
Всякие невыстрелившие: F#, Groovy, Hack, Dart, Alice

Призы зрительских симпатий уходят ноде, тайпскрипту, элму, расту, го, haxe, flow, codesys, перлу, vb.net и котлину!

Кстати, есть ещё языки, на которых (в определённых кругах) писать нельзя. Это:

- лиспы (скобочки!)
- перл, с++, javascript (большие неконсистентные языки)
- С, С++, D, Rust (нет gc или безопасности памяти)
- haskell (avoid success, ленивость, утечки, баги, борьба с тайпчекером, отсутствие инструментов)
- С, С++, С#, Java, Python, Delphi (низкоуровнево). Даже х-ь иногда (от любителей кдб, например)
- Python (кривые замыкания)
- все языки за пределами нестыдных (по причине стыдности)
- нода (т.к. евент дривен и жабоскрипт и либы написаны идиотами)
- руби, го (хипсторы и подвороты)
- похапе
- Rust (надо писать на Go)
- Go (gc же богомерзкий)
- Typescript (негодная система типов, надо писать на flow)
- Flow (он не развивается, надо писать на тайпскрипте)

В-общем, в зависимости от того, кого вы спрашиваете, нельзя писать вообще ни на чём!

Upd: тут подбросили ссылку на DOU: https://dou.ua/lenta/articles/language-rating-jan-2018/

Ну и там неприятные новости для упоротых:

- оставьте С для эмбеддеда, низкоуровневых либ и иных спецприменений: только С++, только хардкор!
- Python и PHP живее всех живых
- С#, притом это вовсе не емакс и моно, - 15% всей работы и 3-е место после жабы и жс
- в топе святая шестерка - Java/C#, Javascript/Python/PHP, C++ (и там же SQL на самом деле™)
- хотите промышленной зрелой экзотики - добро пожаловать в Typescript, Go, Ruby, Scala
- мобло - это Swift и внезапно Kotlin, причем если про котлин не совсем понятно - то Swift опередил Objective-C
- Delphi и 1C ещё встречаются
- в "совсем уж экзотике" в Украине значатся Closure и R
- из лигасёвого лигаси только перл

Upd2: Scala, Typescript и Kotlin - внезапно не провалы

Эффекты в Haskell

2018-01-18T00:00:00+00:00

Реализация эффектов в Haskell.

Обращение в будущее

2018-01-13T08:11:02+00:00

Убедительная просьба к тем, кто будет создавать следующий язык программирования, скажем, Java Pro или Scala ++. Пожалуйста, добавьте синтаксический сахар для монад, например, похожий на вычислительные выражения F#. Порою очень не хватает

Эффекты и чистые функции

2018-01-10T00:00:00+00:00

Попытка объяснить эффекты без монад.

Программировал в прошлом году - отчитайся

2018-01-03T10:15:13+00:00

Не забудьте заполнить форму о используемых языках программирования в 2017

https://dou.ua/lenta/sitenews/programming-languages-survey-2018/

//боже мой, я это делаю уже 9 лет

Нестандартные запросы в Slick.

2017-12-25T16:33:26+00:00

Можно ли в Slick сформировать запрос, аналогичный такому?

select * from jr
       where (id1, id2) in (
         ('000002e4-6b99-45ac-9187-4d00b7b457fc', 'a1c4fa6f-370c-11e6-bb37-f832e4bd9ad8'),
         ('00011eaf-f65d-42a7-ae54-3b16dff65f22','4834f6b6-af4a-4cc5-88d6-924a84f0ef31'));

Стардарт SQL такое не поддерживает, но и MySQL, и Postgres его выполняют. Но в Slick как сделать из двух slick.lifted.Rep[String] одну slick.lifted.Rep[(String,String)] я не нашел. Это вообще возможно?

Програмологія: Розслідування фальшивих академіків НАН

2017-12-21T08:04:32+00:00

Поки ми готуємо документи, якими ми намагатимемось бомбардувати наші корумповані прикордонні служби, прокуратуру та інші установи, на які тільки у нас вистачить грошей, у зв'язку з недопуском в Україну видатного математика-педагога, дійсного члена комітету по стандартизації мови Haskell, я вирішив поцікавитися, а які у Українців є опції, якщо не Брагілєвскьий, то хто в Україні претендує на звання спеціаліста з поєднання логіки та математики? Результати мене надзвичайно здивували, виявляється у нас є академік НАН України, який є прямим конкурентом Хаскеля Карі, Філіпа Вадлера, Стівена Кліні, Хенка Барендрехта та інших. Однак, що дивно, у списку його праць жодним чином немає згадок про його закордонних колег. Я вирішив провести розслідування і детальний аналіз цього академіка разом з його працями, аби з'ясувати, яке майбутнє чекає Україну в контексті приходу алгебраїчних мов програмування у повсякденну інженерну практику (перш за все я маю на увазі функціональні мови програмування, які ви всі добре знаєте: ML, Haskell, Scala, Erlang, Clojure).

Редько Володимир Никифорович

Граматика

Почнему з базової елементарної освіти 1—9 класів. Зайдемо на сайт Кафедра теорії та технології програмування, читаємо:

"Повні класи вичіслімих функцій різних рівнів абстракції були описані." — формулювання речень у стилі магістра Йоди з граматичними помилками.
"Мета проекту: автоматизації математичних відрахувань до різних областях" — взагалі незрозуміло про що йде мова.
"Деякі програми САД є:
розподілених автоматизованих докази теорем
верифікації математичних текстів
дистанційного навчання в математичних дисциплін
будівництво баз даних для математичних теорій
" — таке враження, що перекладали translate.google.com, але якщо подумати над суттю, то вийде, що максимально, що тут можна собі уявити — це "блокчейн з теоремами", рівень магістерських робіт на заході.

"Розробка програмних засобів для Склад називному Мови (CNL)
Короткий опис: Є розробки програмних засобів для підтримки не менше трьох CNL:
Бекон (Основні CNL)
DECON (Описова CNL = Бекон + описові вирази нових складів через основні з них)
Recon (Рекурсивні CNL = DECON + рекурсивного вираження нових складів через основні з них)
" — тут я так розумію Бекон, Декон та Рекон, це щось накшталт Relux, Redux та React, торгові марки університету, які вочевидь є темами захисту докторських дисертації в Національному Університеті України ім. Тараса Шевченка. Направді абсолютно синтетичні, надумані теорії які немають жодного зв'язку з реальністю.
"беконом і DECON знаходяться в бета-версії стадії тестування" — речення побудоване роботами-дибілами.
"Хід об’єкту: перша версія готова" — посилання не працює, в rar файлах вірогідність відшукати щось працююче хоча б на Delphi дорівнює нулю.

Аналіз програмології, як конкретної науки

Я буду називати це спробою аналізу, тому, що заглиблюватися в цей божевільний світ маразму у мене немає часу та можливостей. Почнемо зі списку праць нешанованого академіка, та вікіпедії.

"Неоклассические логики предикатов" — неокласичні, ну добре, про Хаскеля Карі забули, а вже в неокласики.
"Композиционно-номинативный подход к уточнению понятия программы" — 1999 рік, у той час коли на заході вже верифікували процесори за допомогою ACL2, Coq та HOL.
"Композитционные базы данных" — орфографія збережена, учень цього академіка Буй полюбляє бази даних, тому наукові роботи пестрять CASE системами та SQL моделями на Delphi.

Ось ці теми дуже вражають своєю теоретичністю:
"Базы данных и информационные системы" — тут вчать писати INNER JOIN.
"Введение в операционные системы" — цікаво чи інститут Шевченко зробив хоч одну операційну систему, яка була проваджена виробництво (відповідь очевидна, ні)
"Неподвижные точки и операторы замыкания: программологические аспекты" — тут йдеться мова очевидно про фікспойнти, F-алгебри, однак згадки про Філіпа Вадлера, та Вармо Вене ви там не знайдете. А коли відриєте дисертацію на цю тему то у вас випаде останнє волосся.

Наукові зв'язки
"Кафедра теорії та технології програмування має наукові зв’язки з провідними учбовими та науковими установами у багатьох країнах світу: Данія, Макао, Молдова, Латвія, Нідерланди, Німеччина, Польща, Росія, США, Фінляндія, Франція, Чехія" — очевидно ніяких посилань, я впевнений якщо запитати з ким вони там зв'язуються то виявиться що половина неправда, а інша половина це їхні студенти які влаштувалися там з "програмологією" в Макао.

Приклади робіт учнів цього академіка

Омельчук Людмила Леонідівна УДК 681.3 АКСІОМАТИЧНІ СИСТЕМИ СПЕЦИФІКАЦІЙ ПРОГРАМ НАД НОМІНАТИВНИМИ ДАНИМИ

Дослідження декартових добутків, транзитивності. Нагадую — це не реферат, а дисертація на здобуття кандидата! Ви думаеєте, що це одна стаття така? Будь-яку берете, розбираєте на атоми і впевнюєтеся, що це якшо не шизофренія, то просто балаболство і накидання математичних термінів для вигляду у журнал "Мурзілка".

УДК 681.3.06 Бойко Б. I. СТРУКТУРА ІМЕНУВАНЬ У ПРОГРАМУВАННІ

Робота Бойко присвячена тому, як називати змінні в мові програмування Delphi, і приклад як роботи запити на мові Delphi в базу даних SQL.

Список людей які захищалися

Однак сам академік, який придумав "Програмологію" це гідра, яка генерує своїх клонів: Редько, Нікітченко, Буй, син Редька (очевидно, що корупція), та інші менш значущі доцентіки. Усі вони начебто займаються математичною логікою та відносять себе до мінжародної школи "Програмології" яку вигадав Редько і про яку більше ніхто крім цього гадюшніка не знає.

http://science.univ.kiev.ua/research/scientific_school/programologiya-ta-yiyi-zastosuvannya/

P.S. Стаття буде наповнюватися новими прикладами математичного аферизму та шизофренії в КНУ ім. Шевченка та академіків НАН.

Список літератури для аналізу

[1] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/86588/08-Redko.pdf?sequence=1
[2] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/1530/08-Redko.pdf?sequence=1
[3] http://knutd.edu.ua/publications/pdf/Visnyk/2012-5/34_42.pdf
[4] http://dspace.nbuv.gov.ua/bitstream/handle/123456789/1454/%E2%84%962-3_2008_Zybenko.pdf?sequence=1

Прошу долучатися та додавати ті дисертації які заслуговують Фрунзе 103 на вашу думку. Фактично будь-яка робота, якщо детально її проаналізувати це мімікрія під головного Програмолога України.

конец хаскеля

2017-12-19T17:00:58+00:00

Свежее выступление Майкла Сноймана:
https://www.youtube.com/watch?v=KZIN9f9rI34
"Вот посмотрим на простейшие монадные трансформеры. Тут фигня, и тут фигня. Тут не срастается. Тут не работает. Тут данные теряются. Тут опять фигня. Мой совет: не вы#$%йтесь, используйте мутабельные переменные, кидайте рантайм исключения."

fooling people with theorem provers

2017-12-18T12:32:00+00:00

Занятный доклад на свежем FP Conf про equational reasoning и теорем пруверы:
https://www.youtube.com/watch?v=TRAPqhRdAH0
Докладчик рассказал, почему Liquid Haskell и F* пока не годятся, потом показал как он на Isabelle верифицировал вывод radix sort'a из tree sort'a, взятый из старинной статьи Gibbons'a. Типа, вот у нас реализация сортировки через построение дерева, вот мы тут колдуем-колдуем с эквивалентными преобразованиями кода и вот свели сортировку к foldr по списку, получился радикс сорт, сортирует за один проход, красота.
Только это все неправда.
То, что там названо treesort'ом, внутри себя уже реализует принципы радикссорта. Идея такая. Вот есть у нас список, условно, коротких строк ограниченной длины, [a]. И есть функции извлечения "букв" a -> b, где тип "букв" b принадлежит классам Bounded и Enum, т.е. все его возможные значения можно перечислить по порядку списком
rng = [minBound .. maxBound]
Тогда входной список "строк" можно разбить на подпоследовательности / бакеты - по одной для каждого значения "буквы". Partitioning function:

ptn :: (Bounded b, Enum b) => (a->b) -> [a] -> [[a]]
ptn d xs = [ filter ((m==) . d) xs | m <- rng ]

Здесь d - функция извлечения "буквы" b из "строки" a.
Тогда возьмем набор функций [a->b] по извлечению из условной строки первой буквы, второй буквы, третьей... Разобьем входные данные на бакеты по первой букве, каждый из них - на бакеты по второй, те - по третьей и т.д., получим дерево списков. В каждом узле дерева бакеты идут по порядку возрастания "букв", так что в итоговом дереве все окажется уже отсортированным, останется лишь его сплющить в один выходной список.

data Tree a = Leaf a | Node [Tree a]

mktree :: (Bounded b, Enum b) => [a->b] -> [a] -> Tree [a]
mktree [] xs = Leaf xs
mktree (d:ds) xs = Node (map (mktree ds) (ptn d xs))

treesort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
treesort ds xs = flatten (mktree ds xs)

Тут важно, что mktree принимает два списка, ds и xs, первый это короткий список функций по извлечению "букв", второй - сами данные, которые уже будем сортировать, и организована mktree индукцией по списку функций. И flatten имеет очевидное устройство тоже индукцией по дереву. Ну и вот, дальше Gibbons и вслед за ним наш докладчик просто берут эти mktree и flatten и выражают их через foldr, заменяют явную рекурсию стандартным катаморфизмом, плюс избавляются от промежуточной структуры дерева, т.к. собранное mktree дерево тут же flatten'ом разбирается обратно. И, собственнно, весь equational reasoning и вся верификация на Isabelle сводятся к тому, чтобы показать, что реализация на foldr равна процитированной тут реализации на явной рекурсии. Это дело чистой механики и переписывания термов, сам алгоритм там не меняется ни сколько. Получается

radixsort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
radixsort = foldr ft id
  where ft d g = concat . ptn d . g

Вот он, один проход по списку, но это проход по списку функций извлечения "букв", а не по входным данным! А вот по входным данным мы будем елозить внутри ptn, в каждом узле дерева входной список данных будет пройден L раз, где L - размер алфавита. Причем Gibbons в статье это понимает и честно отмечает, предлагая в конце альтернативную реализацию функции раскидывания по бакетам ptn. Но исходные рассуждения и доказательства проводятся не с ней, а с наивным вариантом. Докладчик с FPConf же то ли честно не понимал, что делает, то ли решил публику обмануть ради пущего эффекта. Вот, говорит, сортировка за один проход списка foldr'ом. А что совсем не того списка - не сказал. :) Ну и "доказал корректность" довольно простой тавтологии (radixsort == treesort), молодец.

Выучить от сих до сих!

2017-12-11T07:30:51+00:00

Отседова: https://github.com/mpickering/apply-refact/blob/master/src/Refact/Fixity.hs#L115-L155

-- | All fixities defined in the Prelude.
preludeFixities :: [(String, Fixity)]
preludeFixities = concat
    [infixr_ 9  ["."]
    ,infixl_ 9  ["!!"]
    ,infixr_ 8  ["^","^^","**"]
    ,infixl_ 7  ["*","/","quot","rem","div","mod",":%","%"]
    ,infixl_ 6  ["+","-"]
    ,infixr_ 5  [":","++"]
    ,infix_  4  ["==","/=","<","<=",">=",">","elem","notElem"]
    ,infixr_ 3  ["&&"]
    ,infixr_ 2  ["||"]
    ,infixl_ 1  [">>",">>="]
    ,infixr_ 1  ["=<<"]
    ,infixr_ 0  ["$","$!","seq"]
    ]

-- | All fixities defined in the base package.
--
--   Note that the @+++@ operator appears in both Control.Arrows and
--   Text.ParserCombinators.ReadP. The listed precedence for @+++@ in
--   this list is that of Control.Arrows.
baseFixities :: [(String, Fixity)]
baseFixities = preludeFixities ++ concat
    [infixl_ 9 ["!","//","!:"]
    ,infixl_ 8 ["shift","rotate","shiftL","shiftR","rotateL","rotateR"]
    ,infixl_ 7 [".&."]
    ,infixl_ 6 ["xor"]
    ,infix_  6 [":+"]
    ,infixl_ 5 [".|."]
    ,infixr_ 5 ["+:+","<++","<+>"] -- fixity conflict for +++ between ReadP and Arrow
    ,infix_  5 ["\\\\"]
    ,infixl_ 4 ["<$>","<$","<*>","<*","*>","<**>"]
    ,infix_  4 ["elemP","notElemP"]
    ,infixl_ 3 ["<|>"]
    ,infixr_ 3 ["&&&","***"]
    ,infixr_ 2 ["+++","|||"]
    ,infixr_ 1 ["<=<",">=>",">>>","<<<","^<<","<<^","^>>",">>^"]
    ,infixl_ 0 ["on"]
    ,infixr_ 0 ["par","pseq"]
    ]

Это вам не таблички "как работает == в джаваскрипте" по карманам тырить!

Статус HaLVM (годичной давности)

2017-12-03T02:32:33+00:00

http://uhsure.com/halvm3.html

Мне вот кажется изначально дебильной эта задача "стать совместимыми с Hackage-либами юзающими Си"

Верифицированный лигаси-фри стек в пару рыл за 20 лет

2017-12-03T02:11:30+00:00

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

Итак, смотрим что можно сделать относительно реалистичного.

POSIX-говно выбросить проще простого - роль BIOS играют коммерческие гипервизоры, которые со временем верифицируются, особенно Type 1 типа Hyper-V, ~~ESXi и Xen~~; роль libc - интерфейс гиперколлов. В KVM virtio, впрочем, гиперколлов нет, а паравиртуализированные устройства - это обычные PCI-устройства, просто с менее дебильным интерфейсом. Минимально нужен APIC, Baloon, PCI (configuration space etc) и сеть. Процессы, полноценный IP-стек и юзермод не нужны - пусть будет 1 поток per VM c одним "raw сокетом", на таком "node.rs for DOS" можно налепить юзермод-TCP и остальные ф-ции получать через p9-образный протокол от сервера на Linux-виртуалке, играющего роль микроядра.

Далее нам надо какой-то рантайм, который не требует реализации позикс-говна. Как ни странно, таких рантаймов 3 - это Си, С++ и rust. Си нам понадобится в хардкорных местах, в-основном же хватит Rust LibCore.

Если мы берём Rust - то есть достаточно прямолинейный вариант с RumpRun Rust. Это Rust unikernel на основе кодобазы netbsd, позволяющий запускать "полный" Rust std (даже не core). Дальше есть хардкорные (aka нерабочие) кодобазы rustboot и robigalia, из которых можно слепить "совершенно пустой юникернел" (т.е. без netbsd-кода) с памятью, APIC и PCI, и заняться портированием virtio на раст (дабы не было соблазна делать всё юникс-вэй можно взять нейтральный сюжет, рекомендованный детям дошкольного возраста - виндовые дрова). Понятно что хороший программист сделает себе позикс над любым системным апи, но это лечится административными пиздюлями aka code review. Нет сомнений, что в результате получится говно. Но зато _маленькое_ говно!

После virtio-net мы можем уже сделать дебильный недо-tcp, даже не сделав arp и демультиплексор, и тестить концептуальный клиент-сервер.

Ну а дальше задача скрестить ежа с этим недоужом. Т.е. сделать некий рантайм на расте, в пределе GHC-подобный в плане зеленых потоков, со сборкой мусора, и компилить под него из ФЯ с опциональной верификацией. А если не делать, а найдется готовый - то можно и на сях, главное чтобы был достаточно изолированный от POSIX-анахронизмов и весь из себя по-хипсторски бородатый!

Bitcoin Proof of Work in Pure Lambda Calculus

2017-12-01T17:33:11+00:00

From command line to MLC:

$ npm i -g @alexo/lambda
└── @alexo/lambda@0.3.6

$ node work2mlc.js getwork.json 381353fa | tee test.mlc
Mid = x: x
        hex(24e39e50)
        hex(1efebbc8)
        hex(fb545b91)
        hex(db1ff3ca)
        hex(a66f356d)
        hex(7482c0f3)
        hex(acc0caa8)
        hex(00f10dad);

Data = x: x
        hex(a7f5f990)
        hex(fd270c51)
        hex(378a0e1c);

Nonce = hex(381353fa);

Zero32 (Pop 8 (RunHash Mid Data Nonce))
$ lambda -pem lib.mlc -f test.mlc
3335648(653961), 17837 ms
v1, v2: v1
$

https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487

comments

Implementation of SHA-256 in Macro Lambda Calculus

2017-11-24T21:18:18+00:00

https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487

$ npm i -g @alexo/lambda
└── @alexo/lambda@0.3.6

$ make
	shasum -a 256 /dev/null
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  /dev/null
	lambda -pem lib.mlc 'Pri32 hex(e3b0c442)'
857(230), 19 ms
_1 _1 _1 _0 _0 _0 _1 _1 _1 _0 _1 _1 _0 _0 _0 _0 _1 _1 _0 _0 _0 _1 _0 _0 _0 _1 _0 _0 _0 _0 _1 _0
	lambda -pem lib.mlc 'Pri32 (Shift 8 (Hash1 NullMsg))'
3247721(688463), 17211 ms
_1 _1 _1 _0 _0 _0 _1 _1 _1 _0 _1 _1 _0 _0 _0 _0 _1 _1 _0 _0 _0 _1 _0 _0 _0 _1 _0 _0 _0 _0 _1 _0
	shasum -a 256 </dev/null | xxd -r -p | shasum -a 256
5df6e0e2761359d30a8275058e299fcc0381534545f55cf43e41983f5d4c9456  -
	lambda -pem lib.mlc 'Pri32 hex(5df6e0e2)'
856(230), 15 ms
_0 _1 _0 _1 _1 _1 _0 _1 _1 _1 _1 _1 _0 _1 _1 _0 _1 _1 _1 _0 _0 _0 _0 _0 _1 _1 _1 _0 _0 _0 _1 _0
	lambda -pem lib.mlc 'Pri32 (Shift 8 (Hash2 NullMsg))'
6448027(1373506), 38750 ms
_0 _1 _0 _1 _1 _1 _0 _1 _1 _1 _1 _1 _0 _1 _1 _0 _1 _1 _1 _0 _0 _0 _0 _0 _1 _1 _1 _0 _0 _0 _1 _0
$

comments

"Зависимые" "типы"

2017-11-21T05:32:23+00:00

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

Слово "типы" зашкварилось тогда, когда Рассел его забыл запатентовать, и его начали использовать для чего попало. Слово "лямбда" зашкварилось, когда Маккарти его украл у Чёрча, забывшего запатентовать. Даже слово "рекурсия" имхо зашкварено рекурсивными программами, т.к. Гёдель его забыл запатентовать. Более свежие зашквары - "нетотальность" зашкварена своим применением для обозначения чего попало. Слово "исчисление" законтачено интегральным исчислением, причём это редкий случай, когда в английском хуже, чем в русском.

Короче, туториалы по непонятным вещам ака НЁХ надо писать такими словами, чтобы не вызывать ложных аллюзий. Где-то видел пародийное объяснение устройства Saturn V словами, понятными ребёнку.

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

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

- "семантический паскаль"
- "семантическая джава"
- "семантическая луа"

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

Наша игра в подстановки - это не футбол, не дота и не шахматы, а скорее пасьянс, причём ближе к пауку с 4 мастями, которого почему-то все боятся. Программа на семантическом ершове играет роль колоды. Далее компьютер раскладывает эту колоду на игровом поле, а задача человека её сложить. Компьютер, как и в обычном пауке, следит за правилами и дает нам "читы" вроде возможности откатить и переиграть с любого места. Причём если получилось - то у нас не салют, а гарантия того, что в исходном ершове ни один ассерт не сработает. Это не так много, но считается, что этого достаточно, чтобы самолёты не убирали шасси стоя на земле и спутники не отворачивали антенны.

Педагогическая польза этой белиберды в том, что мы заявляем, что паук - это не язык программирования и не язык спецификаций, а некая логика/inference system. Что позволяет абстрагироваться от понятия компайл-рантайма, типов-значений, переменных, времени и т.п. и сосредоточиться на soundness. Т.е. сразу отметаются идеи "добавить в паук присваивание", т.к. любая модификация должна сохранять нашу гарантию.

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

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

И понятно, что формальная система паука не должна в общем случае походить на язык программирования - скажем, discharge of proof obligations by an smt solver or a non-constructive prover достаточно сильно не похоже на чисто функциональную трансляцию исходного ершова.

Далее, мы фокусируемся исключительно на статической семантике паука. И считаем, что у нас просто такое компайл-тайм перекладывание кусков текста программы на языке Ершова, т.е. у нас смешаны не типы и значения, а вспомогательные конструкции паука и фрагменты текста.

То есть к примеру, мы говорим студенту, что сигма-тип - это не тапл, тип второго элемента которого зависит от рантайм-значения содержащегося в первом элементе, а просто такая хитрая синтаксическая подстановка. Т.е. вот у нас есть (x: A) * B x и это просто 2 куска текста, в котором есть "локальный" кусок, обозначенный "буквой" x, который фигурирует (т.е. "подставлен") сразу во многих местах (подстановка B может быть "сколь угодно нелинейной"). И что эта конструкция нужна, чтобы "давать хинты" движку "пасьянса", какие синтаксические куски у нас "текстуально равны", чтобы ему было легче следить за правилами.

С пями та же самая история но в профиль, а лямбды \(x: A) -> ... - это просто способ изготавливать вторые компоненты-подстановки в сигмах (x: A) * B x и пях (x: A) -> B x

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

C индуктивными типами при таком педагогическом подходе тоже становится понятнее. Нам вообще плевать что у нас есть натуральные которые демонстрируют вычислительную мощь натуральных. Нам важно, что мы можем использовать мощь индукции при манипуляциях в пасьянсе. То есть, нам плевать на обычные элиминаторы, но критически важно (soundness all the way down!), чтобы были индуктивные элиминаторы, традиционно зашкваренно называемые "зависимыми". То есть, чтобы у нас была _доказательная_ мощь _аксиоматической теории_ натуральных, а на вычисление тотальных функций между натуральными нам по большому счёту плевать (и "в самолётах"/ершове натуральных всё равно нету, ибо анальное рабство хард реалтайма и всё преаллоцировано)

Паттерн Model-Update-View и зависимые типы

2017-11-20T10:56:32+00:00

Написал статью на Хабре о том, чего нет в Elm.
Кто не может комментировать там, могут комментировать здесь.

binnat.ctt

2017-11-20T00:32:59+00:00

nponeccop импортнул, я померял.

data binN = binN0 | binNpos (p : pos)

NtoBinN : nat -> binN = split
  zero  -> binN0
  suc n -> binNpos (NtoPos (suc n))

doublesN : nat -> nat -> nat = split
  zero  -> \(m:nat) -> m
  suc n -> \(m:nat) -> doublesN n (doubleN m)

Это мгновенно (транспортная decode):

> let a: binN = NtoBinN (doublesN n10 n10) in a
Checking: a
EVAL: binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x1 (x0 pos1)))))))))))))

Это долго (минуты, через isoPath):

> let a: binN = transNeg binN nat PathbinNN (doublesN n10 n10) in a
Checking: a
EVAL: binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x1 (x0 pos1)))))))))))))

Доказательство, что 2^20 * e = 2^5 * (2^15 * e), мгновенно.

data Double =
  D (A : U)            -- carrier
    (double : A -> A)  -- doubling function computing 2 * x
    (elt : A)          -- element to double

carrier : Double -> U = split D c _ _ -> c

iter (A : U) : nat -> (A -> A) -> A -> A = split
  zero  -> \(f:A->A) (z:A) -> z
  suc n -> \(f:A->A) (z:A) -> f (iter A n f z)

double : (D : Double) -> (carrier D -> carrier D)
 = split D _ op _ -> op

doubles (D : Double) (n : nat) (x : carrier D) : carrier D =
  iter (carrier D) n (double D) x

propDouble (D : Double) : U
 = Path (carrier D) (doubles D n20 (elt D))
                    (doubles D n5 (doubles D n15 (elt D)))

bin1024 : binN = binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))

doublesBinN : nat -> binN -> binN = split
  zero  -> \(m:binN) -> m
  suc n -> \(m:binN) -> doublesBinN n (doubleBinN m)

DoubleBinN : Double = D binN doubleBinN bin1024

propBin : propDouble DoubleBinN = _> doublesBinN n20 (elt DoubleBinN)

> :n propDouble
NORMEVAL: \(D : Double) -> PathP ( carrier D) (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (elt D))))))))))))))))))))) (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (double D (elt D)))))))))))))))))))))

> :n propBin
NORMEVAL:  binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))))))))))))))))))))))

Книга про моделирование и Haskell

2017-11-11T13:52:54+00:00

Здесь тоже поделюсь. Написал книгу про имитационное моделирование с той точки зрения, как я это реализовал на языке Haskell в своем комплексе программных библиотек Айвика. Книгу назвал «Aivika: Computation-based Modeling and Simulation in Haskell».

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

http://aivikasoft.com/downloads/aivika/aivika.pdf

https://github.com/dsorokin/dsorokin.github.io/blob/master/downloads/aivika/aivika.pdf

Книга охватывает последовательное моделирование, параллельное и распределенное моделирование, а также вложенное моделирование. Фокус на дискретно-событийном моделировании, прежде всего, процесс-ориентированной парадигме, которая сводится на уровне реализации к событийно-ориентированной.

Начну представлять книгу с конца.

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

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

Главная же часть книги описывает основные концепции дискретно-событийного моделирования применительно к последовательной имитации. Дискретные события, дискретные процессы, ресурсы, вытеснение ресурса, очереди и т.д. Но очень важно заметить, что практически все это работает и в случае распределенного моделирования, и вложенного моделирования, включая GPSS-подобный предметно-ориентированный язык, который тоже бегло описан.

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

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

В общем, приглашаю к прочтению. Книга о том, как можно использовать мой комплекс библиотек Айвика для решения самых разных задач имитационного моделирования. Есть только один нюанс. Для охвата более широкой аудитории я решил написать книгу на английском языке.

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

Унивалентность на кубических типах

2017-11-08T05:08:32+00:00

https://github.com/mortberg/cubicaltt/tree/master/lectures (там же чекер на х-е) позволяет понять, как примерно будет выглядеть обещанное Воеводским счастье ("his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant")

Идея заключается в том, чтобы усилить identity type так, чтобы больше вещей можно было доказать "в одно действие" через аналог идрисовского replace (названный в лекциях subst):

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

Для этого из ~~гомосексуальных~~ гомологических примитивов собирается тип Path X a b, играющий роль {X} -> (a: X) = (b: X), который можно населить:

- "рефлом", т.е. definitionally equal terms

refl (A : U) (a : A) : Path A a a

- экстенсионально равными функциями (версия для dependent product тоже есть)

funExtNonDep (A B: U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) : Path (A -> B) f g

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

isoPath (A B : U) (f : A -> B) (g : B -> A)
      (s : (y : B) -> Path B (f (g y)) y)
      (t : (x : A) -> Path A (g (f x)) x) : Path U A B

Интересно, что всё это работает и с функциями уровня типов.

В результате можно написать такую функцию:

functor_transport (F G: U -> U) (p: Path (U -> U) F G) (f: functor F): functor G
  = subst (U -> U) functor F G p f

То есть, для изоморфных типов F и G (с кайндами * -> * в терминах х-я) по инстансу функтора для F можно родить инстанс для G, при этом тело и сигнатуры fmap и теоремы о соблюдении законов функтора переписываются "автомагически".

Ну а дальше оказывается, что изоморфизмы у нас повсеместно. Скажем, таплы у самоизоморфны - т.е. есть Path U (A, B) (B, A), ну и из (first, fst, functorForA) "в одно действие" получаются (second, snd, functorForB). А дальше из (first, fst, functorForA, second, snd, functorForB) "в одно действие" получается реализация 6 функций и док-во 4 теорем (1 ф-ция и 2 теоремы внутри functorA/B сидят) для пар в кодировках чёрча и остальных over 9000 возможных представлений пар.

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

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

data food = cheese | beef | chicken

-- Predicate encoding which food someone eats
eats (X : U) : U = list (and food X)

anders : eats bool = cons (cheese,true)
                    (cons (beef,false)
                    (cons (chicken,false) nil))

-- Cyril eats the complement of Anders
cyril : eats bool = substEquiv eats bool bool notEquiv anders

notEquiv тут как раз доказательство изоморфизма. Ну и понятно что заменяются не все вхождения Bool, а "все вхождения в позициях, отмеченных Х". Любопытно, что код ничего не знает о том как обходить списки - у нас нету fmap для eats :)

Дебильные комментарии, комментарии "практиков" и школьников - как обычно, скринятся. RTFM, do you homework, пиши развёрнуто и конструктивно! https://t.me/groupoid (но там банхаммер, так что лучше сюда)

Cubical Parser in Erlang

2017-11-07T21:08:04+00:00

Сделано все, кроме гомотопических прититивов <> @ []. Вернулись на позапрошлогодний уровень EXE. Пришлось сделать case аналисис в стиле ML языков (с палками), так как, говорят 2D синтаксис голым эрланговским LALR не возьмешь. С where тоже проблемы, пришлось делать карированую версию where. Оно и логично — в минималистичных ядрах должно быть все карированое. YECC файл занимает ровно 50 строчек, в отличие от 261 строки для EXE. В примере показан Хрономирфизм и Категорная Семантика односвязного списка

module lam1 where

listCategory (A: U) (o: listObject A): U = undefined

histo (A:U) (F: U -> U) (X: functor F) (f: F (cofree F A) -> A) (z: fix F): A
  = extract A F ((cata (cofree F A) F X (\(x: F (cofree F A)) -> CoFree (Fix (CoBindF (f x) ((X.1 (cofree F A) (fix (cofreeF F A)) (uncofree A F) x)))))) z) where
  extract (A: U) (F: U -> U): cofree F A -> A = split
    | CoFree f -> unpack_fix f where
  unpack_fix: fix (cofreeF F A) -> A = split
    | Fix f -> unpack_cofree f where
  unpack_cofree: cofreeF F A (fix (cofreeF F A)) -> A = split
    | CoBindF a -> a

futu (A: U) (F: U -> U) (X: functor F) (f: A -> F (free F A)) (a: A): fix F
  = Fix (X.1 (free F A) (fix F) (\(z: free F A) -> w z) (f a)) where
  w: free F A -> fix F = split
    | Free x -> unpack x where
  unpack_free: freeF F A (fix (freeF F A)) -> fix F = split
    | ReturnF x -> futu A F X f x
    | BindF g -> Fix (X.1 (fix (freeF F A)) (fix F) (\(x: fix (freeF F A)) -> w (Free x)) g) where
  unpack: fix (freeF F A) -> fix F = split
    | Fix x -> unpack_free x

chrono (A B: U) (F: U -> U) (X: functor F)
       (f: F (cofree F B) -> B)
       (g: A -> F (free F A))
       (a: A): B = histo B F X f (futu A F X g a)

listAlg (A : U) : U
    = (X: U)
    * (nil: X)
    * (cons: A -> X -> X)
    * Unit

listMor (A: U) (x1 x2: listAlg A) : U
    = (map: x1.1 -> x2.1)
    * (mapNil: Path x2.1 (map (x1.2.1)) (x2.2.1))
    * (mapCons: (a:A) (x: x1.1) -> Path x2.1 (map (x1.2.2.1 a x)) (x2.2.2.1 a (map x)))
    * Unit

listObject (A: U) : U
    = (point: (x: listAlg A) -> x.1)
    * (map: (x1 x2: listAlg A)
            (m: listMor A x1 x2) ->
            Path x2.1 (m.1 (point x1)) (point x2))
    * Unit

{module,{id,1,"lam1"},
        {where,1},
        [],
        [{def,{id,5,"listCategory"},
              {tele,[{id,5,"A"}],
                    {id,5,"U"},
                    {tele,[{id,5,"o"}],{app,{id,5,"listObject"},{id,5,"A"}},[]}},
              {id,5,"U"},
              {id,5,"undefined"}},
         {def,{id,7,"histo"},
              {tele,[{id,7,"A"}],
                    {id,7,"U"},
                    {tele,[{id,7,"F"}],
                          {pi,{id,7,"U"},{id,7,"U"}},
                          {tele,[{id,7,"X"}],
                                {app,{id,7,"functor"},{id,7,"F"}},
                                {tele,[{id,7,[...]}],
                                      {pi,{app,...},{...}},
                                      {tele,[...],...}}}}},
              {id,7,"A"},
              {app,{app,{app,{id,8,"extract"},{id,8,"A"}},{id,8,"F"}},
                   {app,{app,{app,{app,{app,{id,8,[...]},{app,{...},...}},
                                       {id,8,"F"}},
                                  {id,8,"X"}},
                             {app,{lam,{tele,[{id,...}],{app,...},[]},{id,8,[...]}},
                                  {app,{id,8,[...]},{app,{...},...}}}},
                        {id,8,"z"}}},
              {def,{id,9,"extract"},
                   {tele,[{id,9,"A"}],
                         {id,9,"U"},
                         {tele,[{id,9,"F"}],{pi,{id,9,[...]},{id,9,...}},[]}},
                   {pi,{app,{app,{id,9,"cofree"},{id,9,"F"}},{id,9,"A"}},
                       {id,9,"A"}},
                   {split,[{br,[{id,10,"CoFree"},{id,10,[...]}],
                               {app,{id,10,...},{id,...}}}]},
                   {def,{id,11,"unpack_fix"},
                        [],
                        {pi,{app,{id,...},{...}},{id,11,...}},
                        {split,[{br,...}]},
                        {def,{id,...},[],...}}}},
         {def,{id,16,"futu"},
              {tele,[{id,16,"A"}],
                    {id,16,"U"},
                    {tele,[{id,16,"F"}],
                          {pi,{id,16,"U"},{id,16,"U"}},
                          {tele,[{id,16,"X"}],
                                {app,{id,16,"functor"},{id,16,[...]}},
                                {tele,[{id,16,...}],{app,{...},...},{tele,...}}}}},
              {app,{id,16,"fix"},{id,16,"F"}},
              {app,{id,17,"Fix"},
                   {app,{app,{app,{app,{fst,{id,17,...}},{app,{app,...},{...}}},
                                  {app,{id,17,[...]},{id,17,...}}},
                             {lam,{tele,[{id,17,...}],{app,{...},...},[]},
                                  {app,{id,17,...},{id,...}}}},
                        {app,{id,17,"f"},{id,17,"a"}}}},
              {def,{id,18,"w"},
                   [],
                   {pi,{app,{app,{id,18,"free"},{id,18,[...]}},{id,18,"A"}},
                       {app,{id,18,"fix"},{id,18,"F"}}},
                   {split,[{br,[{id,19,[...]},{id,19,...}],
                               {app,{id,...},{...}}}]},
                   {def,{id,20,"unpack_free"},
                        [],
                        {pi,{app,{...},...},{app,...}},
                        {app,{split,...},{...}},
                        {def,{...},...}}}},
         {def,{id,26,"chrono"},
              {tele,[{id,26,"B"},{id,26,"A"}],
                    {id,26,"U"},
                    {tele,[{id,26,"F"}],
                          {pi,{id,26,"U"},{id,26,"U"}},
                          {tele,[{id,26,"X"}],
                                {app,{id,26,[...]},{id,26,...}},
                                {tele,[{id,...}],{pi,...},{...}}}}},
              {id,29,"B"},
              {app,{app,{app,{app,{app,{id,29,"histo"},{id,29,[...]}},
                                  {id,29,"F"}},
                             {id,29,"X"}},
                        {id,29,"f"}},
                   {app,{app,{app,{app,{app,{id,...},{...}},{id,29,...}},
                                  {id,29,"X"}},
                             {id,29,"g"}},
                        {id,29,"a"}}}},
         {def,{id,31,"listAlg"},
              {tele,[{id,31,"A"}],{id,31,"U"},[]},
              {id,31,"U"},
              {sigma,{tele,[{id,32,"X"}],{id,32,"U"},[]},
                     {sigma,{tele,[{id,33,"nil"}],{id,33,"X"},[]},
                            {sigma,{tele,[{id,34,...}],{pi,{...},...},[]},
                                   {id,35,"Unit"}}}}},
         {def,{id,37,"listMor"},
              {tele,[{id,37,"A"}],
                    {id,37,"U"},
                    {tele,[{id,37,"x2"},{id,37,"x1"}],
                          {app,{id,37,"listAlg"},{id,37,"A"}},
                          []}},
              {id,37,"U"},
              {sigma,{tele,[{id,38,"map"}],
                           {pi,{fst,{id,38,[...]}},{fst,{id,38,...}}},
                           []},
                     {sigma,{tele,[{id,39,"mapNil"}],
                                  {app,{app,{...},...},{fst,...}},
                                  []},
                            {sigma,{tele,[{id,...}],{app,...},[]},{id,41,[...]}}}}},
         {def,{id,43,"listObject"},
              {tele,[{id,43,"A"}],{id,43,"U"},[]},
              {id,43,"U"},
              {sigma,{tele,[{id,44,"point"}],
                           {pi,{tele,[{id,...}],{app,...},[]},{fst,{id,...}}},
                           []},
                     {sigma,{tele,[{id,45,[...]}],{app,{app,...},{...}},[]},
                            {id,48,"Unit"}}}}]}

В тред приглашаются специалисты по LALR парсерам.
_______________
[1]. https://github.com/groupoid/infinity/blob/master/src/cub_parser.yrl

Любые имена и ключ -m в MLC

2017-11-04T02:06:59+00:00

Лямбда стала веселее!

$ npm i -g @alexo/lambda@0.2.8
└── @alexo/lambda@0.2.8 

$ cat фубля.mlc 
I = x: x;
K = x, y: x;
T = K;
F = K I;
NOT = p, a, b: p b a;
+ = m, n: f, x: m f (n f x);
* = m, n: f: m (n f);
^ = m, n: n m;
0 = F;
1 = I;
2 = + 1 1;
3 = + 1 2;
4 = ^ 2 2;
5 = + 2 3;
6 = * 2 3;
7 = + 3 4;
8 = ^ 2 3;
9 = ^ 3 2;
10 = * 2 5;
1000 = ^ 10 3;
четно = n: n NOT T;
$ alias лямбда="lambda -pm фубля.mlc"
$ лямбда 'четно (^ 9 1000) да. нет. и чо?'
48363(8123), 324 ms
нет. и чо?
$ лямбда 'четно (^ 10 1000) да. нет. и чо?'
55403(10146), 384 ms
да. и чо?
$

Вот так играешься, играешься, и доиграешься до P = NP.

comments

List Eliminator and Case Analysis in Pure Functions

2017-10-31T12:00:14+00:00

-- List/@
  λ (A : *)
→ ∀ (List: *)
→ ∀ (Cons: A → List → List)
→ ∀ (Nil: List)
→ List

-- List/Cons
  λ (A: *)
→ λ (Head: A)
→ λ (Tail:
    ∀ (List: *)
  → ∀ (Cons: A -> List -> List)
  → ∀ (Nil: List)
  → List)
→ λ (List: *)
→ λ (Cons: A -> List -> List)
→ λ (Nil: List)
→ Cons Head (Tail List Cons Nil)

-- List/Nil
  λ (A: *)
→ λ (List: *)
→ λ (Cons: A -> List -> List)
→ λ (Nil: List)
→ Nil

-- List/cond
   \ (a : *)
-> \ (x: \/ (r : *) -> (a -> r -> r) -> r -> r)
-> x

-- List/match
   \ (A: *)
-> \ (value: #List/@ A)
-> \ (ret: *)
-> \ (cons_branch: ret)
-> \ (nil_branch: ret)
-> #List/cond A value ret
              (\(_:A)->\(_:ret)-> cons_branch)
              nil_branch

-- List/match.test
#List/match #Nat/@ (#List/Nil #Nat/@)
            #Nat/@ #Nat/Two #Nat/Five

-- List/match.test2
#List/match #Nat/@ (#List/Cons #Nat/@ #Nat/Zero (#List/Nil #Nat/@))
            #Nat/@ #Nat/Two #Nat/Five

> ch:unnat('List':'match.test2'()).
2
> ch:unnat('List':'match.test'()).
5

Доказательство коммутативности в кубике

2017-10-31T04:51:42+00:00

Если кратно, то индукция, индуктивные типы с приходом гомотопических пруверов кажутся уж не таким и сильными инструментами. Покажем на примере коммутативности сложения для двух и трех аргументов.

Доказательство коммутативности сложения курильщика

Theorem plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' Sn' ].
  - simpl. rewrite <- plus_n_0. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite <- Sn'. reflexivity.
Qed.

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n as [| n' Sn' ].
  - simpl. reflexivity.
  - simpl. rewrite <- Sn'. reflexivity.
Qed.

Доказательство коммутативностит сложения нормального человека

add_comm (a : nat) : (n : nat) -> Path nat (add a n) (add n a) = split
  zero  -> <i> add_zero a @ -i
  suc m -> <i> comp (<_> nat) (suc (add_comm a m @ i))
                    [ (i = 0) -> <j> suc (add a m)
                    , (i = 1) -> <j> add_suc m a @ -j ]

add_comm3 (a b c : nat) : Path nat (add a (add b c)) (add c (add b a)) =
 let r: Path nat (add a (add b c)) (add a (add c b)) = <i> add a (add_comm b c @ i)
  in <i> comp (<_> nat) ((add_comm a (add c b)) @ i)
              [ (i = 0) -> <j> r @ -j,
                (i = 1) -> (<z> assocAdd c b a @ -z) ]

Клон N2O.hs

2017-10-30T18:09:36+00:00

http://hackage.haskell.org/package/threepenny-gui

Идея та же - вебсокет-сервер с RPC в обратную сторону, т.е. из х-я в б-р.

Причем даже через eval:

https://github.com/HeinrichApfelmus/threepenny-gui/blob/master/js/ffi.js#L78

Оно там на говне и палках, но можно понадергать идей и кода и постепенно унифицировать.

Contracts first

2017-10-30T12:07:56+00:00

Тут из альтернативной вселенной сообщают, что завтипы говно и не нужны.

Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers

Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.

Pure Sigma

2017-10-29T23:27:58+00:00

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

-- Sigma/@
   \ (A: *)
-> \ (P: A -> *)
-> \ (n: A)
-> \/ (Exists: *)
-> \/ (Intro: A -> P n -> Exists)
-> Exists

-- Sigma/Intro
   \ (A: *)
-> \ (P: A -> *)
-> \ (x: A)
-> \ (y: P x)
-> \ (Exists: *)
-> \ (Intro: A -> P x -> Exists)
-> Intro x y

-- Sigma/fst
   \ (A: *)
-> \ (B: A -> *)
-> \ (n: A)
-> \ (S: #Sigma/@ A B n)
-> S A ( \(x: A) -> \(_: B n) -> x )

-- Sigma/snd
   \ (A: *)
-> \ (B: A -> *)
-> \ (n: A)
-> \ (S: #Sigma/@ A B n)
-> S (B n) ( \(_: A) -> \(y: B n) -> y )

-- Sigma/test
-- P: nat -> U = (\(_:nat) -> list nat)
-- mk nat P n5 nil
#Sigma/Intro #Nat/@
             (\(n: #Nat/@) -> #List/@ #Nat/@)
             #Nat/Five
             (#List/replicate #Nat/@ #Nat/Five #Nat/Zero)

-- Sigma/test.fst
-- fst nat P zero test
#Sigma/fst #Nat/@
           (\(n: #Nat/@) -> #List/@ #Nat/@)
           #Nat/Zero
           #Sigma/test

-- Sigma/test.snd
-- snd nat P zero test
#Sigma/snd #Nat/@
           (\(n: #Nat/@) -> #List/@ #Nat/@)
           #Nat/Zero
           #Sigma/test

В тестах создание тапла (nat, list nat) = (5, [0,0,0,0,0]) и взятие у него первой и второй проекции:

1> om:fst(om:erase(om:norm(om:a("#Sigma/test.snd"))))
== om:fst(om:erase(om:norm(om:a("(#List/replicate #Nat/@ #Nat/Five #Nat/Zero)")))).
true
2> om:fst(om:erase(om:norm(om:a("#Sigma/test.fst"))))
== om:fst(om:erase(om:norm(om:a("#Nat/Five")))).
true
3> om:type(om:type(om:a("#Sigma/snd"))).
{star,1}
4> om:type(om:type(om:a("#Sigma/fst"))).
{star,1}

Трюк заключается в протаскивании первого элемента в базу, все равно конструктор один и он же принимает его. Т.е. классическое индуктивное определение

data Sigma (A: Type) (P: A -> Type): Type
   = (intro: (x:A) (y:P x) -> Sigma A P)

сменяется на следующее:

data Sigma (A: Type) (P: A -> Type) (x:A): Type
   = (intro: (y:P x) -> Sigma A P)

Наверн проблемы начнутся как с pred, когда придется закодировать N-тапл из сигм и переносить все кроме последнего в базу, но тоже вроде все законно. Единственное к чему тут можно предъявить претензии — это дополнительный параметр пустышка #Nat/Zero который передается в примерах в качестве (x:A) при вызове элиминаторов, он нужен для совместимости типов, но как видно из примера, экстрактятся из сконструированного тапла #Sigma/Intro настоящие значения (fst test = 5 и snd test = [0,0,0,0,0]). Другими словами это означает что первый элемент типовой пары должен быть как минимум стягиваемым пространством, что в принципе в духе Сигмы и квантора существования. Что думают по этому поводу типовые теоретики?

P.S. Модель в cubicaltt, для тех, кто не доверяет Ом.

module puresigma where
import nat
import list

P: nat -> U = (\(_:nat) -> list nat)
sig (A:U)(P:A->U)(x:A): U = (e:U)->(i:A->P x->e)->e
mk  (A:U)(P:A->U)(x:A)(y:P x)(e:U)(i:A->P x->e):e=i x y
fst (A:U)(P:A->U)(x:A)(s:sig A P x):A=s A(\(z:A)(y:P x)->z)
snd (A:U)(P:A->U)(x:A)(s:sig A P x):P x=s(P x)(\(z:A)(y:P x)->y)

test: sig nat P n5 = mk nat P n5 nil
test_pr1: nat = fst nat P zero test
test_pr2: list nat = snd nat P zero test

> test_pr2
EVAL: nil
> test_pr1
EVAL: suc (suc (suc (suc (suc zero))))

Тут мне подсказывают, что писал Thorsten Altenkirch:

Ok, when we think of homogenous tuples AxA then this can also be understood as a function 2 -> A. This also works for heterogenous tuples like AxB using dependent functions Pi x:2.if x then A else B. However the next logical step is Sigma x:A.B x, which have no good representations as functions (unless we accept very dependent functions which in my mind goes against the spirit of type theory). For this reason it seems to me that the generalisation from -> to Pi and from x to Sigma is the primary one, and the fact that tuples can be represented as functions is secondary.

Позволю себе не согласиться с Торстеном,Альтенкирхом: на мой взгляд, именно Черч кодировка и показывает скрытую категорную стркутуру теории типов обнажая ее самантику, она ни как не может идти в разрез духа тетории типов, которым как раз и является теория категорий.

Существует и другая более общая связь между Пи и Сигмой. Сигму можно интерпретировать как тотальное пространство расслоения B -> A над A. Где расслоение — это терм

section (A B : U) (p : A -> B) (s : B -> A) : U = (y : B) -> Path B (p (s y)) y

А элементы Пи или лямбды — это сечения тривиального расслоения A -> A x B. Симметричной функцией является ретракт:

retract (A B : U) (f : A -> B) (g : B -> A) : U = (a : A) -> Path A (g (f a)) a

Не могу к сожалению (пока) понять, как устроены йоги Гротендика, но это устройство связи Пи и Сигмы помоему две из них и есть.

Надо переписать на кубикал, кто возьмется?

Prerequisites:

_⋔_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
_⋔_ A B = A → B

_⊗_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
_⊗_ A B = A × B

∫↓ : ∀ {a b} {X : Set a} → (X → X → Set b) → Set (a ⊔ b)
∫↓ {X = X} P = ∀ {x} → P x x

∫↑ : ∀ {a b} {X : Set a} → (X → X → Set b) → Set (a ⊔ b)
∫↑ {X = X} P = ∐ [ x ∶ X ] P x x

Левое и правое расширения Кана:

Ran : ∀ {x c v u p} {𝔵 : Set x} {𝔠 : Set c} {𝔳 : Set v}
  → (𝒸 : 𝔠 → 𝔠 → Set u)
  → (_⋔_ : Set u → 𝔳 → Set p)
  → (G : 𝔵 → 𝔠)
  → (H : 𝔵 → 𝔳)
  → (𝔠 → Set (p ⊔ x)) = 𝒸 _⋔_ G H A = ∫↓ λ x y → 𝒸 A (G x) ⋔ H y

Lan : ∀ {x c v u p} {𝔵 : Set x} {𝔠 : Set c} {𝔳 : Set v}
  → (𝒸 : 𝔠 → 𝔠 → Set u)
  → (_⊗_ : 𝔳 → Set u → Set p)
  → (G : 𝔵 → 𝔠)
  → (H : 𝔵 → 𝔳)
  → (𝔠 → Set (p ⊔ x)) = 𝒸 _⊗_ G H A = ∫↑ λ x y → H x ⊗ 𝒸 (G y) A

По сигнатуре видно, что Пи и Сигма — элементы одного пространства.

Sigma: ∀ {x y} {X : Set x} {Y : Set y} → (X → Y) → 𝒫 x X → 𝒫 (x ⊔ y) Y = Ran _≡_ _⋔_ f

Pi:    ∀ {x y} {X : Set x} {Y : Set y} → (X → Y) → 𝒫 x X → 𝒫 (x ⊔ y) Y = Lan _≡_ _⊗_ f

___________
[1]. Расширения Кана Бартоша https://henrychern.files.wordpress.com/2017/10/27.pdf

Зависимые типы и high kind types.

2017-10-27T08:55:20+00:00

Есть вполне полезные языки, не поддерживаюшие HKT - Rust, Elm. Возможно ли (и осмысленно) в подобных языках делать поддержку зависимых типов? Например, Elm справедливо требует тотальности кода, но из-за этого приходится описывать и обрабатывать невозможные ситуации, например когда пользователь еще не залогинился, а уже разлогинивается. Зависимые типы позволяют описать невозможность такого события.

arXiv:1710.07516 [cs.LO]

2017-10-23T02:13:22+00:00

https://arxiv.org/abs/1710.07516

An impure solution to the problem of matching fans

We present an algorithm to solve the problem of matching fans in interaction net implementations of optimal reduction for the pure untyped lambda calculus without use of any additional agent types. The algorithm relies upon a specific interaction nets reduction strategy and involves side effects in one of interaction rules.

comments

Фронт с роботами.

2017-10-20T15:59:59+00:00

В порядке паралельного изучения ELM и ROS состыковал одно с другим.
Хотя в ELM не хватает тайпклассов и макросов, UI на нем пишется поразительно быстро и легко. Я уже просто не понимаю, зачем делать фронтенд на чем либо еще.

My Dream Comes True

2017-10-19T01:54:10+00:00

Optimal reduction without oracle finally shows its ugly face.

I found an impure solution to the problem of matching fans, playing around the ideas from arXiv:1701.04691v2. The solution heavily relies on needed reduction. The trick is to use nonces and a global hash table. The default algorithm in MLC is abstract now, but the only good thing about it is that it is damn fast:

Next up, I need to decide if and how I should describe this hack in a paper.

P. S. Why did I think it would be more exciting?

comments

Дно двунаправленности пробито

2017-10-11T02:08:26+00:00

import System.IO.Streams (contramap)
quux x = do
   foo <- contramap show x
   bar <- contramap Just foo
   return bar

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

Т.е. у нас "вход" как бы снизу, а x - это "выход". return bar отправляет этот вход в bar, дальше он проходит Just и отправляется в foo, а оттуда проходит через show и попадает в x

Тип соответствующий:

quux :: Show a => OutputStream String -> IO (OutputStream a)

a "на входе", затем Just делает Maybe a, и show делает строку.

neovim + haskell-ide-engine

2017-10-10T07:48:42+00:00

Всё как обычно.

1. Даже не билдится (happy не находит). Билдится после доводки напильником. Инструкция по сборке на сайте не тестировалась.

2. После сборки всё запускается и стартует (в pstree виден hie), но ничего не происходит. Один раз как-то получилось от него ошибку компиляции получить.

Надо разбираться дальше.

концепция итераторов

2017-10-07T10:54:15+00:00

Попытался разобраться с Traversable в Хаскелле. Но понял что надо начать хотя бы с "Аппликативных функторов". Начал смотреть последних и набрел на следующую статью:

"The Essence of the Iterator Pattern",
Jeremy Gibbons and Bruno C. d. S.
Oliveira Oxford University Computing Laboratory

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