Russian Lambda Planet

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

23 ноября 2017, 16:10

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

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

В. Брагилевский в Киеве 18.11.2017

Теперь официально. Виталий Брагилевский в Киеве 18 Ноября 2017 года Суббота Институт Математики НАН Украины. Бесплатно. Будет видео в записи. Please Share TWIMC.

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

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, который идет только с динамическими либами, без этого статик-говна для любителей говна. Понятно, что всё в результате похудело, и 32-битный GHC занимает 300 метров, а не 900.

Но поскольку пидарасы, пишущие ghc, так и не сделали у либ никакого ABI (их объяснения я знаю не надо в комментах пересказывать), при попытках пекеджить GHC-либы так же, как пекаджат сишные либы, наступают жопы самого разнообразного плана. Т.е. нельзя просто так взять и выпустить 6-мегабайтный cabal-install, который будет зависеть от libHSCabal.so, при апдейтах начнётся пизда и борода и хуй. Чтобы не началось, надо делать разные приседания. Школ приседания с версиями системных либ есть минимум две в Арче, ну и в каждом другом дистре линукса своя схема.

Ну и эти двое пидарасов не дружат с третьими пидарасами, которые делают стек. Поскольку уже для сборки Setup.hs нужен ключик -dynamic, а стек в это не умеет.

Вроде бы не умеет, поэтому зафайлил ишшуй в стек: https://github.com/commercialhaskell/stack/issues/3409

Если интересно посмотреть на арчевых пидарасов, можно почитать https://wiki.archlinux.org/index.php/Haskell Там из абзаца, начинающегося с "For these reasons, you have to make sure" написано, что не только stack нинужен™, но и cabal-install. Я хуею, дорогая редакция! Интересно кстати, что там на страничке наслоения старых школ приседаний. А у второй большой школы приседаний есть отдельная страничка https://wiki.archlinux.org/index.php/ArchHaskell У них даже свой несовместимый GHC был. Но уже нету поскольку i686 is deprecated.

Upd: стек-пидарасы сказали что вы должны терпеть боль и билдить статически no matter what. Хорошее замечание.

03 сентября 2017, 21:44

Новости 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

29 августа 2017

ru_declarative

Вакансия на Scala.

Тут внезапно освободилась вакансия Scala-разработчика, возможно переобучение с других языков. Разрабатывать придется облачный (хостится на AWS) энтерпрайзный PLM. Зарплаты рыночные и раз в год индексируются. Компания (слишком) быстрорастущая. Называется Adalisk. Оффис около метро Ясенево в Москве.
Есть желающие?

написал Mike Potanin (mpotanin@gmail.com) 29 августа 2017, 16:16

26 августа 2017

Anton Salikhmetov

I Have a Dream

I want to see optimal reduction without brackets and croissants.

Modify interaction rules, change data attached to abstraction, application, and fan nodes, even play with global state if needed. Just get it done without introducing any more agents except those three.

Is it possible? I don't know, let's find out!

comment count unavailable comments

26 августа 2017, 19:06

20 августа 2017

Anton Salikhmetov

Депрессия

У меня тут экзист... в общем, кризис среднего возраста. Были поводы. Пока было солнце, море и пиво две недели, думал, что пройдет. Не прошло. Вокруг какая-то сплошная хуита творится. Нашел какие-то online social support groups. Открыл, посмотрел и закрыл. Только хуже стало. Одни уроды и дебилы. Те же самые, что и в жизни. А где взять глобус с неуродами и недебилами, неизвестно. Уроды и дебилы - депрессия - еще больше уроды и дебилы - еще больше депрессия... Это замкнутый круг какой-то!

В прошлом году на день рождения получил пианино. За год немного научился играть. Хоть одна радость в жизни. А лямбды застопорились. Примерно знаю, чего хочу. Но этого мало, чтобы решение найти. В математике надо четко сформулировать, а потом обычно решение очевидно (особенно в этой теме). Оказывается, сформулировать не так-то просто. А компетентные люди все заняты грантами, конференциями, студентами, рецензиями и прочей хуитой. Внезапно оказалось, что они еще друг друга ненавидят всей душой. Неудивительно, что лямбды в жопе. Уже лет двадцать как, судя по публикациям.

Короче, надо просто всех убить, и все.

comment count unavailable comments

20 августа 2017, 06:50

16 августа 2017

nponeccop

Объясните грабли

bug.ts:
export const foo = (bar: number) => {
    console.log(arguments)
}
Компиляция без ключей, "tsc bug.ts", ожидаемо падает c сообщением о том, что arguments нету в случае arrow function.

А если собирать как "tsc -t es6 bug.ts" - то собирается без ошибок, а в рантайме понятно что жопа.

Так и должно быть? Да-нет и почему.

16 августа 2017, 19:28

