Russian Lambda Planet

26 марта 2017

nponeccop

Экстракшен

https://hal.archives-ouvertes.fr/file/index/docid/338973/filename/letouzey_extr_cie08.pdf

Долго длившийся односторонний "спор" с maxim по поводу правомерности использования термина "extraction" закрыт в его пользу.

Отец кок-экстрактора Pierre "какой-то студент" Letouzey употребляет этот термин вольно через предложение в статье по ссылке. Также на эту работу ссылаются пейперы по F* и так же вольно употребляют extraction.

В-общем, на то что extraction это превращение прувов в программы - можно забить. Все всё равно превращают только программы в программы, а CHI-экстракция остаётся не более чем любопытным курьёзом.

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

26 марта 2017, 03:05

25 марта 2017

nponeccop

Новости хакатона

Создал тучу тасок по окзору: https://github.com/ptol/oczor/issues/10

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

По HNC посрывали низковисящие фрукты, но осталось ещё немного.

25 марта 2017, 03:27

24 марта 2017

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

Cubical Type Theory in a Topos

Axioms:

ax1 : [∀(φ:I Ω).(∀(i:I).φi∨¬φi)⇒(∀(i:I).φi)∨(∀(i:I).¬φi)]
ax2 : [¬(0 = 1)]
ax3 : [∀(i:I).0⊓x=0=x⊓0 ∧ 1⊓x=x=x⊓1] 
ax4 : [∀(i:I).0⊔x=x=x⊔0 ∧ 1⊔x=1=x⊔1].
ax5 : [∀(i:I). cof(i=0) ∧ cof(i=1)]
ax6 : [∀(φψ:Ω). cofφ⇒cofψ⇒cof(φ∨ψ)]
ax7 : [∀(φψ:Ω). cofφ⇒(φ⇒cofψ)⇒cof(φ∧ψ)].


____________________________
[1] https://www.cl.cam.ac.uk/~rio22/pdf/Fields-talk.pdf
[2] http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf
[3] http://www.cl.cam.ac.uk/~rio22/agda/cubical-topos/root.html

24 марта 2017, 00:59

22 марта 2017

nponeccop

N2O.hs погнил

- в зависимости HJavascript почему-то перестали работать констрейнты на суперклассы. Т.е. class Show a => IsClass a, и в функции с IsClass a => a -> Foo требуетcя теперь констрейнт Show a.
- перестал работать фейковый инстанс Data для Connection из WebSocket (который абстрактный тип, не экспортирующий конструкоры). Задам ща вопрос на SO.

22 марта 2017, 19:10

21 марта 2017

nponeccop

Прогресс по хакатону-2

У нас уже 15 коммитов, в-основном однострочные рефакторинги, от 3 участников: xgromxx, yury-panchin и ingvar-lynn. И 6 служебных коммитов от меня.

Задания-однострочники описаны в двух тасках:

https://github.com/nponeccop/HNC/issues/97
https://github.com/nponeccop/HNC/issues/82

Помимо этого можно делать всё что хочется :)

21 марта 2017, 20:50

20 марта 2017

David Sorokins WebLog

GPSS на Haskell

