Russian Lambda Planet

12 марта 2018

nponeccop

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

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

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

12 марта 2018, 19:37

03 марта 2018

nponeccop

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

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

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

03 марта 2018, 23:30

Alexey Romanov

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

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

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

03 марта 2018, 19:33

16 февраля 2018

29 января 2018

Dee Mon journal

ну всё теперь



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

29 января 2018, 05:18

27 января 2018

nponeccop

State of the Haskell ecosystem

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

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

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

27 января 2018, 22:42

24 января 2018

nponeccop

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

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

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

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

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

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

24 января 2018, 15:25

23 января 2018

nponeccop

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

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

Берем 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 - внезапно не провалы

23 января 2018, 20:04

13 января 2018

David Sorokins WebLog

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

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

написал dsorokin (noreply@blogger.com) 13 января 2018, 08:11

03 января 2018

rssh

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

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

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

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

03 января 2018, 10:15

25 декабря 2017

Scala@livejournal.com

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

Можно ли в 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)] я не нашел. Это вообще возможно?

написал Mike Potanin (mpotanin@gmail.com) 25 декабря 2017, 16:33

21 декабря 2017

Максим Сохацкий

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

Поки ми готуємо документи, якими ми намагатимемось бомбардувати наші корумповані прикордонні служби, прокуратуру та інші установи, на які тільки у нас вистачить грошей, у зв'язку з недопуском в Україну видатного математика-педагога, дійсного члена комітету по стандартизації мови 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 на вашу думку. Фактично будь-яка робота, якщо детально її проаналізувати це мімікрія під головного Програмолога України.

21 декабря 2017, 08:04

19 декабря 2017

Dee Mon journal

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

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

19 декабря 2017, 17:00

18 декабря 2017

Dee Mon journal

fooling people with theorem provers

Занятный доклад на свежем 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), молодец.

18 декабря 2017, 12:32

11 декабря 2017

nponeccop

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

Отседова: 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"]
    ]
Это вам не таблички "как работает == в джаваскрипте" по карманам тырить!

11 декабря 2017, 07:30

03 декабря 2017

nponeccop

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

http://uhsure.com/halvm3.html

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

03 декабря 2017, 02:32

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

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

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

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-анахронизмов и весь из себя по-хипсторски бородатый!

03 декабря 2017, 02:11

21 ноября 2017

nponeccop

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

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

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

Короче, туториалы по непонятным вещам ака НЁХ надо писать такими словами, чтобы не вызывать ложных аллюзий. Где-то видел пародийное объяснение устройства 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!), чтобы были индуктивные элиминаторы, традиционно зашкваренно называемые "зависимыми". То есть, чтобы у нас была _доказательная_ мощь _аксиоматической теории_ натуральных, а на вычисление тотальных функций между натуральными нам по большому счёту плевать (и "в самолётах"/ершове натуральных всё равно нету, ибо анальное рабство хард реалтайма и всё преаллоцировано)

21 ноября 2017, 05:32

20 ноября 2017

Mike Potanin

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

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

20 ноября 2017, 10:56

Максим Сохацкий

binnat.ctt

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))))))))))))))))))))))))))))))

20 ноября 2017, 00:32

11 ноября 2017

David Sorokins WebLog

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

Здесь тоже поделюсь. Написал книгу про имитационное моделирование с той точки зрения, как я это реализовал на языке 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-подобный предметно-ориентированный язык, который тоже бегло описан.

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

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

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

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

написал dsorokin (noreply@blogger.com) 11 ноября 2017, 13:52

08 ноября 2017

nponeccop

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

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 (но там банхаммер, так что лучше сюда)

08 ноября 2017, 05:08

07 ноября 2017

Максим Сохацкий

Cubical Parser in Erlang

Сделано все, кроме гомотопических прититивов <> @ []. Вернулись на позапрошлогодний уровень 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

07 ноября 2017, 21:08

31 октября 2017

Максим Сохацкий

List Eliminator and Case Analysis in Pure Functions

-- 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

31 октября 2017, 12: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) ]

31 октября 2017, 04:51

30 октября 2017