David Sorokins WebLog

Трансляция модели из Python в Haskell

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

Пакет больше предназначен быть неким клеем, с помощью которого на языке Python можно соединять и объединять готовые компоненты в единую модель, причем сами компоненты предполагается создавать уже на языке Haskell. Однако, во многих случаях должно хватить существующего набора компонент, и поэтому часто можно ограничиться одним языком Python. В планах добавить поддержку GPSS-подобного DSL.

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

Итак, модель описывается на языке Python. По ней автоматически создается соответствующий код на языке Haskell. Более того, создается готовый проект на основе системы сборки Stack. Собственно, это главное техническое требование - на системе пользователя должен быть установлен Stack. Здесь предвижу некоторые возможные трудности с пакетом old-time на некоторых системах Windows, но надеюсь, что со временем они благополучно разрешатся.

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

Мне был довольно интересен такой эксперимент по использованию Haskell из Python. Может быть, кто-нибудь возьмет идею на вооружение

написал dsorokin (noreply@blogger.com) 16 августа 2017, 07:31

09 августа 2017

nponeccop

Внезапно работы по GHC+libuv

https://ghc.haskell.org/trac/ghc/ticket/8400

там правда не RTS, а товарищ свою NIH base пишет, с libuv и IOCP.

09 августа 2017, 22:36

04 августа 2017

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

Swift Model Generator from Erlang Types

-module(roster_swift).
-export([parse_transform/2]).
-compile(export_all).
-define(SRC, "apps/roster/priv/macbert/").

parse_transform(Forms, _Options) -> switch(directives(Forms)), Forms.
directives(Forms) -> lists:flatten([ form(F) || F <- Forms ]).

switch(List) ->
    file:write_file(?SRC++"Source/Decoder.swift",
    iolist_to_binary(lists:concat([
       "func parseObject(name: String, body:[Model], tuple: BertTuple) -> AnyObject?\n"
       "{\n    switch name {\n",
       [case_rec(X) || X <- List],
       "    default: return nil\n"
       "    }\n}"
    ]))).

act(List,union,Args,Field,I) -> act(List,union,Args,Field,I,simple);
act(List,Name,Args,Field,I) -> act(List,Name,Args,Field,I,keyword).

act(List,Name,Args,Field,I,Fun) ->
%    io:format("Keyword: ~p~n",[{Name,Args}]),
    lists:concat([tab(1),List,".",Field,
    " = body[",I,"].parse(bert: tuple.elements[",I+1,"]) as? ",
    ?MODULE:Fun(Name,Args,{Field,Args}),"\n"]).

case_rec({Atom,T}) ->
    List = atom_to_list(Atom),
    Lower = string:to_lower(List),
    Var = "a" ++ List,
    lists:concat([ "    case \"", List, "\":\n"
    "        if body.count != ", integer_to_list(length(T)), " { return nil }\n",
    io_lib:format("        let ~s = ~s()\n",[Var,List]),
    [ tab(2) ++ act(Var,Type,Args,Field,I-1) ||
         {{_,{_,_,{atom,_,Field},Value},{type,_,Type,Args}},I} <- lists:zip(T,lists:seq(1,length(T))) ],
    "        return " ++ Var ++ "\n" ]).

form({attribute,_,record,{List,T}})  ->
   [X|Rest]=atom_to_list(List),
   case X >= $A andalso X =< $Z andalso List /= 'Client'
                                orelse List == io
                                orelse List == error
                                orelse List == ok2
                                orelse List == error2
                                orelse List == ok of true
      -> spec(List,T),
         class(List,T),
         {List,T};
    _ -> [] end;
form(Form) ->  [].

class(List,T) ->
   file:write_file(?SRC++"/Model/"++atom_to_list(List)++".swift",
   iolist_to_binary(case lists:concat([ io_lib:format("\n    var ~s",
                [ infer(Name,Args,atom_to_list(Field))])
               || {_,{_,_,{atom,_,Field},Value},{type,_,Name,Args}} <- T ]) of
               [] -> [];
               Fields -> lists:concat(["\nclass ",List," {", Fields, "\n}"]) end)).

spec(List,T) ->
    file:write_file(?SRC++"/Spec/"++atom_to_list(List)++"_Spec.swift",
    iolist_to_binary("func get_"++atom_to_list(List) ++ "() -> Model {\n  return " ++ premodel(List,T) ++ "}\n")).

premodel(List,T) ->
    D = 1,
    Model = tab(D) ++ string:join([ model({type,X,Type,Args},D+1) || {_,_,{type,X,Type,Args}} <- T ],",\n"++tab(D)),
    erlang:put(List,Model),
    io_lib:format("Model(value:Tuple(name:\"~s\",body:[\n~s]))",[atom_to_list(List), Model]).