Если кто еще не знает, GPSS - это один из самых известных специализированных языков дискретно-событийного моделирования. Так вот, я добавил в AivikaSim [http://www.aivikasoft.com/ru/products/aivikasim.html] поддержку GPSS-подобного предметного-ориентированного языка. Это пакет aivikasim-gpss [https://github.com/dsorokin/aivikasim-gpss]. Вот здесь находится работающий тестовый пример [https://github.com/dsorokin/aivikasim-gpss-test].

Постарался охватить основные моделирующие блоки, такие как SEIZE, PREEMPT, GATHER, ASSEMBLE, MATCH. Другие либо имеют явные аналоги у меня, либо требуют небольшого программирования как в случае блоков LINK и UNLINK. Не гарантируется точного совпадения результатов с GPSS World, так как логика работы с транзактами у меня совершенно иная, но в некоторых случаях результаты получаются очень близкими.

Вот, здесь примеры моделей [https://github.com/dsorokin/aivikasim-gpss/tree/master/examples] из красной книги Шрайбера по GPSS. Там в начале каждого примера приводится соответствующий код модели на языке GPSS World. Можно сличить результаты.

Example2A.hs означает, что это пример 2A из книги, а вот Example7-26.hs означает, что это соответствует модели на рисунке 7.26. Модели с окончанием Trans, такие как Example2BTrans.hs, означают, что там используется обобщенная версия AivikaSim. Фактически это означает, что приведенный код готов для использования в распределенной имитации.

Более того, пример Example7-26Distributed.hs непосредственно запускается через модуль распределенного моделирования. В данном случае это формально последовательная модель, но запускается она фактически в виде распределенной, т.е. она готова для кластера компьютеров. Используется оптимистичный алгоритм деформации времени.

Сразу напишу, что хотя для приведенных моделей удалось добиться очень хорошего соответствия с GPSS, то вот для примера 5D из книги Шрайбера такого близкого соответствия, скорее всего, не получится. Сейчас совпадение идет в 9 случаях против одного, где модель будет уже другой. Причем, совпадает даже на очень нетривиальных моделях, где важен порядок обработки транзактов.

Касательно скорости моделирования. Модуль GPSS-подобного языка последовательной версии AivikaSim моделирует примерно в 5-7 раз медленнее, чем GPSS World, но зато позволяет использовать разные методы в рамках одной модели, например, агенты и события. Для сравнения, распределенный модуль AivikaSim на последовательных задачах медленнее в раз 6-9, чем последовательная версия AivikaSim, но зато распределенную версию можно запустить много раз на разных узлах в рамках одной модели. Например, можно запустить 7 параллельно работающих локальных процессов на одной системе с 8-ядерным процессором.

Если кто захочет проверить результаты, то вот руководство по установке AivikaSim [https://github.com/dsorokin/aivikasim-installer].

написал dsorokin (noreply@blogger.com) 20 марта 2017, 20:56

19 марта 2017

Anton Salikhmetov

Лямбды на веревочках с рюшечками

Большие новости!

Я доделал needed reduction на веревочках, почистил лямбду от уродской waiting construct, сделал closed reduction дефолтным алгоритмом и обновил браузерную демку. Там теперь есть бесконечная прокрутка для дебага. Зацените рюшечки:

https://codedot.github.io/lambda/

Приятно иметь калькулятор в браузере, который одновременно печатает полную βη-нормальную форму для любого бестипового λK-терма и при этом считает 10 2 2 1 в цифрах Черча за долю секунды на моем Хромбуке.

Напомню, что 21024 примерно в (1017)4 раз больше, чем гиперобъем пространства-времени всей наблюдаемой вселенной с момента большого взрыва в планковских единицах измерения, в наши дни имеющий порядок (1060)4 планковских единиц.

Вот.

comment count unavailable comments

19 марта 2017, 17:43

nponeccop

Прогресс по хакатону

Создал тут рум для обучения падаванов работе с гитхабом:

https://gitter.im/nponeccop/github-fu

Секта святых Сквоша и Ребейза. Таинства Резьбы по вайтспейсу, Пересадки коммитов между ветками и Незалезания в чужой монастырь.

Уже есть два пулл-реквеста в HNC замёрженных однострочных. Но с конфы пока никого, чернила на флаера потрачены :)

19 марта 2017, 16:25

18 марта 2017

Scala@livejournal.com

Общее окончание

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

Для 2х строк получилось так:
def commonSuffix(s1: String, s2: String): String = {
  val n = (s1.reverseIterator zip s2.reverseIterator)
            .takeWhile {case (a, b) => a == b}
            .size
  s1.substring(s1.length - n) // is substring efficient ?
}
А как найти общее окончание для нескольких строк ?

написал Michael 18 марта 2017, 20:37

17 марта 2017

Yan Tayga

Уникальный курс по Хаскелю на русском

Хочу обратить внимание всех заинтересованных в изучении этого языка на сабж. Уже скоро.

Первая часть была просто замечательна; вторая как минимум не должна быть хуже.

17 марта 2017, 19:24

16 марта 2017

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

HoTT на 1 странице

~30 аксиом, больше чем у Гильберта!

   Id : (A : U) (a b : A) -> U
   refl : (A : U) (a : A) -> Id A a a
   inh : U -> U
   inc : (A : U) -> A -> inh A
   squash : (A : U) -> prop (inh A)
   inhrec : (A : U) (B : U) (p : prop B) (f : A -> B) (a : inh A) -> B
   contrSingl : (A : U) (a b : A) (p : Id A a b) -> Id (singl A a) (a, refl A a) (b, p)
   equivEq : (A B : U) (f : A -> B) (s : (y : B) -> fiber A B f y)
             (t : (y : B) -> (v : fiber A B f y) ->
             Id (fiber A B f y) (s y) v) -> Id U A B
   transport : (A B : U) -> Id U A B -> A -> B
   transpInv : (A B : U) -> Id U A B -> B -> A
   transportRef : (A : U) (a : A) -> Id A a (transport A A (refl U A) a)
   equivEqRef : (A : U) -> (s : (y : A) -> pathTo A y) ->
                (t : (y : A) -> (v : pathTo A y) ->
                Id (pathTo A y) (s y) v) ->
                Id (Id U A A) (refl U A) (equivEq A A (id A) s t)
   transpEquivEq : (A B : U) -> (f : A -> B) (s : (y : B) -> fiber A B f y) ->
                   (t : (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v) ->
                   (a : A) -> Id B (f a) (transport A B (equivEq A B f s t) a)
   appOnPathD :  (A : U) (F : A -> U) (f g : (x : A) -> F x) -> Id ((x : A) -> F x) f g ->
                 (a0 a1 : A) (p : Id A a0 a1) -> IdS A F a0 a1 p  (f a0) (g a1)
   mapOnPath : (A B : U) (f : A -> B) (a b : A) (p : Id A a b) -> Id B (f a) (f b)
   appOnPath : (A B : U) (f g : A -> B) (a b : A) (q : Id (A -> B) f g) (p : Id A a b) -> Id B (f a) (g b)
   IdP : (A B : U) -> Id U A B -> A -> B -> U
   mapOnPathD : (A:U) (F: A -> U) (f: (x:A) -> F x) (a0 a1: A) (p: Id A a0 a1) -> IdS A F a0 a1 p  (f a0) (f a1)
   mapOnPathS : (A:U) (F: A -> U) (C: U) (f: (x:A) -> F x -> C)
                (a0 a1 : A) (p : Id A a0 a1) (b0 : F a0) (b1 : F a1)
                (q : IdS A F a0 a1 p b0 b1) -> Id C (f a0 b0) (f a1 b1)
   funHExt : (A : U) (B : A -> U) (f g : (a : A) -> B a) ->
             ((x y : A) -> (p : Id A x y) -> IdS A B x y p (f x) (g y)) ->
             Id ((y : A) -> B y) f g
   S1 : U
   base : S1
   loop : Id S1 base base
   S1rec : (F : S1 -> U) (b : F base) (l : IdS S1 F base base loop b b) (x : S1) -> F x
   I : U
   I0 : I
   I1 : I
   line : Id I I0 I1
   intrec : (F : I -> U) (s : F I0) (e : F I1) (l : IdS I F I0 I1 line s e) (x : I) -> F x

   prop : U -> U
   prop A = (a b : A) -> Id A a b
   Sigma : (A : U) (B : A -> U) -> U
   Sigma A B = (x : A) * B x
   fiber : (A B : U) (f : A -> B) (y : B) -> U
   fiber A B f y = Sigma A (\x -> Id B (f x) y)
   id : (A : U) -> A -> A
   id A a = a
   singl : (A : U) -> A -> U
   singl A a = Sigma A (Id A a)
   pathTo : (A:U) -> A -> U
   pathTo A = fiber A A (id A)
   sId : (A : U) (a : A) -> pathTo A a
   sId A a = (a, refl A a)
   IdS : (A : U) (F : A -> U) (a0 a1 : A) (p : Id A a0 a1) -> F a0 -> F a1 -> U
   IdS A F a0 a1 p = IdP (F a0) (F a1) (mapOnPath A U F a0 a1 p)

16 марта 2017, 22:56

Infinity Language

Require    Import Strings.String.

Inductive  Loc: Type := intro: string -> nat -> nat -> Loc.
Definition Ident     := string.
Definition Label     := string.
Definition Binder    := prod Ident Loc.
Definition Branch    := prod Label (prod (list Binder) Type).
Definition NamedRec  := list (prod Binder Type).
Definition NamedSum  := list (prod Binder NamedRec).
Definition Decls     := Type.

Inductive PiCalculus :=
 | Send              | Recv
 | Spawn             | Kill
 | Sequential        | Parallel
 | Stop              | Start
 | Pub               | Sub.

Inductive EffectCalculus :=
 | EGet              | ESet
 | ESend             | ERecv
 | Write             | Read
 | Index             | Search
 | Rand              | Raise
 | Try               | Catch.

Inductive StreamCalculus :=
 | Map               | Fold
 | Scan              | Iota
 | SLoop             | Transpose
 | Rotate            | SSplit
 | Concat            | Zip
 | Reduce            | StreamMap
 | StreamMapPer      | StreamRed
 | StreamSeq         | Partition
 | Reshape           | Shape
 | Rearrange         | Copy
 | For               | While.

Inductive HomotopyCalculus :=
 | Id                | Refl
 | Inh               | Inc
 | Squash            | InhRec
 | TransU            | TransInvU
 | TransURef         | CSingl
 | MapOnPath         | AppOnPath
 | HExt              | EquivEq
 | EquivEqRef        | TransUEquivEq
 | IdP               | MapOnPathD
 | AppOnPathD        | Circle
 | Base              | HLoop
 | CircleRec         | I
 | I0                | I1
 | Line              | IntRec
 | Undef: Loc -> HomotopyCalculus.

Inductive MLTT :=
 | App:    MLTT   -> MLTT -> MLTT
 | Pi:     MLTT   -> MLTT -> MLTT
 | Lam:    Binder -> MLTT -> MLTT
 | Sigma:  MLTT   -> MLTT -> MLTT
 | Pair:   MLTT   -> MLTT -> MLTT
 | Fst:    MLTT   -> MLTT
 | Snd:    MLTT   -> MLTT
 | Where:  MLTT   -> Decls -> MLTT
 | Var:    Ident  -> MLTT
 | U:      MLTT
 | Con:    Label  -> list MLTT   -> MLTT
 | Split:  Loc    -> list Branch -> MLTT
 | Sum:    Binder -> NamedSum    -> MLTT
 | HIT:    HomotopyCalculus -> MLTT
 | PI:     PiCalculus       -> MLTT
 | EFF:    EffectCalculus   -> MLTT
 | STREAM: StreamCalculus   -> MLTT.


Скоро будет обновление Групоид Инфинити, я покажу как я вижу сопряжения Coq или Lean и линковку с рантаймами, которые делают пи калкулус (виртуальной машины с каналами) или стрим процессинг (типа футарка, управление GPU или векторизацией). Все это в фашистком стиле с единой вертикалью власти, которая лендится на MLTT коре, но в отличие от ОМ с сигмой и другими излишествами. Если вам интересно вы всегда можете высказаться на канале Infinity Language: http://gitter.im/groupoid/exe

EXE соответственно будет историческим названием конфигурации MLTT + EFF + PI. Без стримов и гомотопической теории. В Групоиде также найдется место для нетипизированных интерпретаторов в виде языка О. Вова по-прежнему топит за лендинг на Erlang, т.е. Coq-Erlang. Экстракт в Erlang и Rust — этими двумя направлениями занимаются японцы. Базовая библиотека передет в System F секцию (так как для рантайма зависимые типы нужны не особо), которая создана для оптимизирующих компиляторов типа Oczor и HNC. Для Oczor я слышал по-секрету скоро появится LLVM бекенд.

Вообще я вижу Групоид Инфинити как журнал, которых захватывает все продакшин применения всех систем типов и их приложений. Так что я думаю пиздить или приглашать публиковаться на тему: как я создал язык X для продакшина или любые достижения и самые модные (но обязательно минималистичные) подходы в каждом из пяти калкулусов. C HoTT как я понял, пока все основные конструкторы бюлтинами не сделаешь, никакого минимализма не получится, зато так даже лучше видно из чего состоит язык геометрии. HoTT и кубическую теорию будем считать продакшином для математиков.

Скину пока только скриншотик:

16 марта 2017, 16:22

15 марта 2017

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

Идея для дисера, дарю!

Рабочее название: Непрерывные отображения лямбда термов

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

Пример. Точка — Юнит. Две точки — Булевый тип. Две точки и одна перменная — например обработчик ошибок OK | Err reason. Две точки и две переменных — протокол с кодом возврата OK value | Err reason. Или другое ветвление. Две точки, одна переменная и рекурсивное зацикливание или петля — List A = Nil | Cons A (List A). И так далее. Если вы запустите генератор такой группы (какая у нее симметрия?) то вы получите все возможные базовые библиотеки функциональных языков программирования. Напоминаю, согласно МакБрайду орнамента всего три: точка, переменная и рекурсивное зацикливание. Ну и переменных может быть любое количество, кодировать нумералами черча, как и вселенные.

В гомотопической теории еще конструктор Пути, или просто говоря равенство, четвертый орнамент. Там альтернативное ветвление такое. Путь — Отрезок. Точка и Путь — S1. Но конструктор пути многомерный! Поэтому. Сфера — это Точка и двумерный путь (движение одномерного пути). Дальше высшие сферы, конусы, надстройки и так далее. Возможно добавление трех предыдущих орнаментов, что означает добавление носителя, т.е. для первых поллов генератора — типы натуральных Nat = 0 | S Nat, целых Z = 0 | S | P, действительных R = Stream Digit чисел. Да, да, для действительных чисел нужна корекурсия и коиндуктивные типы, простейший из которых стрим. Стрим от листового конса отличается тем что у него элиминатор и интродакшин поменяны местами.

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

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

15 марта 2017, 05:45

14 марта 2017

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

Домашка по топологии №3

Онлайн база данных топологических пространтсв: https://github.com/jamesdabbs/pi-base-data

14 марта 2017, 06:19

Natural Deduction in MLTT

Inductive ND_proves : list (prop atom) -> prop atom -> Prop :=
| ND_exfalso_quodlibet {Γ P} : Γ ⊢ ⊥ -> Γ ⊢ P
| ND_True_intro {Γ} : Γ ⊢ ⊤
| ND_or_introl {Γ P Q} : Γ ⊢ P -> Γ ⊢ P ∨ Q
| ND_or_intror {Γ P Q} : Γ ⊢ Q -> Γ ⊢ P ∨ Q
| ND_proof_by_cases {Γ P Q R} : Γ ⊢ P ∨ Q -> P :: Γ ⊢ R -> Q :: Γ ⊢ R -> Γ ⊢ R
| ND_and_intro {Γ P Q} : Γ ⊢ P -> Γ ⊢ Q -> Γ ⊢ P ∧ Q
| ND_and_elim {Γ P Q R} : Γ ⊢ P ∧ Q -> P :: Q :: Γ ⊢ R -> Γ ⊢ R
| ND_cond_proof {Γ P Q} : P :: Γ ⊢ Q -> Γ ⊢ P ⊃ Q
| ND_modus_ponens {Γ P Q} : Γ ⊢ P ⊃ Q -> Γ ⊢ P -> Γ ⊢ Q
| ND_assumption {Γ P} : In P Γ -> Γ ⊢ P
| ND_cut {Γ P Q} : Γ ⊢ P -> P :: Γ ⊢ Q -> Γ ⊢ Q
where "Γ ⊢ P" := (ND_proves Γ P).

14 марта 2017, 06:11

13 марта 2017

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

8,601,448 B2

Эрик запатентовал референсные типы для пойнтеров и хипа. Хаха



Надо лямбду запатентировать ребята!

13 марта 2017, 18:39

12 марта 2017

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

Retrofitting Linear Types

Когда я сказал недавно известному киевскому хаскелисту, который докладывал на kievfprog, что системам типов Раста сложнее чем у Хаскеля, он гыгыгнул так призрительно, что наверно подумал про HKT (которое на самом деле реаилизуется даже в версии 1.0). Линейные типы — это другое лицо пи калкулуса.

6.6 Ownership typing a` la Rust

Rust [31] features ownership (aka uniqueness) types. But like the original formulation of linear logic, in Rust A stands for linear values, unrestricted values at type A are denoted !A, and duplication is explicit. Rust quite beautifully addresses the problem of being mindful about memory, resources, and latency. But this comes at a heavy price: Rust, as a programming language, is speci cally optimised for writing programs that are structured using the RAII pa ern8 (where resource lifetimes are tied directly or indirectly to stack allocated objects that are freed when the control ow exits the current lexical scope). Ordinary functional programs seldom t this particular resource acquisition pa ern so end up being second class citizens. For instance, tail-call optimization, crucial to the operational behaviour of many functional programs, is not usually sound. is is because resource liberation must be triggered when the tail call returns. Hask-LL aims to hit a di erent point in the design space where regular non-linear expressions are the norm yet gracefully scaling up to latency-sensitive and resource starved programs is still possible.



Очень рад таким пейперам, мечтаю о полной и точной модели скедулера операционной системы, где ядра процессоров являются коиндуктивными процессами, а все программы — индуктивными протоколами. Может у хаскелистов получится нормальный API сделать для простых трех комбинаторов пи-калкулуса. Вот только как в Coq сделать так чтобы по spawn создавался и запускался отдельный CoFixpoint это все очень не просто. Хелоуворлдических статей на эту тему нет. В Агде кстати IO тоже сделано на коиндуктивных типах. Также как у меня в Co. Больше нигде коиндукции в IO нет. Катинг едж.
____________
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/2017/03/haskell-linear-submitted.pdf

12 марта 2017, 12:41

HKT in Rust

Компилирующийся код! А в этом журнале — это редкость, полноценные монадки на расте:


pub trait HKT<u> {
    type C; // Current type
    type T; // Type with C swapped with U
}

macro_rules! derive_hkt {
    ($t:ident) => {
        impl HKT<u> for $t<t> {
            type C = T;
            type T = $t<u>;
        }
    }
}

pub trait Functor<U>: HKT<U> {
    fn map<F>(&self, f: F) -> Self::T where F: Fn(&Self::C) -> U;
}

pub trait Applicative<U>: Functor<U> {
    fn pure_(value: U) -> Self::T where Self: HKT<U, C=U>;
    fn seq<F>(&self, <Self as HKT<F>>::T) -> 
       <Self as HKT<U>>::T where Self: HKT<F>, 
          F: Fn(&<Self as HKT<F>>::C) -> U;
}

pub trait Monad<U>: Applicative<U> {
    fn bind<F>(&self, F) -> Self::T where F : FnMut(&Self::C) -> Self::T;

    fn return_(x: U) -> Self::T where Self: HKT<U, C=U> {
        Self::pure_(x)
    }

    fn join<T>(&self) -> T where Self: HKT<U, T=T, C=T>, T: Clone {
        self.bind(|x| x.clone())
    }
}

impl<T, U> Functor<U> for Vec<T> {
    fn map<F>(&self, f: F) -> Vec<U> where F: Fn(&T) -> U {
        let mut result = Vec::with_capacity(self.len());
        for value in self {
            result.push( f(value) );
        }
        result
    }
}

impl<T, U> Applicative<U> for Vec<T> {
    fn pure_(value: U) -> <Self as HKT<U>>::T { vec![value] }

    fn seq<F>(&self, fs: <Self as HKT<F>>::T) -> 
      <Self as HKT<U>>::T where F: Fn(&<Self as HKT<F>>::C) -> U {
        let mut result = vec![];
        for (i, f) in fs.into_iter().enumerate() {
            let v = (f)( &self[i] );
            result.push(v)
        }
        return result;
    }
}

impl<T, U> Monad<U> for Vec<T> {
    fn bind<F>(&self, mut f: F) -> Vec<U> where F : FnMut(&T) -> Vec<U> {
        let mut result = vec![];
        for x in self {
            let v = f(x);
            result.extend(v);
        }
        result
    }
}

derive_hkt!(Vec);

fn test() {
        let v = Vec::return_(1);
        let v = v.bind(|x| vec![x.to_string(); 3]);
        println!("{:?}", v);

        let v = vec![vec!(true), vec!(false)];
        let v = v.join();
        println!("{:?}", v);
}

12 марта 2017, 12:33

Новости языков с кванторами

Габриель запили Dhall — Annah с рекордами или DSL #2 поверх Morte.

let zombieNames = [ "Rachel", "Gary", "Liz" ] : List Text in
let isAZombie = \(name : Text) -> { name = name, occupation = "Zombie" } in
let tag = map Text { name : Text, occupation : Text } in
let zombies = tag isAZombie zombieNames in
let policeNames = [ "Leon", "Claire" ] : List Text in
let worksForPolice = \(name : Text) -> { name = name, occupation = "Police officer" } in
let policeOfficers = tag worksForPolice policeNames in
let characters = concat { name : Text, occupation : Text }
                      ( [ zombies , policeOfficers ] : List (List { name : Text, occupation : Text }) ) in

{   protagonist = List/head { name : Text, occupation : Text } policeOfficers,
    numberOfCharacters = List/length { name : Text, occupation : Text } characters }


Что класно, что Rust так быстро развивается, что ядро Om/Exe уже не надо самому писать на расте, уже все заимплеменчено — грабь и воруй! — докидывай вселенных.

https://github.com/nanotech/dhall-rs.git

$ ./dhall < test
{ numberOfCharacters : Natural, protagonist : Optional { name : Text, occupation : Text } }

{ numberOfCharacters = List/length { name : Text, occupation : Text } (List/build { name : Text, occupation : Text } (λ(list : Type) → λ(cons : { name : Text, occupation : Text } → list → list) → λ(nil : list) → List/fold { name : Text, occupation : Text } (List/fold { name : Text, occupation : Text } nil list cons (List/build { name : Text, occupation : Text } (λ(list : Type) → λ(cons : { name : Text, occupation : Text } → list → list) → List/fold Text (["Leon", "Claire"] : List Text) list (λ(x : Text) → cons { name = x, occupation = "Police officer" })))) list cons (List/build { name : Text, occupation : Text } (λ(list : Type) → λ(cons : { name : Text, occupation : Text } → list → list) → List/fold Text (["Rachel", "Gary", "Liz"] : List Text) list (λ(x : Text) → cons { name = x, occupation = "Zombie" }))))), protagonist = List/head { name : Text, occupation : Text } (List/build { name : Text, occupation : Text } (λ(list : Type) → λ(cons : { name : Text, occupation : Text } → list → list) → List/fold Text (["Leon", "Claire"] : List Text) list (λ(x : Text) → cons { name = x, occupation = "Police officer" }))) }


Так что кто хочет пописать язык с зависимыми типами, в котором можно написать экстенсиональное равенство и при этом парадокс жирара/хуркенса/рассела не чекнется, и сделать это на Rust, милости просим на вневременной хакатон http://gitter.im/groupoid/exe
Фактически уже есть три имплементации на Haskell, Rust, Erlang. Скоро Om/Morte станет стандартом распространения лямбда термов в интернете.

12 марта 2017, 09:04

Scala@livejournal.com

ru_scala @ 2017-03-11T22:03:00

Предположим у нас есть несколько функций, которые вызываются при наступлении некоторого события. Так например при добавлении нового поста в ЖЖ нужно послать почту всем подписчикам, а также опубликовать ссылку на пост в социальных сетях, твитере и так далее.
case class NewPost(...)
type NewPostSubscriber = NewPost => Either[Exception, Unit]
Допустим, что все эти функции не зависят друг от друга и либо не возвращают ничего в случае удачного завершения, либо возвращают ошибку. Предположим также, что все возвращаемые ошибки нужно аккумулировать.

Теперь можно воспользоваться тем, что функции типа NewPostSubscriber можно превратить в функции NewPost => ValidatedNel[Exception, Unit], которые образуют моноид. Тогда вызов тех функций будет выглядеть так:
// invoke all subscribers with a NewPost event

def fireNewPost(event: NewPost, subscribers: List[NewPostSubscriber]) = {
  val invokeAll = subscribers foldMap { s => s map (_.toValidatedNel) } map (_.toEither)
  invokeAll(event)
}
Как вам такое решение ?

написал Michael 12 марта 2017, 08:56

11 марта 2017

nponeccop

Хрюшка на схемах

http://stackoverflow.com/q/42726378/805266

Cпросил тут, как на схемах эту хрюшку переписать:

fib a b = a : fib b (a + b)

Как бы анаморфизм, который складирует в свой сид старые значения

fib' :: (Integer, Integer) -> [Integer]
fib' = ana $ \(x, y) -> Cons x (y, x+y)

Но хочется честно хранить все генерически, а не только два.

11 марта 2017, 07:20

Фибоначчи на хистоморфном анаморфизме

На вопросы телезрителей http://stackoverflow.com/a/42731252/805266 за неимением Александра Друзя отвечают сами телезрители:
type L f a = f (Cofree f a)

histAna :: (Functor f, Corecursive t) =>
     (f (Cofree f a) -> Base t (f a)) -> f (Cofree f a) -> t
histAna psi = ana $ \oldHist -> fmap (:< oldHist) <$> psi oldHist

fibsListAna :: Num a => L Maybe a -> [a]
fibsListAna = histAna $ \case
    Just (x :< Just (y :< _)) -> Cons (x + y) (Just (x + y))

r1 :: [Integer]
r1 = take 10 $ fibsListAna $ Just (0 :< Just (1 :< Nothing))
Есть ещё версия для младшего школьного возраста:
histAna' :: Corecursive t => ([a] -> Base t a) -> [a] -> t
histAna' psi = ana $ \oldHist ->  (: oldHist) <$> psi oldHist
Непонятно, отличается ли она от взрослой.

11 марта 2017, 06:41

10 марта 2017

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

Fib as CoFixpoint

Require Import Streams.
CoFixpoint fib (a b: nat) : Stream nat := Cons a (fib b (a + b)).

10 марта 2017, 10:48

nponeccop

Стек починили

Закрыли оба бага (пока только в HEAD):

- утечку пространства tmpfs при билде проекта с большим количеством зависимостей https://github.com/commercialhaskell/stack/issues/3018
- баг солвера в проектах с setup-depends https://github.com/commercialhaskell/stack/issues/3044

10 марта 2017, 05:11

09 марта 2017

nponeccop

Фикспоинт на ЖСе

сonst fix = f => x => f(x1 => fix(f)(x1))(x)
sumInt = n => { 
    const sum = f => x => acc => x == 0 ? acc : f(x-1)(x+acc)
    return fix(sum)(n)(0)
}

09 марта 2017, 17:50

08 марта 2017

nponeccop

Уголок оверинжиниринга

У меня есть хохма-модуль Utils.Kmett, который стал ещё круче, чем был.

https://github.com/nponeccop/HNC/commit/c5a9ef249e86d2044be7995f1cbf525abe58c00f

Модуль реализует 2 строчки-хелпера, которые однако "имеют обобщённый тип и заслуживают выноса в либу".

Для этих 2 строчек:

- подключается 3 либы lens, bifunctors и аdjunctions, больше нигде в проекте не используемых
- подключается 5 синтаксических расширений, включая TemplateHaskell
- импортируются 8 символов из 7 модулей 4 либ (один символ используется только в невидимом TH-коде)

08 марта 2017, 03:07

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

От создателей Лямбда-Отеля и Групоид Инфинити

Для конференция #kievfprog 2017.1, которая пройдет в НАН Украины

http://conference.imath.kiev.ua/index.php/kievfprog/kievfprog-2017_1/index

Секретные флаера для участников конференции



https://github.com/groupoid/groupoid.space/blob/master/tex/flyer.pdf

08 марта 2017, 02:02

07 марта 2017

Scala@livejournal.com

Задачка из Твитера

Я прочитал про решение на Скале одной известной задачки.
Оно мне показалось слишком сложным. А как бы вы решали эту задачку ?

написал Michael 07 марта 2017, 16:44

Моноид для ключей командной строки

Наткнулся на моноид для ключей командной строки. Кто-нибудь имплементировал такое решение на Скале ?

написал Michael 07 марта 2017, 12:20

Anton Salikhmetov

How to Fix a Bug with Git

I am currently working on implementing needed reduction for interaction nets. To do that, I first needed to refactor a lot of somewhat ugly fast-written code in inet-lib. At some point, I changed retrieving an element from an array to .pop() from .shift(), just because in JavaScript the former happens to be a cheaper operation than the latter.

Many commits later, I decided to play with the program a little bit and compare performance between .shift()ing and .pop()ing. Boom! The program appeared to be broken. Even worse, invariance of the queue that is represented by that array with respect to the order in which it is processed is the whole point of interaction nets, namely the property of strong confluence also known as the one-step diamond property. I thought I fucked up hard.

First, I took a look at git-blame(1) for the line of code that calls .pop(), and found the corresponding commit. Then, I marked its parent commit as good with git-bisect(1). After a few steps, git-bisect(1) found the first bad commit.

Evidently, the problem had something to do with indirection applied by non-deterministic extension of interaction nets. And it did not take more than a couple of minutes to figure out a simple one-liner fix.

Overall, it took less than half an hour from finding a bug to fixing it which I first thought would take hours if not days. To me, it looks like yet another evidence that the idea of git-bisect(1) is totally genius. So, thanks again, Linus!

P. S. Free advice: when making commits, it is always useful to keep in mind 1) a possible need to git-grep(1) some lines of code later, and 2) almost inevitable need to deal with bugs which is a lot easier when commits are suitable for git-bisect(1).

comment count unavailable comments

07 марта 2017, 01:16

06 марта 2017

nponeccop

Листовки для #kievfprog 2017.1

https://docs.google.com/document/d/1L_yRb1_ajj9eswByMnRGHQlJ28T1B81dasUCyyMJThE/pub

По причине моего отсутствия пришла идея сделать листик и пораздавать. Это драфт, надо будет уложиться в не более чем один листик с 2 сторон.

Приглашение заняться некоммерческим групповым сексом с хаскелем, дабы избежать успеха. Разумеется, с упоминанием HNC, Exe и типизированного брейнфака!

06 марта 2017, 19:41

Scala@livejournal.com

Функциональное Решение

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

--

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

Решение заключается в проходе по массиву слева направо и справа налево с помощью двух индексов right и left: right указывает на правый текущий элемент, а left на левый. На каждой итерации проверяется сумма текущего левого и правого элементов. Если она равна target'у, то искомая пара найдена, если меньше, то right сдвигается влево, а если больше, то left сдвигается вправо.
def pair(a: Array[Int], target: Int): Option[(Int, Int)] = {

    var left = 0
    var right = a.length - 1
    var result: Option[(Int, Int)] = None
    while (left < right && result.isEmpty) {
      (a(left), a(right)) match {
        case (x, y) if x + y == target => result = Some(x, y)
        case (x, y) if x + y < target => left = left + 1
        case (x, y) if x + y > target => right = right - 1
      }
    }
    result
  }
А что если нам нужно найти не одну а все пары элементов массива, сумма которых равна target'у ?
Тогда придётся переписать наше решение:
def pairs(a: Array[Int], target: Int): List[(Int, Int)] = {

    var left = 0
    var right = a.length - 1
    var result: List[(Int, Int)] = List()
    while (left < right) {
      (a(left), a(right)) match {
        case (x, y) if x + y == target => result = result :+ (x, y); left = left + 1
        case (x, y) if x + y < target => left = left + 1
        case (x, y) if x + y > target => right = right - 1
      }
    }
    result
  }
А можно обойтись без copy-paste ?

Оказывается можно, если написать "функциональное" решение !
Сначала мы сформируем ленивый список (stream) всех "кандидатов":
def streamOfPairs(a: Array[Int], target: Int): Stream[(Int, Int)] =
    Stream.iterate(a) { xs => if (xs.head + xs.last > target) xs.init else xs.tail }
      .take(a.length - 1)
      .map { xs => (xs.head, xs.last) }
А теперь из полученного "стрима" легко получим как одну, так и все искомые пары:
 def pair(a: Array[Int], target: Int): Option[(Int, Int)] =
    streamOfPairs(a, target) find { case (x, y) => x + y == target }

  def pairs(a: Array[Int], target: Int): List[(Int, Int)] =
    (streamOfPairs(a, target) filter { case (x, y) => x + y == target }).toList
Как видим, "функциональный подход" помог нам избавиться от copy-paste и упростить решение.

написал Michael 06 марта 2017, 16:36

05 марта 2017

nponeccop

Стек хелл

Внезапно Снойман ответил, что стек мне собирает снапшот для 8.0.2 с GHC 8.0.1 и фейлится пытаясь собрать пекедж встроенный в GHC. Сейчас я написал довольно безумный скриптик, чтобы убеждаться что стек что-то собирает именно в тех версиях, которые имелись ввиду:
$ ls && ls lts-8.3 && (ls lts-8.3/8.0.2/lib/i386-linux-ghc-8.0.2/ -1 | wc -l)
lts-8.3
8.0.2
284
Пока собрано 140 зависимостей стека из 175, 284 это от сборки oczor ещё лишнее. Я даже тайм мерить пробовал, если не ошибся - посмотрим, сколько времени откидывание на кресло займет. Даёшь distghc/incredibuild! А лучше cloud stack, в котором зависимости собираются в докере на каком-нибудь ironworker и копеечка идёт Снойману на поддержку штанов.

Ахаха, зафейлился как раз на 140 из-за https://github.com/commercialhaskell/stack/issues/3018, отъел всю tmpfs и умер.

05 марта 2017, 15:11

Стек готов к продакшену

Снойман 21 декабря запилил поддержку setup-depends (это всякие препроцессоры типа happy, gtk2hstools или в моем случае uuagc-cabal). Но в мастер это замержилось только 4 декабря, что позже последней стабильной версии стека.

Сейчас пробую собрать HEAD-версию стека на двух платформах. И я решил немного сплясать и собрать с последним lts-8.3. И оно даже собирается (пока).

Внезапно под виндой собралось, а под линуксом жопа. Пробую ща ещё раз "откинуться на спинку кресла", и запустить билд тупо в бутстреп-режиме кабал-инсталлом.

05 марта 2017, 00:12

04 марта 2017

rssh

Разные миры

Сегодня на занятии, слушатели обратили внимание, что в UML диаграммах просто нет способа отобразить нетривиальное наследование в scala (типа cake паттерна). Я несколько лет об этом не задумывался -- просто никому не было нужно.

04 марта 2017, 16:56

nponeccop

Связные списки и хистоморфизм для Nat

data ListF a b = Cons a b | Nil
data CListF a b = CCons a (Maybe b)

Я когда-то давно писал, что в С++ связные списки - это не Fix (ListF a), а Fix (CListF a). Если хочется пустые списки - приходится городить дополнительный слой Maybe (Fix (CListF a))

И вот сегодня я узнал, что

data Cofree f a = a :< f (Cofree f a)

То есть, что сишные списки - это просто Cofree Maybe a.

А хистоморфизм для Nat = Fix Maybe имеет вид

natHisto :: (Maybe (Cofree Maybe a) -> a) -> Nat -> a

то есть внезапно принимает Maybe (Cofree Maybe a) -> a, аналог [a] -> a для связных списков.

Т.е. Nothing - это NULL, пустой указатель на список. Just (a :< Nothing) - это ненулевой указатель на конс-ячейку, с next = NULL. И т.д.

Если написать type instance Base (Maybe (Cofree Maybe a)) = ListF a и инстанс Recursive - то можно писать фибоначчи вот так:
fibN' :: Nat -> Integer
fibN' = histo $ \case
  (refix -> x:y:_) -> x + y
  _ -> 1
refix - это изоморфизм между обычными списками и Maybe (Cofree Maybe a), через гиломорфизм инициальных и терминальных (ко)алгебр. А конструкция refix -> ... - это view pattern.

04 марта 2017, 01:31

03 марта 2017

28 февраля 2017

Nikita Prokopov

ClojureCup 2015

По традиции, мы опять упоролись хакатоном.

TL;DR видео-демка

(Ссылка на голосование внизу поста)

Про идею

Меня давно волновало, что все сервисы для докладчиков какие-то, ну, никакие. Да, хочется поделиться слайдами после доклада (speakerdeck, slideshare), но хочется чтобы у презентации какая-то жизнь была после этого, а не «слил и забыл». Или можно «делать слайды» (google docs, prezi, slides.com), но мне вот не кажется, что ключ к крутому докладу в эффектных слайдах или головокружительных переходах. Т.е. это вишенка, но на торте, которого сейчас ни у кого нет. А то что есть — всё в разных уголках, сделал на google docs, показал из pdf, залил на slideshare, на вопросы отвечаешь в ЖЖ.

Так родился Deckatron — сервис презентаций, на котором можно придумать, создать, показать, ответить на вопросы, опубликовать свою презентацию и украсть чужую.

Начинается все с markdown-редактора. Текст накидывается прямо на сайте, и markdown, на мой взгляд, идеальный формат для того, чтобы быстренько записать, упорядочить разрозненные мысли и составить план. Беда всех редакторов слайдов — в них невозможно «думать», слишком много возни, чтобы поправить текст, поменять порядок, добавить пару мыслей. У нас вся презентация — один сплошной текстовый документ. Что может быть проще?

Дальше нужно добавить немного разметки (стандартные markdown заголовки, выделения, ссылки, списки, конечно, плюс разделители слайдов --- и ===). Из этого автоматически генерируются слайды. Важно, что если вы слайды уже почти сделали, а потом поняли, что нужен еще один раунд брейншторминга, вы остаетесь внутри того же самого удобного и гибкого текстового документа. В обычных редакторах чем полнее ты сделал слайды, тем сложнее что-то глобально реорганизовывать, и тем меньше хочется это делать.

У редактора есть WYSIWYG, так что в реальном времени видно, что там получается из слайдов (не переносится ли заголовок, входит ли код, не мешает ли фон). Подготовка заканчивается выбором цветовой темы.

Дальше по идее должен идти режим репетиции, но я пока не уверен, чем он должен от режима презентации отличаться. В любом случае, здесь у нас пока пусто.

И наконец презентация! Тут у нас все для этого и даже больше. Полноэкранный режим — разумеется.

Есть еще режим зрителя: когда ты заходишь на главную страницу, там есть секция «Live right now», т.е. презентации, которые прямо сейчас идут.

Если в такую ткнуть, она тоже откроется на полный экран и можно видеть, как докладчик переключает слайды в реальном времени. Удобно, если сидишь за колонной в зале, например. Плюс видно, сколько человек смотрит прямо сейчас (такое же есть на slides.com)

Ну и вторая важная фича — вопросы докладчику. Пока идет доклад, можно открыть специальный попап, задать вопрос или проголосовать за чужой (ради этого, например, существует целый отдельный сервис sli.do).

В конце доклада вставляется специальный слайд, на котором показаны наиболее популярные вопросы (да, больше не надо специально делать слайд «Вопросы?»). Естественно, всё это в реальном времени, без перезагрузок, на server push и вебсокетах. Мне нравится, как традиция (слайд в конце со словом «вопросы») реализуется современными технологиями на качественно новом уровне и начинает буквально выполнять ту функцию, которую она до этого только обозначала.

Наконец, что происходит после доклада? У вас хорошая порция материала, он уже структурирован, глупо выбрасывать его. Выложить слайды часто недостаточно. Видео делают долго (а ажиотаж штука быстро протухающая), да и смотреть его потом часто мучительно медленно. Декатрон позволяет доклад грамотно выложить — разбавить слайды комментариями, чтобы получился такой блог-пост с картинками. Можно начать с поста, потом добавить слайдов, можно сделать слайды, потом дописать комментарии — как больше нравится. Главное, что другие люди смогут это прочитать и извлечь пользу. Идея родилась два с половиной года назад, опробована тут, тут и тут.

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

Наконец, уже просто веселухи ради, мы прикрутили кнопку «Fork this deck», которой можно скопировать себе презентацию и поправить как угодно. Осмысленный вариант использования — самому делать вторую/третью/четвертую версию однажды уже рассказанного доклада. Неосмысленный — социализация, что ли?

Про реализацию

Мы сделали это все за двое суток командой из четырех человек. Clojure, ClojureScript, Http-kit, Rum, Transit, Instaparse. Без DataScript-а.

Экраны мы проектировали в Precursor (проект, выросший из ClojrueCup, между прочим), его даже можно посмотреть

Очень много углов срезано, держится буквально на соплях. Из страшного — markdown парсер мы писали сами, и он получился, что называется, «с особенностями». Синхронизация данных работает только по оптимистичному пути — если что-то пойдет не так, в лучшем случае undefined behaviour. Презентации хранятся в обычных файлах. Логинов нет, аутентификация по автоматически выдаваемой куке.

Короче, все, что не портит в первом приближении user experience, сделано по максимально простому пути. Фокус — на фичах, а не техническом совершенстве, которое, скорее всего, на таких масштабах никто не сможет оценить.

Из хорошего — мы сделали довольно изящную систему синхронизации. Взяли clojure.data/diff чтобы вычислять дельты между произвольными словарями и написали функцию patch которая может эти дельты применять. Дальше, на любое изменение мы шлем, бродкастим и применяем эти дельты где можем. Кайф в том, что механизм универсальный и автоматический, поэтому вся работа со стейтом локальная, ничем не ограниченая (меняй как хочешь), и где-то в фоне по волшебству просасывается ко всем. Например, вопросы на слайды я добавил где-то за час (из него минут 20 я сердечко для лайков искал), и написал 0 строк кода чтобы они были риалтаймовыми — они по-другому просто получиться не могли. В идеальном мире, конечно, данные будут не словарями, а CRDT, а редактор текста вообще OP, и тогда это еще и надежно заработает, но за два дня такого не успеть (ну или нужен опыт работы со swarm.js, которого не было).

Что я хочу сказать — в будущем, когда клиент-серверное общение будет настраиваться одной кнопкой по принципу «вот ip сервера, общайтесь», и дальше оно как-то само, в фоне, с fallback на localStorage и прочими оптимизациями, тогда заживем. Стоимость веб-приложений упадет до нуля практически (ну, если еще вместо box модели нормальные констрейнты прикрутят).

Заключение

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

Ну и я очень доволен, что мы сделали достаточно много фич, по крайней мере, чтобы показать поддержку полного цикла жизни презентации. Продуктивно и организованно провели два дня. Жалею только, что кнопка «Read» стоит до «Present», а не после.

ВАЖНО!

Как обычно, нам нужен ваш голос. Да-да, именно ваш! Если идея вас впечатлила, пройдите на clojurecup.com/voting, залогиньтесь через github и проголосуйте за Deckatron (команда The Other Guys).

В главных ролях:

Олександр Шишко, Михаил Акованцев, Ренат Идрисов и я.

Предыдущие серии: 2013, 2014

28 февраля 2017, 20:50

27 февраля 2017

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

Домашка по Топологии на ПНД

Lemma. Consider commutative triangle:

    { f = g . p,
      f: X -> Z,
      p: X -> Y,
      g: Y -> Z } where p: Quotient, g: Surjective.

Then f: Continuous <=> g: Continuous.


Record quot_class_of (T Q : Type) := QuotClass {
       repr : Q -> T;
       pi : T -> Q;
       reprK : forall x : Q, pi (repr x) = x }.

Record quotType (T : Type) := QuotType {
       quot_sort :> Type;
       quot_class : quot_class_of T quot_sort }

Record type_quotient (T : Type)
                     (equiv : T -> T -> Prop)
                     (Hequiv : equivalence equiv) := {
       quo :> Type;
       class :> T -> quo;
       quo_comp : forall (x y : T), equiv x y -> class x = class y;
       quo_comp_rev : forall (x y : T), class x = class y -> equiv x y;
       quo_lift : forall (R : Type) (f : T -> R), compatible equiv f -> quo -> R;
       quo_lift_prop : forall (R : Type) (f : T -> R) (Hf : compatible equiv f),
                       forall (x : T), (quot_lift Hf \o class) x = f x;
       quo_surj : forall (c : quo), exists x : T, c = class x
}.


____________
[1]. http://ai2-s2-pdfs.s3.amazonaws.com/1704/7a639180e384cea1f183cf9082e7e13f021a.pdf

27 февраля 2017, 00:09

25 февраля 2017

nponeccop

Сломаем всё!

https://github.com/ptol/oczor/blob/master/src/Oczor/Infer/Unify.hs#L21
/home/foo/oczor/src/Oczor/Infer/Unify.hs:21:3: warning:
    Pattern match checker exceeded (2000000) iterations in
    a case alternative. (Use -fmax-pmcheck-iterations=n
    to set the maximun number of iterations to n)

25 февраля 2017, 00:02

24 февраля 2017

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

Рантайм библиотека на Coq

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

CoREPL> spawn ack 4 1
20
CoREPL> spawn ack 4 1 
21
CoREPL> ls
[(20,ack,10043),(21,ack,10033)]
20:65533
21:65533
CoREPL> kill 20
Ok
CoREPL> send 20 "hello"
Error
CoREPL>


Вот такое написать — уже неплохая цель, думаю даже больше будет чем любые другие а ля VM на Coq. Странно конечно звучит писать обычные программы, а в полях держать поля username и password в теоремах, но почему нет?

В такое я думаю трансформировать со временем https://github.com/5HT/co
Кто там хотел в Групоид Инфинити, приходите писать на Coq будет весело https://gitter.im/groupoid/exe
Денег нет, популярности нет, чистейшее R&D под ваши нужды, предлагайте свои идеи, будем в эту сторону двигать! Область наших интересов в этом проекте: стрим процессинг, векторизация, стрим фьюжин (т.е. с вероятностью > 1/2 то же, чем вы занимаетесь у себя на производстве) компиляция в LLVM языки — точка соприкосновения с http://groupoid.space/hnc. Этот проект назовем в будущем условно co — такого двухбуквенного сочетания в домене проектов нашей вселенной Marvell еще не было — REPL интерпретатор и рантайм система для программирования на Coq.

24 февраля 2017, 13:52

nponeccop

осzor

https://github.com/ptol/oczor/blob/master/src/Oczor/CodeGen/CodeGenJs.hs#L7

Чувак конечно бох - взял правильную либу и ебанул приттипринтинг однострочником катаморфизмом. Cравнение явно не в мою пользу:

https://github.com/nponeccop/HNC/blob/master/CPP/Visualise.hs#L26

Надеюсь, я его уделаю в унификации. Он делал руками и там небольшие конюшенки:

https://github.com/ptol/oczor/blob/master/src/Oczor/Infer/Unify.hs#L16

Тут уже я взял правильную либу и ебанул:

https://github.com/nponeccop/HNC/blob/master/Unifier/Unifier.hs#L12
https://github.com/nponeccop/HNC/blob/master/Unifier/Restricted.hs#L21

Но прямое сравнение некорректно, т.к. у него в типах продукций больше. Надо будет его код унификаций и подстановок попробовать причесать через unification-fd.

С комманд-лайном я вроде тоже обломался - сейчас все молятся на optparse-applicative:

https://github.com/ptol/oczor/blob/master/src/Oczor/Compiler/CommandLine.hs#L10

A у меня System.Console.GetOpt который вообще из base:

https://github.com/nponeccop/HNC/blob/master/HNC.hs#L27
https://github.com/nponeccop/HNC/blob/master/Utils/Options.hs#L11

24 февраля 2017, 05:01

Откиньтесь на спинку кресла

Экспериментирую тут с со стеком. Как обычно я всё поломал своим нетрадиционным сетапом.

Их якобы реализованная поддержка setup-depends нифига не работает, хез как репортить.

В-общем, попытка сборки HNC стеком заканчивается на этапе компиляции Setup.hs. Стек не в курсах что требуется uuagc-cabal, хотя в setup-depends прописано.

Я буду долго смеяться ещё, впрочем, видя, как они наколенно эмулируют кабал (после того как починят это). Например хрен там они догадаются, что AG/Root.ag - это зависимость Bar.ag, который в свою очередь зависимость Bar.hs, который собирается в dist/build/что-то-там. Об этом кабалу сообщает плагин, ну а снойманы академиев не кончавшие видимо, и об этом не в курсах и эвристически это как-то эмулируют для наиболее частых случаев типа happy/gtk2hs.

Кроме того их стек собирает всё параллельно, отчего ему требуется уйма ОЗУ, т.е. не меньше 2 гиг (вариант c просто кабальным сендбоксом живет на гиге с полгигом свопа - оно только в ld бывает столько жрет и только иногда). В-общем, если у вас винда+виртуалка+4гб - будет очень тесно, грузитесь с лайвсиди. У меня впрочем 8.

Ну, а если сделать чтобы стек в одно ядро собирал - будет медленно. У меня на 3 мбитах говноинета бинарные версии хаскельных либ вытягиваются очень быстро по сравнению с их же сборкой на i3-4005U. Я чуть не уснул, пока ждал сборки зависимостей oczor стеком. Там их аж 77 (транзитивных) против 45 у HNC. А вытягиваются "хлоп-хлоп-хлоп", только конечно с бинарными ОС-пекеджами отдельные проблемы, не панацея или по-крайней мере нужно ещё растить инфраструктуру.

24 февраля 2017, 02:39

23 февраля 2017

nponeccop

Полку HNC прибыло

https://github.com/ptol/oczor

Обнаружился тут аналог. Буду у него фичи пиздить (а может и он у меня). Тем более что тоже на хаскеле и не в рабочекрестьянском стиле.

Насчёт планов по HNC - сейчас надо компонентизировать все "неинтересные" фрагменты типа тайп-чекера и кодогенератора. Доку по части тайпчекера Макс всё не выложит никак.

23 февраля 2017, 19:20

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

Языки и Программирование: Coq

Почему Coq не был офигенным еще 5 лет назад? Потому что никто не преуспел на его основе сделать язык общего назначения. Поискав "coq as general purpose language" вы пока ничего не найдете. На Coq дофига пакетов в OCaml, но большинство из них математические модели.
Но не на количество моделей надо смотреть, а можно ли на нем писать действительно что-то мощное, ну ладно мощное, хотябы хелоу ворлд и ехо сервер :-) 3 года назад Гиюм Кларе сделал веб-сервер Pluto, и если вы посмотрите на исходники, то найдете стиль poor man человека, с простенькими эфектами, простенькой функциональностью — но все работает. Я хотел прорекламировать сайт автора, но он почему-то лежит, поэтому я просто тут расскажу на пальцах.

Как только появится возможно писать нормальные хелоу ворлды и кто-то возьмется за базовую рантайм библиотеку, которая по производительности была бы хотя бы на уровне PHP, тогда можно выходить в продакшин местячково начинать, ну как мы с n2o. Но кто будет писать на зависимых типах n2o.coq спросите вы? Ну Haskell тоже все боялись, а сейчас каждый джаваскриптер видел уже PureScript и Elm и может на них писать. Так, что мое мнение такое, как только найдется чувак который сделает приятную писанину на Coq сразу появится говнокод и продакшин. Тем более, что для рантайм библиотеки хватит и System F. Я вижу, что Coq мне приятней чем Scala/Haskell, и что его можно окультурить, есть Notation, можно даже DSL строить прямо в языке.

Кстати про OCaml, он тоже довольно омолодился за последние 5 лет. Во-первых opam, во вторых более нормальный сайт, Multi-core OCaml, самый быстрый паттерн мачинг, ReasonML тоже. Кароче куча всего, Lwt по сути уже стандарт де факто, успех Джейн Стрит и т.д. Неспешный но прекрасный язык для командной разработки. В ЖЖ дофига чуваков пишут/писали на OCaml.

Я к чему веду, так как мы с вами 10 лет назад интересовались лямбдой, 5 лет назад зависимыми типами, так и сейчас это кто-то делает, и этого будет больше. Конечно сама теория зависимых типов создает некую элитарность, но успех таких чистых и приятных штук как PureScript говорит, что даже сложные вещи можно сделать простыми, для меня лично PureScript — это реинкарнация Miranda, т.е. System F язык каким он должен быть. Такой же реинкарнацией Coq является Lean, а позже и EXE. Но Coq in Coq круче будет чем EXE in Rust, к примеру.

Я думаю, что нужно продолжать дело coq.io, и искать новые рабочие формы в библиотеке рантайм типов (а не PhD хелоу ворлды, которые если чесно уже заебали, буду стараться сделать не очередной хелоу ворлд!). Эту библиотеку, как я ее видел для EXE, можно написать на Coq и попробовать на простеньких догфуд программах, ну а что мы пишем, WebSocket, бинарный стриминг и очередя. Так, что вцелом, мы в Coq вас не тащим, но сами стараемся туда попасть раньше чем вы.

23 февраля 2017, 16:04

Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake, Takuo Watanabe

Coq:
CoFixpoint behvA := receive (fun msg ⇒
match msg with
| name_msg sender ⇒ me ← self; sender ! name_msg me; become behvA
|_⇒ child ← new behvB; child ! msg; become behvA
end)

Erlang:
behvA() → receive Msg → case Msg of
{name_msg, Sender} → Me = self(), Sender ! {name_msg, Me}, behvA()
     _ → Child = spawn(fun() → behvB() end), Child ! Msg behvA()
end.

_______________
[1] http://amutake.github.io/actario/AGERE2015.pdf

23 февраля 2017, 03:50

22 февраля 2017

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

CoFixpoint Extraction REPL Prototype Zero

Ну что, я таки нанписал CoFixpoint корекурсию на коке. Точнее сразу REPL для коиндуктивного типа. No OCaml was involved.
$ brew install opam
$ opam install coq
$ opam install coq-io-system

Быстрый старт предполагает наличие всех необходимых opam модулей, которые в предыдущих постах я рассказал как насетапить, а если и не рассказал, то показал какие из них необходимые.
$ git clone git://github.com/5HT/co && cd co
$ make && cd extraction && make && ./main.native
ocamlbuild main.native -use-ocamlfind -package io-system
Finished, 5 targets (5 cached) in 00:00:00.
1
Input: 1.
2
Input: 2.
3
Input: 3.
CTRL-D


Что тут происходит, тут происходит нативный с точки зрения пи калкулуса процесс квантификации операционной бесконечности, комонада спрятаная внутри тайпчекера кока, преобразует корекурсию в потенциально бесконечный процесс на OCaml.

Здесь не используются никакие биндинги, кроме Lwt.

$ cat Main.v
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.
        Import ListNotations.

  CoInductive Co (E : Effect.t) : Type -> Type :=
    | Ret   : forall (A : Type) (x : A), Co E A
    | Bind  : forall (A B : Type), Co E A -> (A -> Co E B) -> Co E B
    | Call  : forall (command : Effect.command E), Co E (Effect.answer E command)
    | Split : forall (A : Type), Co E A -> Co E A -> Co E A
    | Join  : forall (A B : Type), Co E A -> Co E B -> Co E (A * B).

  Arguments Ret {E} _ _.
  Arguments Bind {E} _ _ _ _.
  Arguments Call {E} _.
  Arguments Split {E} _ _ _.
  Arguments Join {E} _ _ _ _.

  Definition ret   {E : Effect.t} {A : Type} (x : A) : Co E A := Ret A x.
  Definition split {E : Effect.t} {A : Type} (x1 x2 : Co E A) : Co E A := Split A x1 x2.
  Definition join  {E : Effect.t} {A B : Type} (x : Co E A) (y : Co E B): Co E (A * B) := Join A B x y.
  Definition call  (E : Effect.t) (command : Effect.command E):
                   Co E (Effect.answer E command) := Call (E := E) command.

  Notation "'ilet!' x ':=' X 'in' Y" := (Bind _ _ X (fun x => Y))
           (at level 200, x ident, X at level 100, Y at level 200).

  Notation "'ilet!' x : A ':=' X 'in' Y" := (Bind _ _ X (fun (x : A) => Y))
           (at level 200, x ident, X at level 100, A at level 200, Y at level 200).

  Notation "'ido!' X 'in' Y" := (Bind _ _ X (fun (_ : unit) => Y))
           (at level 200, X at level 100, Y at level 200).

  Definition read_line : Co effect (option LString.t) :=
    call effect ReadLine.

  Definition printl (message : LString.t) : Co effect bool :=
    call effect (Print (message ++ [LString.Char.n])).

  Definition log (message : LString.t) : Co effect unit :=
    ilet! is_success := printl message in
    ret tt.

  Definition run (argv : list LString.t): Co effect unit :=
    ido! log (LString.s "What is your name?") in
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some name => log (LString.s "Hello " ++ name ++ LString.s "!")
    end.

  Parameter infinity : nat.
  Parameter error : forall {A B}, A -> B.

  Fixpoint eval_aux {A} (steps : nat) (x : Co effect A) : Lwt.t A :=
    match steps with
      | O => error tt
      | S steps =>
        match x with
          | Ret _ v => Lwt.ret v
          | Call c => eval_command c
          | Bind _ _ x f => Lwt.bind (eval_aux steps x) (fun v_x => eval_aux steps (f v_x))
          | Split _ x1 x2 => Lwt.choose (eval_aux steps x1) (eval_aux steps x2)
          | Join _ _ x y => Lwt.join (eval_aux steps x) (eval_aux steps y)
        end
    end.

  Definition eval {A} (x : Co effect A) : Lwt.t A :=
    eval_aux infinity x.

  CoFixpoint handle_commands : Co effect unit :=
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some command =>
        ilet! result := log (LString.s "Input: " ++ command ++ LString.s ".") in
        handle_commands
    end.

  Definition launch (m : list LString.t -> Co effect unit): unit :=
    let argv := List.map String.to_lstring Sys.argv in
    Lwt.launch (eval (m argv)).

  Definition corun (argv : list LString.t): Co effect unit :=
    handle_commands.

  Definition main :=
    launch corun. (* launch run. *)

Extract Constant infinity => "let rec inf = S inf in inf".
Extract Constant error => "fun _ -> failwith ""Unexpected end""".
Extraction "extraction/main" main.


Это то что мы ребятки называем основой верифицированного ядра операционной вычислительной среды для моделирования пи калкулуса и доказательства его основных теорем о бисимуляции, модальных логик и верификации протоколов, и просто для тестирования любых математик в интерактивной среде со своим простым интерпретатором. Наша цель создать единую среду для работы математиков и программистов, где экстракты моделей сразу линкуются с высокопроизводительным CAS рантаймом и CPS интерпретатором. Проверяйте ваши датасеты сразу на моделях заэкстракченых в Rust или OCaml, которые запускаются на seL4, Xen или Mac/Linux. Такой стартап, дали бы денег? :-)

22 февраля 2017, 22:38

nponeccop

Объектоидный макропаскаль

Пришла в голову идея реально упоротого языка синтаксиса. Берём hn0 и переставляем местами функцию и её первый аргумент:
l foldl cons nil =
	acc = nil
	while l neq null
		acc := acc cons (l data) 
		l := l next
	acc
Трансляция в функциональный ЖС:
function foldl(l, cons, nil) {
	let acc = nil 
	while (l != null) {
		acc = cons(acc, data(l))
		l = next(l)
	}
	return acc
}
Преимуществ как минимум два: бесплатные инфиксные операции и автокомплит в объектном стиле. Трансляция в объектный ЖС:
function foldl(l, cons, nil) {
	let acc = nil 
	while (l.neq(null)) {
		acc = acc.cons(l.data())
		l = l.next()
	}
	return acc
}
Но это конечно же не объекты, а что? Пусть будут объектоиды! Ещё у нас все ФВП это макросы, а ":=" и общая убогость - как в паскале. Оружие массового поражения!

Лексический синтаксис любой можно налепить. Хоть как в жс.

22 февраля 2017, 21:49

Влажные мечты о категорной имплементации математики

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

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

Сегодня столкнулся с проблемой, что в Coq нет доки по структурной коиндукции и коиндуктивным типам.

Нет чтобы просто сказать, что СЕПУЛЬКАРИИ — устройства для сепуления структурная корекурсия встроена в ядро, продуктивность фикспоинтов коалгебр постулируется, а ключевое слово CoFixpoint просто говорит коку, что дальше у нас Мю Ню и коалгебра.

Вместо этого у них целый туториал как официальная дока, где рассусоливают на 5 страницах что-то про guardedness. Тьфу на них.

22 февраля 2017, 20:56