nponeccop

Клон N2O.hs

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

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

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

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

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

30 октября 2017, 18:09

Contracts first

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

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

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

30 октября 2017, 12:07

29 октября 2017

Максим Сохацкий

Pure Sigma

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

-- 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

29 октября 2017, 23:27

27 октября 2017

ru_deptypes

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

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

написал Mike Potanin (mpotanin@gmail.com) 27 октября 2017, 08:55

20 октября 2017

Mike Potanin

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

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

20 октября 2017, 15:59

11 октября 2017

nponeccop

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

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 делает строку.

11 октября 2017, 02:08

10 октября 2017

nponeccop

neovim + haskell-ide-engine

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

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

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

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

10 октября 2017, 07:48

07 октября 2017

rvp74

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

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

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


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

07 октября 2017, 10:54

nponeccop

acme-kohirnt

Колонка аппликатива в таблице оказывается лишней: единственная операция *> эквивалентна >>. То есть, можно (в альтернативной прелюде) всё переименовать: (Monad.>>) выкинуть, а *> переименовать для единообразия в >>.

Тогда получаем единообразную матрицу 3х3 (две матрицы, если считать флипнутую версию с <=| и т.п.):

module Acme.Kohirnt(
-- |..    >..    $..
  (|=>), (>=>), ($=>), -- .=>
  (|>=), (>>=), ($>=), -- .>=
  (|>),  (>>),  ($>),  -- .>
) where

import Prelude hiding ((>>))
import Control.Monad ((>=>))
import Data.Functor (($>))
import Control.Category ((>>>))
import Data.Function ((&))

(|>) :: a -> b -> b
(|>) = flip const

(|=>) :: (a -> b) -> (b -> c) -> a -> c
(|=>) = (>>>)

(|>=) :: a -> (a -> b) -> b
(|>=) = (&)

($>=) :: Functor f => (a -> b) -> f a -> f b
($>=) = (<$>)

($=>) :: Functor f => (a -> b) -> (b -> c) -> f a -> f c
g $=> f =  ($>=) (g $=> f)   -- fmap (g >>> f)

(>>) :: Applicative f => f a -> f b -> f b
(>>) = (*>)

07 октября 2017, 04:24

Атакуем ApplicativeApplication

Ещё направление аналогий:

pure = zipWith0 = fmap0
fmap = zipWith1 = fmap1
liftA2 = zipWith2 = fmap2

Ну, и аргумент у liftA2 оказывается излишним, его можно заменить таплом:

class Functor f => Applicative' f where
  pure' :: a -> f a
  liftA2' :: f a -> f b -> f (a, b)
оказывается эквивалентен обычному аппликативу.

Всё равно ничего не понятно.

07 октября 2017, 03:44

03 октября 2017

nponeccop

Синтаксический перец rdo-нотации

А давайте для
foo = (\bar -> quux) =<< baz
сделаем
foo = rdo
   quux
   bar <- baz
!

В этом направлении, можно пойти дальше и сделать функциональную ду-нотацию:
y = fdo
 x
 g
 f
как сахар для
y = f (g x)
и
z = frdo
 f
 g
 x
как сахар для
x & g & f
Есть кстати http://taylor.fausak.me/flow/ идущая в этом направлении:
x |> f = x & f
f <| x = f $ x
We need to go deeper™!
x |>= f = x & f
x |> f = f
f |>=> g = f >>> g


- значения Functor Applicative Monad
Application x |>= f x $>= f x *>= f x >>= f
Sequencing x |> y x $> y x *> y x >> y
Composition g |=> f g $=> f g *=> f g >=> f



- значения Functor Applicative Monad
Application a -> (a -> b) -> b f a -> (a -> b) -> f b x *>= f m a -> (a -> m b) -> m b
Sequencing a -> b -> b f a -> b -> f b f a -> f b -> f b f a -> f b -> f b
Composition (a -> b) -> (b -> c) -> a -> c (a -> b) -> (b -> c) -> f a -> f c g *=> f (a -> f b) -> (b -> f c) -> a -> f c

03 октября 2017, 00:43

02 октября 2017