tab(N) -> lists:duplicate(4*N,$ ).

model({type,_,nil,Args},D)     -> "Model(value:List(constant:\"\"))";
model({type,_,binary,Args},D)  -> "Model(value:Binary())";
model({type,_,atom,Args},D)    -> "Model(value:Atom())";
model({type,_,list,[{type,_,atom,[]}]},D)    -> "Model(value:List(constant:nil, model:Model(value:Atom())))";
model({type,_,list,[{type,_,binary,[]}]},D)  -> "Model(value:List(constant:nil, model:Model(value:Binary())))";
model({type,_,list,[{type,_,integer,[]}]},D) -> "Model(value:List(constant:nil, model:Model(value:Number())))";
model({_,_,list,[{_,_,record,[{_,_,Name}]}]},D) -> lists:concat(["Model(value:List(constant:nil,model:get_",Name,"()))"]);
model({type,_,list,[Union]},D)    -> "Model(value:List(constant:nil, model:"++ model(Union,D) ++ "))";
model({type,_,record,[{atom,_,Name}]},D)        -> lists:concat(["get_",Name,"()"]);
model({type,_,list,Args},D)    -> "Model(value:List(constant:nil))";
model({type,_,boolean,Args},D) -> "Model(value:Boolean())";
model({atom,_,Name},D)         -> lists:concat(["Model(value:Atom(constant:\"",Name,"\"))"]);
model({type,_,term,Args},D)    -> "Model(value:nil)";
model({type,_,integer,Args},D) -> "Model(value:Number())";
model({type,_,tuple,any},D)    -> "Model(value:Tuple())";