nponeccop

К вопросу о Haskell IDE

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

https://www.stackage.org/haddock/lts-9.6/attoparsec-0.13.1.0/src/Data.Attoparsec.Combinator.html#try

02 октября 2017, 22:01

Cмешные прыжки "каретки"

К вопросу о перемежении правостороннего и левостороннего кода в х-е. Я тут шутку придумал, но нужен кто-то, кто знает левосторонний язык, дабы не было хатуль мадана (он же калитка законопроект). Идея переписать данный код на кейворды на левостороннем языке. Т.е. чтобы OPEN OUTPUT SupplierFile. превратилось в

.SupplierFile פלט פתוח 
(но с нормальным переводом). Cобственно код на коболе:

PROCEDURE DIVISION.
Begin.
    OPEN OUTPUT SupplierFile.
    OPEN INPUT SupplierFileSeq.
    
    READ SupplierFileSeq 
        AT END SET EndOfFile TO TRUE
    END-READ
    PERFORM UNTIL EndOfFile
       MOVE SupplierCodeSeq TO SupplierKey
       MOVE SupplierRecordSeq TO SupplierRecord
       WRITE SupplierRecord
          INVALID KEY DISPLAY "Supplier status = " SupplierStatus
       END-WRITE
       READ SupplierFileSeq 
            AT END SET EndOfFile TO TRUE
       END-READ
    END-PERFORM.    

    CLOSE  SupplierFile, SupplierFileSeq.
    STOP RUN.
Интересно кстати, это только в иврите так курсор смешно прыгает на цифрах?

02 октября 2017, 18:54

30 сентября 2017

nponeccop

Почему Prelude говно

Ввиду наличия 26+ разных NIH-прелюд хорошо бы создать свою 27-ю перечислить недостатки, настоящие или мнимые, которые эти прелюды исправляют или "исправляют".

Потребление процессора и памяти:

- String
- Array

Семантика, недружественная к нубам:

- lazy IO (readFile . lines, interact-подобный хеллоувордизм)
- foldl без ', нестрогие sum/product

Пуризмы:

- "настоящие" частичные функции (head vs headMay)
- "функции-исключения" притворяющиеся частичными (error, undefined...)

Непереносимость:

- бэкпортирование фич новой base в старые GHC

Бойлерплейт:

- неэкспорт нужных штук типа (>=>)
- одни и те же имена (*.map == fmap, IsMap, sequenceA == sequenceM)

Недостаточно ортогональный и алгебраический дизайн:
- numeric tower
- algebraic tower
- отсутствие единообразности - например, есть maybe и either, но нет bool

На этом этапе мне надоело, продолжим завтра

30 сентября 2017, 23:44

Какую Prelude юзать

Дефолтовая понятно говно хотя бы из-за того, что String и Lazy IO пролазят во все дыры.

Пока остановился на Protolude. 51 обратная зависимость на Хакадже, т.е. вроде не abandonware.

base-prelude - это Снойман, есть сомнения.
classy-prelude - больше классов = больше неоднозначносте = больше сигнатур, тоже есть сомнения

Upd:

foundation - несовместимое переизобретение Text = невозможность использования либ
basic-prelude - второй кандидат, в-основном из-за фокуса на Text
rebase - идея тупого реэкспорта с целью экономии импортов. Отказать.
preliminaries -
prelude-extras -
algebraic-prelude -
helium-overture -
pregame -
intro -
definitive-base -
awesome-prelude -
universum -
preamble -
liblawless -
classy-prelude-conduit -
interlude-l -
papa -
safe-prelude -
protolude-lifted -
yap -
psi -
lifted-protolude -
subhask -

Это не смешно!

30 сентября 2017, 22:14

25 сентября 2017

rssh

В эту пятницу - Emerging Languages / UA

Если вы разрабатываете языка программирования - приходите.

https://prjctr.com.ua/events/emerging-languagesua.html



25 сентября 2017, 19:49

nponeccop

В Перле внезапно классный split with a limit

Типа split ' ', 'foo bar baz', 2 - это ('foo', 'bar baz').

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

В JavaScript же лимит работает не так, и из аналогичного вызова вернется 'foo', 'bar'.

Тьфу! В х-е кстати тоже.

25 сентября 2017, 17:30

24 сентября 2017

Anton Salikhmetov

Упражнения из Барендрегта, глава 3

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

3.5.1. Нарисовать графы G(M) для каких угодно термов каждый может и сам.

3.5.2. А вот найти термы по заданному бета-графу - это уже интересно:
(i) M1 -> ... -> Mn -> M1 для произвольного n:
M1 = N N~n, где N = x1,..., xn: xn ... x2 x1 x1;
(ii) чтобы добавить к (i) Mi -> Mi для всех i, возьмем M1 Ω;
(iii) чтобы добавить к (i) Mi -> I для всех i, возьмем (x: I) M1;
второй граф имеет терм I ω ω -> I Ω -> Ω, I Ω -> Ω, Ω -> Ω;
третий граф имеет терм K I Ω -> (x: I) Ω -> I, K I Ω -> Κ Ι Ω, (x: I) Ω -> (x: I) Ω;
(iv) чтобы сделать бесконечный цилиндр из (i), возьмем M1 ((x: x x x) (x: x x x)).

3.5.3. Построим терм M0, такой, что M0 ->>β M1 ->η M2 ->>β M3 ->η M4 ->>β ...:
M0 = x: (y: M) x x ->>β x: M x ->η M ->>β Μ0;
M найдем, как будто мы до сих пор никогда не слышали про Y:
M = (f, x: (y: f) x x) M, M = W W, W = w: (f, x: (y: f) x x) (w w).

3.5.4. Пусть M = (b, x, z: z ( b b x)) (b, x, z: z (b b x)) x. Чтобы получить кайф, построив G(M) и установив, что для каждого n этот граф имеет n-мерный куб в качестве подграфа, нужно сначала покурить каннабис на родине автора.

3.5.5 (Бем). Бем не обидится, если не все будут рисовать G(M).

3.5.6 (Виссер). (i) Это мое самое любимое упражнение. Покажем, что имеется единственный редекс R с одной вершиной в G(R).
Если R = (x: M) N, то M[x := N] = (x: M) N. Рассмотрим все случаи:
1) x не входит в M => M = R => R = (x: R) N - это не терм;
2) M = x => x[x := N] = R => N = R => R = (x: x) R - это не терм;
3) M = P Q;
4) M = y: M' => R = y: M'[x := N] - это не редекс.
Значит, R = (x: P Q) N =
= (P Q)[x := N] = P[x := N] Q[x := N] = (x: P Q) N => P[x := N] = x: P Q и Q[x := N] = N;
Рассмотрим все случаи для P:
1) x не входит в P => P = (x: P Q) - это не терм;
2) P = x => N = x: x Q;
3) P = y: P', но тогда в R было бы два редекса, а не один;
4) P = P1 P2 => P[x := N] = P1[x := N] P2[x := N] - это аппликация, а не абстракция.
Значит, R = (x: x Q) (x: x Q) -> (x: x Q) Q[x := x: x Q] => Q[x := N] = x: x Q.
Рассмотрим все случаи для Q:
1) x не входит в Q => Q = x: x Q - это не терм;
2) Q = x;
3) Q = Q1 Q2 => Q1[x := N] Q2[x := N] - это аппликация, а не абстракция;
4) Q = y: Q' => y: Q'[x := N] = x: x Q => Q'[x := N] = y Q, но тогда x не входит в Q.
Таким образом, R = (x: x x) (x: x x).
(ii) А вот это не самое любимое мое упражнение.

3.5.7-3.5.10. Бла-бла-бла про хитровытраханные графы и понятия редукции.
Может быть, они и полезные упражнения, но я иду дальше.