model({type,_,union,Args},D)   -> io_lib:format("Model(value:Chain(types:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,tuple,Args},D)   -> io_lib:format("Model(value:Tuple(name:\"\",body:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,Name,Args},D)    -> io_lib:format("Model(~p): Args: ~p~n",[Name,Args]).

keyword(X,Y,_Context) -> keyword(X,Y).
keyword(record, [{atom,_,Name}]) -> lists:concat([Name]);
keyword(list, [{type,_,record,[{atom,_,Name}]}]) -> lists:concat(["[",Name,"]"]);
keyword(list, [{type,_,atom,[]}]) -> lists:concat(["[","String","]"]);
keyword(list, Args)   -> "[AnyObject]";
keyword(tuple,any)    -> "[AnyObject]";
keyword(term,Args)    -> "AnyObject";
keyword(integer,Args) -> "Int";
keyword(boolean,Args) -> "Bool";
keyword(atom,Args)    -> "StringAtom";
keyword(binary,Args)  -> "String";
keyword(union,Args)   -> "AnyObject";
keyword(nil,Args)     -> "AnyObject".

infer(union,Args,Field) -> Field ++ ": " ++ simple(union,Args,{Field,Args}) ++ "?";
infer(Name,Args,Field)  -> Field ++ ": " ++ keyword(Name,Args,{Field,Args}) ++ "?".

simple(A,[{type,_,nil,_},{type,_,Name,Args}],Context) -> keyword(Name,Args,Context);
simple(A,[{type,_,Name,Args},{type,_,nil,_}],Context) -> keyword(Name,Args,Context);
simple(_,_,_) -> "AnyObject".

04 августа 2017, 19:23

28 июля 2017

nponeccop

Implementing Algebraic Effects in C “Monads for Free in C”

Тут проскочила ссылка на пейпер. Не радуйтесь, там это лапша из setjmp/long jump, а не rust-style zero cost.

28 июля 2017, 16:22

10 июля 2017

nponeccop

Опять починили Hyper-V

Теперь правда не креши, а поддержку high dpi displays. Теперь гостевые low dpi displays на low dpi хостах снова отображаются корректно (но только после того как загрузится модуль hyperv_fb)

С крешами ситуация старая по веткам:

4.11.9 работает
4.9.36 падает
4.4.76 вешается
4.1.42 падает
3.18.60 работает
3.16.43 работает
3.14.2 работает

10 июля 2017, 23:18

25 июня 2017

Nikita Prokopov

Зачем вам нужна Clojure?

Слайды доклада на Codefest: https://speakerdeck.com/tonsky/clojure-at-codefest-2013 (там же и pdf)

Картинки для привлечения внимания:





Спасибо lionet и моей жене Юле за помощь в подготовке доклада.

25 июня 2017, 22:48

21 июня 2017

beroal

сумма как моноидальное произведение

Правильно ли я думаю, что любой функтор F является моноидальным между категориями, в которых моноидальная структура задана категорной суммой? Конкретно, (F, [F(ι0), F(ι1)]) есть моноидальный функтор? (ι… — инъекции суммы.)

21 июня 2017, 12:33

map, filter, catMaybes

∃a. ∃b. ∃m:a->Maybe b. ∀f:a->b. ∀p:a->Bool. ¬(catMaybes . map m == map f . filter p)

Другими словами, не всякий catMaybes можно выразить через map и filter. Ситуация такая же, как с инъекциями и сюръекциями. Для каждой инъекции s:A->B, кроме случая, когда A пустое и B населённое, существует сюръекция r такая, что r∘s=id. Это «кроме» портит всё удовольствие.

Значит, придётся отказаться от filter в пользу функции zyu

zyu m = catMaybes . map m
zyu (m1 <=< m0) == zyu m1 . zyu m0

где <=< — композиция в категории Клейсли над Maybe.

21 июня 2017, 12:33

the list type constructor and its analogs

Besides singly linked (inductive) lists, there are other entities similar to lists. They may be more or less convinient than lists depending on a problem.

Inductive lists first. The most concise interface for lists is the isomorphism list e ≅ list_step e (list e), where list_step e rc := 1 + e×rc. The right-to-left component of this isomorphism is list construction, left-to-right is destruction. The glaring property of such lists is asymmetry. A head of a list is accessible by 1 destruction, other elements require more. An inductive list is a stack, construction is “push”, destruction is “pop”, a head of a list is a top of a stack.

But we can provide 2 isomorphisms for every side of a list, where side is “left” or “right”. The S-side isomorphism tinkers with the S-most element of the list.

I will describe 2 kinds of symmetric lists: free monoids and arrays.

Viewing a list as a free monoid stresses the fact that a list may be folded/accumulated by a monoid. In detail, there are the category of sets, the category of monoids, and the adjunction F⊣U between them. F e is a monoid, the free monoid of e. It is the standard list monoid, i.e. its operations are concatenation and the empty list. Its carrier is the set of lists with elements from the set e. ε (the counit) of the adjunction is a folding function. ε m, where m is a monoid, folds a given list with m. List elements must come from the carrier of m, of course. η e (the unit of the adjunction) converts a value into a singleton list containing this value. (A singleton list is a list of length 1.)

Folding provides a limited way of reading. Some definitions first. I will use “assop” is another name for associative (2-ary) operation. For every side S, S-assop is the operation which returns its argument at S. Using a free functor from the category of assops to the category of monoids, we obtain the S-monoid, its created neutral element will be denoted as NONE and an assop element a as SOME a. For every list bs, folding map SOME bs by S-monoid gives SOME a, where a is the S-most element of the list, if it exists, and NONE otherwise. But we cannot read, for example, the element after the head in this way. This can be proved. Suppose that there is a function f and a monoid m, m = ⟨+', 0'⟩, such that fold m (map f bs) returns the element of bs after the head. Let g bs := fold m (map f bs). Then ∀a, ∀b, g [a, b] = SOME b and g [a, b] = f a +' g [b] = f a +' NONE. This means that SOME 0 = SOME 1, but SOME is injective like every data constructor.

Suppose that a function is constructing an abstract list, i.e. using an interface of lists. A monoid is not enough: we need to build finite lists somehow. So the interface must at least contain a method which construct a singleton list. Then we can get a finite list by concatenating singleton lists. This interface has 2 type parameters: a monoid carrier m (presumably the standard list monoid) and a type of list elements e. Using category theory, an implementation of this interface can be described concisely as an object in the category (comma category) of morphisms from the object e to the functor U. I call such an interface “a monoid with import”, where the function “import” is singleton list construction, so an element is may be imported into a monoid. Observe that this interface does not depend on a type constructor.

Instead of relying on types m and e, we can provide a type constructor list, a monoid structure on list e for every e, and a monad structure on list. Then import becames η of the monad list.

Random-access lists aka arrays. A simple formal description of an array is a function from list indices (locations) to list elements. Indices may be natural numbers starting from 0, but we do not need such details. A set of indices may be any finite total order. Concatenation of arrays requires a notion of a sum of total orders. Let L0 and L1 be total orders. Then the set carrier(L0)+carrier(L1) (“+” on sets is disjoint union) with lexicografic order is the total order L0+L1. Let a0:carrier(L0)→e and a1:carrier(L1)→e be arrays. carrier(L0+L1) = carrier(L0)+carrier(L1), carrier(L0+L1)→e = carrier(L0)+carrier(L1)→e ≅ (carrier(L0)→e) × (carrier(L1)→e) by properties of categorical sum. The right-to-left component of this isomorphism is concatenation, the left-to-right component is splitting.

21 июня 2017, 12:32

путь к теории категорий



есть очевидный путь к теории категорий: формальная логика, алгебраические структуры, порядки, теория категорий
вы ищете «царский» путь, читаете философию, научпопные сказки, лишь бы не изучать математику
зачем вы так?

настенькины комиксы, не надо так, рисовач.ру

21 июня 2017, 12:32