3.5.11. Будем писать M ^ N, если L ->> M и L ->> N для некоторого терма L. Докажем, что
(i) K I K ^ K I S: возьмем K (K I S) K;
(ii) (x: a x) b ^ (y: y b) a: возьмем (y: (x: y x) b) a;
(iii) (x: x c) c ^ (x: x x) c: возьмем (y: (x: x y) y) c;
(iv) (x: b x) c ^ (x: x) b c: возьмем (y, x: y x) b c;
(v) (x: b x (b x)) c ^ (x: x x) (b c): возьмем (z, y: (x: x x) (z y)) b c;
(vi) (x: b x) c ^ (x: x) (b c): возьмем I ((y, x: y x) b c);
(vii)* (Плоткин) ...ах, если бы я смог доказать, что не имеет места (x: b x (b c)) c ^ (x: x x) (b c), то я бы прочувствовал, что бета-редукция не обладает "перевернутым свойством CR".

3.5.12-3.5.15. Дальше в редукционные дебри углубляться не буду.

comment count unavailable comments

24 сентября 2017, 18:38

20 сентября 2017

nponeccop

Регулярки в х-е дизайнили дебилы

Короче, в регулярке "()foo|()bar" нельзя понять, вторая группа заматчилась или первая. В перле можно ('' vs undef), а в х-е нельзя, т.к. "" vs "".

https://stackoverflow.com/q/46308779/805266

Upd: таки один из 100500 оверлоадов это позволяет делать, но через жопу. Т.е. надо враппер писать

20 сентября 2017, 04:55

15 сентября 2017

09 сентября 2017

nponeccop

Жизнь без статики

А скажите, это нормально всегда билдить стат. и дин. версию либы, даже если одна из них не нужна? И каковы на это затраты времени (при сборке стеком)?

Upd: https://github.com/haskell/cabal/issues/1720 пофиксят - и заживём!

09 сентября 2017, 14:49

06 сентября 2017

nponeccop

Всё что вам надо знать о GHC

Цитата:

I noticed that when running even ghc --make -j2 on my project with 30 modules, sudo csysdig (a program to easily report syscall activity) reports betwen 1-2 *million* calls per second.

06 сентября 2017, 16:00

04 сентября 2017

swizard

а вот, например, ещё вакансии

Собственно, образовалась ещё вакансия. Нам нужно несколько человек, задач много, они все (как это водится) инновационные и интересные, минимум легаси, максимум r&d, ну и так далее.

Формальное описание таково:


От кандидата требуется:
  • Опыт работы с большими объёмами данных.
  • Знание основных паттернов проектирования систем обмена сообщениями.
  • Опыт сетевого программирования.
  • Навыки работы с linux.
Плюсами будут:
  • Знание теории, связанной с bigdata (статистика, машинное обучение, анализ данных, вероятностные алгоритмы, кластеризация, и т.п.)
  • Знание, или устойчивое желание и возможность освоить:
    • Язык программирования Rust
    • Язык программирования Erlang и платформу OTP
  • Владение функциональной парадигмой программирования.
  • Опыт работы с:
    • RabbitMQ
    • Postgres
    • Apache Cassandra
    • Redis

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

Если интересна вакансия, пишите мне на почту (с резюме в аттаче), если знаете кого-то, кому может быть она интересна — рассказывайте! Общие вопросы пишите лучше сюда в комменты, чтобы мне не копипастить по письмам ответы.

04 сентября 2017, 12:40

03 сентября 2017

nponeccop

Новости GHC на Windows

Стек внезапно требует на диске около 4 гигов. 1.7 гб занимает GHC, но пидарасы распаковывают его дважды - сначала .tar.xz -> .tar 1.7 гига, а потом тар растаривают.

В GHC всё никак не починят dll for windows. Но вроде как 4 дня назад написали скриптик который собирает из объектников столько длл, сколько нужно для того? чтобы уместиться в ограничение PE-формата 64к символов. И ещё делает так, чтобы для тех, кто с разделённой длл линкуется, разделение не было заметно. Пока последней версией с поддержкой DLL остается аж 7.6.3

03 сентября 2017, 11:39

01 сентября 2017

ruhaskell.org

Полнофункциональные гетерогенные списки

Использование гетерогенных списков. Фильтрация по классам типов. Вызов соответствующих функций. Реализация концепций instanceOf и asInstanceOf.

написал Денис Шевченко 01 сентября 2017, 00:00