Russian Lambda Planet

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

придумайте какую-нибудь теорию

Задача из учебника по физике: «Запишите уравнение Менделеева—Клапейрона. Придумайте задачу на его применение и решите её». По мотивам я придумал свою: «Изучите теорию категорий. Научите теории категорий других. Придумайте ещё какую-нибудь теорию».

21 июня 2017, 12:31

24 мая 2017

Nikita Prokopov

Читабельная Кложа

Обнаглел настолько, что код вставляю скриншотами

http://tonsky.me/blog/readable-clojure/

24 мая 2017, 14:09

05 мая 2017

Yan Tayga

Курс по Хаскелю на русском, часть 2

Почти закончил курс -- еще есть что решать и можно решать, конечно, но на праздники возможности уже не будет.

По итогам - по глупости завалено 1 peer review, не решена 1 задачка на строгость, не решены 2 задачи на continuation и еще одна задачка на разобраться с типами применяя расширения ghc. Все остальное вроде нормально более менее и понятно.

Курс сам по себе просто отличный. Был бы еще лучше, если бы:
- подробнее бы рассмотрели continuation -- темы вроде на целую неделю вполне хватит, с нормальными постепенно возрастающей сложности задачами. Все таки интересная штука.
- изредка тщательнее формулировались задачи. Впрочем, по отзывам они часто тут же исправлялись командой курса.
- больше задачек не якобы «творческих» и с подвохом, а более рутинных, закрепить понятый материал. Ucucuga в обучении, имхо, не самый лучший выбор.

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

05 мая 2017, 09:29

28 апреля 2017

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

Le Coq` Art

Печатнул обе версии, Французскую и Английскую!



Издательство sagarasousuke

28 апреля 2017, 16:37

24 апреля 2017

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

Quelea — a declarative programming model for eventually consistent data stores

The store is a collection of replicas, each storing a set of objects (x, y, . . .) of a replicated data type. For the sake of an example, let x and y represent objects of an increment-only counter replicated data type (RDT) that admits inc and read operations.

We say that the effects inc1x and inc2x are visible to the effect (inc4x) of x.inc, written logically as vis(inc1x, inc4x) ∧ vis(inc2x, inc4x).

To capture happens-before, we define an irreflexive transitive session order relation that relates the effects of operations arising from the same session. For example, in Fig. 1, inc4x and inc5x are in session order (written logically as so(inc4x, inc5x)).

same object session order (soo = so ∩ sameobj)
same object happens-before order (hbo = (soo ∪ vis)+)
happens-before order (hb = (so ∪ vis)+)

Causal Visibility (CV) ::= ∀a, b, c. hbo(a, b) ∧ vis(b, c) ⇒ vis(a, c) 
Causal Consistency (CC) ::= ∀a, b, c. hbo(a, b) ⇒ vis(a, b)
Strong Consistency (SC) ::= ∀a, b. sameobj(a, b) ⇒ vis(a, b) ∨ vis(b, c)

Read Your Writes (RYW) ::= ∀a,b. soo(a, b) ⇒ vis(a, b)
Monotonic Reads (MR) ::= ∀a,b,c. vis(a, b) ∧ soo(b, c) ⇒ vis(a, c)
Monotonic Writes (MW) ::= ∀a,b,c. soo(a, b) ∧ vis(b, c) ⇒ vis(a, c)
Writes Follow Reads (WFR) ::= ∀a,b,c,d. vis(a,b)∧vis(c,d)∧(soo ∪ =)(b,c) ⇒ vis(a,d)

∀a,b,c.txn{a,b}{c} ∧ sameobj(a,b) ∧ vis(a,c)⇒vis(b,c)
∀a,b,c.txn{a}{b,c} ∧ sameobj(b,c) ∧ vis(b,a)⇒vis(c,a)

∀(a, b : getBalance),
 (c : withdraw ∨ deposit),
 (d : withdraw ∨ deposit). txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ so(a,b) ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)


ШИВА-РАМА-КРИШНА-Н!
______________
[1]. http://kcsrk.info/papers/quelea_ieee16.pdf
KC Sivaramakrishnan, Gowtham Kaki, Suresh Jagannathan
IEEE Data Engineering Bulletin, 39(1): 52 64, March 2016

24 апреля 2017, 17:06

22 апреля 2017

nponeccop

Avoiding success is..

Вместо эпиграфа:
---
Every 2nd grader knows that the C++ template system is Turing complete. So what? Compile time Brainfuck evaluator that’s what!
---

Надо выпустить какой-нибудь сойлент с вкладышами "Avoiding success is.."

22 апреля 2017, 17:30

21 апреля 2017

Dee Mon journal

Streams

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово Inf, и поле оказывается "ленивым": когда данные конструируются, выражение для вычисления этого поля не вычисляется сразу, а автоматически оборачивается в Delay (если явно поленился это сделать), а при паттерн-матчинге оно когда надо автоматически форсится через Force (т.е. механика практически как в окамле с ленивыми значениями, но вручную необязательно оборачивать и форсить, компилятор сам вставляет).
Например, через этот механизм сделан тип бесконечных последовательностей:
data Stream : Type -> Type where
(::) : (value : elem) -> Inf (Stream elem) -> Stream elem

Благодаря автоматическому расставлению делеев и форсов, код с такими коданными выглядит так же просто и чисто, как в хаскеле:
countFrom : Integer -> Stream Integer
countFrom x = x :: countFrom (x+1)

first : Nat -> Stream a -> List a
first Z xs = []
first (S k) (x :: xs) = x :: first k xs

prepend : List a -> Stream a -> Stream a
prepend [] ys = ys
prepend (x :: xs) ys = x :: prepend xs ys

Обратите внимание, что в функциях выше :: используется в паттерн-матчинге и в конструировании сразу и для списков и для стримов, компилятор сам по типу понимает где что, и для стримов вставляет delay/force.
Подобно Основной Теореме Арифметики и Основной Теореме Алгебры, есть Основная Теорема Функционального Программирования (это, по Карри-Говарду, конечно же тоже функция), ее можно записать так:
fibs : Stream Integer
fibs = 1 :: 1 :: zipWith (+) fibs (drop 1 fibs)

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

— Не пугайтесь, Екатерина Петровна, и не волнуйтесь. Только нет в мире никакого равновесия. И ошибка-то всего на какие-нибудь полтора килограмма на всю вселенную, а все же удивительно, Екатерина Петровна, совершенно удивительно!

21 апреля 2017, 18:17

верифай, но проверяй

This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: IronFleet (Dafny/C#), Verdi (Coq/OCaml), and Chapar (Coq/OCaml). Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients, and invalidating verification guarantees.
https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
В протоколах и их доказанных реализациях багов не нашли, все баги были на границе взаимодействия верифицированного кода с жестоким внешним миром - неверифицированным окружением. Сложно описать формально все возможные косяки низкоуровневых библиотек и сторонних процессов. Смешной момент - Dafny для верификации использует Z3 солвер, если солвер невовремя прервать, Дафни считает, что все ок и считает недопроверенную программу годной.

А тут мужики нагенерили много тестовых программок для компиляторов:
In less than six months, our approach has led to 217 confirmed GCC/Clang bug reports, 119 of which have already been fixed ... In about three weeks, we have also found 29 CompCert crashing bugs, and 42 bugs in the production Scala compiler and the Dotty research compiler.
https://arxiv.org/pdf/1610.03148.pdf
GCC и Clang могут падать, а могут неправильный код генерить. CompCert (который на Coq'e верифицирован), как я понял, неправильный код не генерит, но вот сам падать может - ассерты срабатывают внутри, т.е. некоторая неконсистентность логическая там была.

21 апреля 2017, 06:50

17 апреля 2017

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

Пронумеруем типы и их значения

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

encode (X: Type) -> Nat
decode (X: Nat) -> (Sig: Type, Values: Stream Sig)


Еще это можно назвать — глобальное управление контекстами. Функция decode — может состоять из генератора Values: Nat -> Sig, который аллоцирует в виртуальной машине уникальный инстанс типа Sig по заданному Nat. Таким образом каждая возможная переменная в пространстве типов и термов на всех уровнях может индексироваться тройков Nat значений (Nat,Nat,Nat) — индекс вселенной, индекс типа, и индекс инстанса.

Конструирование термов в зависимом тайпчекере:

0 — UNIT      =
1 — NORM      = Nat      // normalisation
2 — SUBST     = Nat      // substitution 
3 — STAR      = Nat      // universe        
4 — REC       = Nat      // Cons: A -> List A -> List A
5 — VAR       = Nat Nat  // Nat, Bool, List A, Vec Nat A
6 — OR        = Nat Nat  // data
7 — AND       = Nat Nat  // record
8 — EQ        = Nat Nat  // definition 
9 — PI        = Nat Nat Nat
A — FUN       = Nat Nat Nat
B — TYPECHECK = Nat        


Пример:

encode "List A = Nil: List A | Cons: A -> List A -> List A"

0 — UNIT        // "A"
1 — UNIT        // "Nil"
2 — UNIT        // "Cons"
3 — UNIT        // "List"
4 — VAR 0 _     // A
5 — VAR 3 4     // List A
6 — REC 5       // Rec List A
7 — AND 4 6     // (A, Rec List A)
8 — VAR 2 7     // Cons: A -> List A
9 — VAR 1 _     // Nil:
A — OR 9 8      // Nil: | Cons:
B — EQ 5 A      // List A = Nil: List A | Cons: A -> List A -> List A


— основные конструкторы, которые индексируют (кроме Unit), некоторую переменную в таблице имен (индексы де Брейна), значение которой составляет тройка, таким образом словарь контекстов — List (Nat, (Nat, Nat, Nat)) — закодирован списком пар.

Для сравнения, List A в формате Lean:

1 — NS 0 u
2 — NS 0 list
3 — NS 0 α
1 — UP 1
0 — ES 1
1 — EP BD 3 0 0
4 — NS 2 nil
2 — EC 2 1
3 — EV 0
4 — EA 2 3
5 — EP BD 3 0 4
5 — NS 2 cons
6 — NS 0 a
6 — EV 1
7 — EA 2 6
8 — EV 2
9 — EA 2 8
A — EP BD 6 7 9
B — EP BD 6 3 10
C — EP BI 3 0 11
D — IND 1 2 1 2 4 5 5 12 1

17 апреля 2017, 16:36

13 апреля 2017

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

Семинары в НАН

Мне кажется мой доклад на прошлом семинаре про категорную семантику индуктивных типов прошел хорошо. Видео записали, скоро выложу.

Приходите на следующий семинар:

20.04.2017, Четвер
Семінар: Похiднi категорiї та їх застосування
Керівники: В.В. Любашенко
Місце: Інститут математики НАН України, вул. Терещенківська, 3, 219/305
Час: 15:30
Доповідач Ю.М. Беспалов
Доповідь: Кубічні групоїди
Резюме: За мотивами книги Ronald Brown, Philip J. Higgins, Rafael Sivera, Nonabelian Algebraic Topology: Filtered Spaces, Crossed Complexes, Cubical Homotopy Groupoids

Трейс семинаров:

Модератор: В.В. Любашенко. Провідний співробітник відділу топологій інституту математики НАН України

1. 30.03.2017 С.І.Максименко: Враження від гомотопічної теорії типів. Голова відділу топології інституту математики НАН України
2. 06.04.2017 М.Е.Сохацький: Категорна семантика індуктивних типів. Групоїд Інфініті
3. 20.03.2017 Ю.М. Беспалов: Кубічні групоїди. Існтитут теоретичної фізики НАН України

13 апреля 2017, 00:28

12 апреля 2017

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

Рекомендации от Mad Advisors Corp



Куда ИНВЕСТИРОВАТЬ, что НАСЛЕДОВАТЬ или ВОРОВАТЬ, на что ориентироваться:

Binary Protocols and Protocol Stacks (CORBA and SOAP Replacement)

— WebSocket
— SVG
— MQTT
— N2O
— ASN.1

Storage Systems (CODASYL and MUMPS Replacement)

— Aerospike (SSD)
— BlazingDB (GPU)
— PumpkinDB (FORTH, AVX) — лучший хакатон стартап на расте, авансом

Array Processing Languages (Fortran replacement)

— Futhark (GPU)
— Julia (AVX)
— AutumnAI (ML)

Concurrency Runtime and Languages (Ada Replacement):

— Pony (Runtime+Language, Erlang replacement, Zero Copy, CAS)
— Erlang, LING (Runtime+Language, Poor man)
— Rust (Language, Zero Copy)

R&D Languages (AUTOMATH replacement):

— Coq
— Z3
— Lean
— F*

Target Languages / Platforms for Runtime (Pascal Replacement):

— OCaml
— LLVM/MIR
— Rust
— D
— GHC

New Markets (Inexistant satisfaction) — озеро, где живут Синие Птицы и Черные Лебеди:

— VHDL FPGA toolchain replacement
— SIP/VoIP/RTP replacement
— Xen, Hyper-V, EXSI replacement
— Wolfram Mathematica replacement
— Lisp Machine replacement
— seL4 replacement

Куда НЕ ИНВЕСТИРОВАТЬ, от чего УБЕГАТЬ или что СОЗЕРЦАТЬ:

— JSON, XML, MessagePack, Text Protocols, ...
— HTML, Virtual DOM, React, Angular, Literally Any JavaScript Framework ...
— HTTP 1, 2, 3, 4, ...
C-Style Languages: Go, C, C++, JavaScript, TypeScript, ES6, ASM.JS, ...
Any LISP: Clojure, Common Lisp, Smalltalk, Self, Io, ...
Big VMs: JVM, CLR, ...
Просто унылое говно: Go, C#, Java, PHP, Scala, Python, PHP, Ruby, Elixir, Perl, node.js ...
Any RDBMS: SQL, MySQL, PostgreSQL, Oracle, ...
British Languages: Haskell, Agda, Idris, ...
APL Languages: K, J, Q, APL, ...
Almost any DHT: Riak, Cassandra, Spark, Hadoop, RethinkDB, CouchDB, Memcache, BDB, Tokio, MongoDB, Redis, ArangoDB, Neo4j, AllegroGraph, OrientDB, OrientDB
Almost any serializers: gRPC, Protobuf, Thrift, ...
Modern way of devops: Kubernetes, Docker, ...
Any product built by Google: Go, TensorFlow, Android, Blockly, Dart, Polymer,
Big Operaing Systems: UNIX, BSD, Linux, Windows, Mac

Список Обновляется. Коментарии Пендинг. Дискас.

Ты выше ЖЖ и не хочешь оставлять контент? Будь Анонимным!
Есть альтернативный канал комментирования https://erlach.co/pr/77c

Follow Back:

http://nponeccop.livejournal.com/556778.html

12 апреля 2017, 07:58

nponeccop

От чего бежать (языки)

Тут наш фашист-консультант сделал наброс типа по тру и не тру технологиям, прошлому и будущему.

Я придумал альтернативную мудаческую схему реальности. Есть академия - пишут "в стол". Есть хипсторы - пишут свистопердящую никому не нужные но красивые игрульки. И промышленные зрелые практики - пишут мейнстрим.

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

- Академия Хипсторы Мейнстрим Ретрограды
Прошлое ML, Coq, ACL2 CL, Ruby, R Сobol, Perl, Ada, C, C++ Scheme, VB6/.Net, PHP, Java, ObjC, D
Настоящее GHC Node, Scala, Erlang C++, Python, JS, Java, PHP С99, Go, Rust, Swift, Dart
Будущее F*, Z3, Lean Purs, Jupyter, Polly C++/OpenCL/OpenAcc, C#, Python, JS, TS


Тут надо комментировать каждую клетку

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

Хипсторы прошлого - CL это совсем далёкое прошлое, Ruby полупрошлое а R вот недавно. Имхо всё же R уступит своё место Питону. А там, где у питона кишка тонка - R уступит место всяким Julia under Jupyter. Джулии нет нигде в табличке, поскольку я вижу её, как чуть более прогрессивную и менее убогую сестру R, Питона и Матлаба.

Мейнстрим прошлого - тут только заведомый мейнстрим не столь далёкого прошлого. Языки упорядочены по моему пониманию степени ужаса программиста, столкнувшегося с соответствующим лигаси.

Ретрограды прошлого - ретрограды, с которыми всё ясно. PHP и Java успешно выполнили ретроградскую миссию и попали в мейнстрим, VB6 умер но VB.Net поддерживается в коме, ObjC если б не монополия/диктаторство Эппл тоже бы умер.

Академия настоящего - тут академия у которой есть шанс попасть на место Инрии в будущем. Я к сожалению мало знаком с академией, которая с одной стороны достаточно прогрессивна, а с другой стороны - работоспособна. Но GHC этому условию удовлетворяет. В отличие от всяких говноидрисов и прочих попыток избежать написания ленивого редуктора. Думаю GHC к 12 версии превратится в унылое но уже совершенно рабочее и зрелое говно.

Хипсторы настоящего - со Скалой проще всего. Если унылые энтерпрайзники жабошарпопитоновые собрались и решили писать стартап во имя блага всех существ - будут писать на Скале пить дать. Эрланг это для лиспорубепохапепитонистов решивших выпендриться. Нода достаточно забавна поскольку по сути лингва франка и не пишет на ней только ленивый лжавист или сишарпник. Для тех же плюсовиков скажем libuv подарок судьбы. Как в конце 1990-х на С++ разве что сайты не писали. Имхо всё из этой клетки просто со временем перекочует в "хипсторы прошлого". СL вот тоже достаточно хорош и хипстотен, но у него нет яркого будущего. Как и у ноды.

Мейнстрим настоящего - тут всё понятно, только нет Рубей, Р и С#. C# в мейнстриме по всем параметрам, но юные веб-падаваны не в курсе того что винда нужна и считают C# маргинальным, хоть он в первых строчках как не считай. Но МС продавливает его на линукс как Сан продавливала джаву куда только можно, и я считаю продавит.

Ретрограды настоящего - все на слуху (кроме может Dart и Swift). C99 отдельная категория. Это мейнстрим, но с ретроградским уклоном, и его адептов можно разделить на 3 категории: рокет саентисты, показывающие зиллионы попугаев там где конкуренты гордятся что у них овер 8000 или на самодельной гармонике играющие лучше чем иные на покупной, жертвы (например эмбедщики у которых просто вендор не написал кроме С ничего другого) и ебанаты (там как GNU-сексуалисты, так и школота жизни не видевшая, олд скул юникс вейщики, и просто упоротые - в общем в сортах специалистом не являюсь). Раст, свифт - можно сказать продолжатели своих соседей этажом выше (D и ObjC). Dart, Go - унылые высеры а ля PHP/нода но got traction.

Будущее лучше в обратном порядке описывать. Я вот не знаю что будет логическим продолжением ретроградской колонки. Ждём пока текущие начнут обсираться и будут предложены новые на их место. Я болею за C99 (может станет гошечкой), Go (может станет си для дебилохипсторов) и Rust (может присоединится к С++ в упоротых конторах, неупоротые говорят что в принципе юзабельно уже сейчас или через год будет).

Джава останется мейнстримом, но превратится в глазах общественности в унылый мейнстрим типа похапе сейчас. Т.е. станет "мейнстримом прошлого". Её место займет C#, в который будут вливать не рандомно-базарные фичи JSR а всякие няшки из ресёрча типа монад компрехеншонов Linq. Ну и под линухом МС запилит с JVM оракловской вряд ли победу - но уверенную ничью. А то и JetBrains купит - на такие кинжалы в спину МС горазда.

Python таки заборет R и Ruby, особенно в свете истерии machine learning. JS станет подобием чистых сей для ебанатов, а TS подобием C++ для промышленных зрелых видавших жизнь практиков с детьми которые будут юзать дремучее и уебищное админподмножество (заметьте и тут длинная рука MS).

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

Lean - в целом направление MLTT-пруверов с уклоном в HoTT

Z3 - направление ультрафинитных слабых логик и арифметик, типа битовых векторов SMT-LIB, я вижу очень перспективным. Долой мракобесие натуральных чисел и Тьюринг-полноты!

F* - направление gradual semi-automatic verification, гибрид модел-чекера, refinement typing, наколенного стат. анализатора и предыдущих двух направлений в рассчёте на экспорт в Бангалор.

12 апреля 2017, 06:53

09 апреля 2017

08 апреля 2017

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

Ватные Зав Типы

Зашел на канал, который гордо именуется зависимые типы: https://t.me/joinchat/AAAAAD9SWO-kmHf9o6Cn-Q, где сидят люди, которые нихуя не знают ни про пи калкулус, ни про лямбда исчисление, по великодушному приглашению моего антагониста 4da. Ни одной статьи полезной, репосты Вадлера (как он то к зависимым типам относится?) и Хаскелей. Ни одной новой темы, ничего. Болото, как и в ебантом ИТ, как и везде. Групоид Инфинити очевидно планку поднял высоко, не думаю что кто-то в Русском Мире до нее допрыгнет. Рома Михайлов вроде высоко парит, но практического применеия его FR языку, кроме как кодировать слова Хуй и Пизда я не вижу.

В конце чата мне предолжили стать оппонентом на защите (чувак с SLC на канале с зависимыми типами), я сказал, что после капитуляции России я сразу же приеду. На что мне сказали, что политека запрещена и я съебался (после того как меня забанили, еще смеялся ехидно, одминчег)! Хорошо, что видосы Вадлера и Хаскель System D разрешены.

В совете админов nivanych, который пизданулся и говорил мне что с Бандерой не так все очевидно как кажеться, сидя у себя в российских ебенях, а второй админ clayrat и глазом не моргнул, хотя живет не в России. Все-таки телеграм ужасно неудобный для чата. Хорошо, что все наши чаты в гиттере.

Кто говорит, что я нихуя не делаю и Групоид Инфинити хуйня, зайдите на канал и охуейте от контента, там 60 человек, саммый большой чат в России по зависимым типам. Нищета. Зайдите почитайте, кто любит срачи. Последнее слово будет Гаага и сказано будет в Гааге!

Вот вам свежая аналитика, по войне, которой нет, пацаны с зав типами:

https://www.youtube.com/watch?v=RQjhqD0fHeo

https://www.youtube.com/watch?v=hqfzOxnx7yI

Ставлю тег Компьютер Сайнс, чо.

Все групповые чаты, которые создают русские обречены на забвение, так было с erlang-russian, так было с ЖЖ, так было с Juick, так стало с FPROG, так будет и с Зав Типами! Ноль контента — одна вата.

08 апреля 2017, 16:54

07 апреля 2017

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

Феномен постоянного повышения ставок

http://www.cs.virginia.edu/~robins/YouAndYourResearch.html

When you are famous it is hard to work on small problems. This is what did Shannon in. After information theory, what do you do for an encore? The great scientists often make this error. They fail to continue to plant the little acorns from which the mighty oak trees grow. They try to get the big thing right off. And that isn't the way things go. So that is another reason why you find that when you get early recognition it seems to sterilize you. In fact I will give you my favorite quotation of many years. The Institute for Advanced Study in Princeton, in my opinion, has ruined more good scientists than any institution has created, judged by what they did before they came and judged by what they did after. Not that they weren't good afterwards, but they were superb before they got there and were only good afterwards.

07 апреля 2017, 13:45

04 апреля 2017

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

Cutting Edge: New Basis for HITs

Andrej Bauer, Niels van der Weide

Theorem: if we have the coequalizers, path coequalizers, and colimits, then we have all HITs. Uses function extensionality.

_______________
[1]. http://5ht.co/three.pdf
[2]. https://github.com/verimath/hit

04 апреля 2017, 21:00

Anton Salikhmetov

Еще одно введение в веревочковедение

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

Сети взаимодействия (interaction nets) - это структуры, подобные графам, состоящие из агентов (agents) и дуг. Агент типа α

имеет арность ar(α) ≥ 0. Если ar(α) = n, то агент α имеет n дополнительных портов (auxiliary ports) x1,..., xn в дополнение к его главному порту (principle port) x0. Все типы агентов принадлежат множеству Σ, называемому сигнатурой (signature). К любому порту можно присоединить не более одной дуги. Порты, которые не соединены ни одной дугой, называются свободными (free ports). Совокупность всех свободных портов в сети называется ее интерфейсом. Разводка (wiring) ω

состоит исключительно из дуг. Индуктивно определяемые деревья (trees)

соответствуют термам t ::= α(t1,..., tn) | x в исчислении взаимодействия (interaction calculus), где x называется именем (name).

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

что в исчислении взаимодействия будет соответствовать конфигурации (configuration)
<t1,..., tm | v1 = w1,..., vn = wn>,
где ti, vi, wi - некоторые термы. Последовательность t1,..., tm называется интерфейсом (interface), остальное же представляет собой мультимножество уравнений (equations). Разводка ω транслируется в выбор имен, и каждое имя обязано иметь ровно два вхождения в конфигурации.

Как и в λ-исчислении, в исчислении взаимодействия естественным образом определяются понятия α-конверсии и подстановки (substitution). Оба вхождения любого имени могут быть заменены на новое имя, если оно не участвует в данной конфигурации. Если терм t имеет ровно одно вхождение имени x, то подстановка t[x := u] определяется как результат замены имени x в терме t некоторым термом u.

Когда два агента соединены своими главными портами, они формируют активную пару (active pair). Для активных пар можно ввести правила взаимодействия (interaction rules), которые описывают, как активная пара будет заменена во время редукции сети взаимодействия. Графически любое правило взаимодействия можно преставить следующим образом:

где α, β ∈ Σ, а сеть N представлена с помощью разводок и деревьев в виде, пригодном для исчисления взаимодействия: в нотации Lafont это соответствует
a[v1,..., vm] >< β[w1,..., wn].
Говорят, что сеть без активных пар находится в нормальной форме (normal form). Сигнатура и множество правил взаимодействия вместе задают систему взаимодействия (interaction system).

Теперь рассмотрим пример для введенных конструкций, в котором участвуют часто использующиеся агенты ε и δ. В нотации Lafont правила взаимодействия для удаляющего (erasing) агента ε

записываются как ε >< α[ε,..., ε], а правила для дублирующего (duplicating) агента δ

выглядят следующим образом:
δ[α(x1,..., xn), α(y1,..., yn)] >< α[δ(x1, y1),..., δ(xn, yn)].
В качестве примера сети, в которой участвуют правила удаления и дублирования, возьмем простую сеть которая не имеет нормальной формы и редуцируется к самой себе:

В исчислении взаимодействия такая сеть соответствует конфигурации
<∅ | δ(ε, x) = γ(x, ε)> без интерфейса.

Редукция для конфигураций определяется более подробно, чем для сетей. Если
a[v1,..., vm] >< β[w1,..., wn], то следующая редукция:
<... | α(t1,..., tm) = β(u1,..., un), Δ> → <... | t1 = v1,..., tm = vm, u1 = w1,..., un = wn, Δ>
называется взаимодействием (interaction). Когда одно из уравнений имеет форму x = u, к конфигурации применимо разыменование (indirection), в результате которого другое вхождение имени x в некотором терме t будет заменено на терм u:
<...t... | x = u, Δ> → <...t[x := u]... | Δ> или <... | x = u, t = w, Δ> → <... | t[x := u] = w, Δ>.
Уравнение t = x называется тупиком (deadlock), если x имеет вхождение в t. Обычно рассматривают только сети, свободные от тупиков (deadlock-free). Вместе взаимодействие и разыменование задают отношение редукции на конфигурациях. Тот факт, что некоторая конфигурация c редуцируется к своей нормальной форме c', где мультимножество уравнений пусто, обозначают через c ↓ c'.

Если вернуться к примеру незавершающейся редукции сети, то бесконечная редукционная цепочка, начинающаяся с соответствующей конфигурации выглядит следующим образом:
<∅ | δ(ε, x) = γ(x, ε)> →
<∅ | ε = γ(x1, x2), x = γ(y1, y2), x = δ(x1, y1), ε = δ(x2, y2)> →*
<∅ | x1 = ε, x2 = ε, x = γ(y1, y2), x = δ(x1, y1), x2 = ε, y2 = ε> →*
<∅ | δ(ε, x) = γ(x, ε)> → ...

На нашем языке программирования, который подобен yacc(1)/lex(1) по структуре и лексически близок к LaTeX-нотации для исчисления взаимодействия, тот же самый пример можно записать следующим образом:
\epsilon {
        console.log("epsilon >< delta");
} \delta[\epsilon, \epsilon];

\epsilon {
        console.log("epsilon >< gamma");
} \gamma[\epsilon, \epsilon];

\delta[\gamma(x, y), \gamma(v, w)] {
        console.log("delta >< gamma");
} \gamma[\delta(x, v), \delta(y, w)];

$$

\delta(\epsilon, x) = \gamma(x, \epsilon);
Отметим, что наш язык программирования позволяет записывать побочные действия в императивном стиле, таким образом давая возможность исполнять произвольный код, включая ввод-вывод, а также условные множественные правила для пар вида αi >< βj в зависимости от значений i и j, которые могут быть произвольными данными, привязанными к агентам.

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

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

P. S. Недавно адаптировал этот текст и дополнил им статью на Википедии.

comment count unavailable comments

04 апреля 2017, 20:17

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

Idris 1.0

Make yourself unemployable (like I did) in 6 months with the book that recruiters don’t want you to know about

04 апреля 2017, 19:15

Российская Интеллигенция

Когда началась война ни один глубокоуважаемый господин из российского компьютер сайнс или математик не написал четкой позиции по этому вопросу. А как TOC в ЖЖ поменяли, так сразу Путин должен уйти в отставку. В отставку блядь! Не Гаага, нет, отставка!

04 апреля 2017, 07:52

01 апреля 2017

Scala@livejournal.com

Event Sourcing и Моноид

Вот говорят, что есть т.н. event sourcing, когда в базу записываются только event-ы, например
"изменить значения таких-то полей у такой-то instance-a такой-то entity", "удалить такой-то instance" и т.д. А потом по последовательности этих event-ов можно восстановить весь state.

Выглядит это восстановление так: каждый event превращается в функцию: State => State, которые потом "композируются". Поскольку A => A с операцией andThen образуют моноид, то процесс восстановения можно записать:
def createTransform(e: Event): State => State = ...
val transform = events foldMap createTransform
transform(state)
Логично ?
Даёт ли нам что-то использование абстракции моноида ?
Есть ли какие-нибудь примера использования моноида для event sourcing ?

написал Michael 01 апреля 2017, 15:53

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

Лучший отпуск в моей жизни

Как все-таки офигенно ничего не делать, а крутить лямбды и категории. Благодаря Владу я бросил работу и мы ходим с ним на лекции по Гомотопической Теории в НАН Украины. Инстайты продолжают струиться, нейронная сеть дышит полным своим дыханием. Как говорится, лучше с умным потерять, чем с дураком найти.

Влад не только трансформировал kievfprog, значительно повысив планку, отфильтровав примитивные доклады джаваскриптеров и кложуристов, но и делает, то, что называется фьюжин фундаментальной науки и инженерного искусства. Что интерсно, тусовка функциональных программистов Киева понравилась академикам, и теперь мы проводим регулярные семинары по четвергам. Например вот такие:



Я был приятно удивлен, увидев на семинаре бывших сотрудников doxtop с Плейтека, которые пишут там на scalaz и purescript с подачи доктора. Сам доктор, как и мы с Владом, не выдержал гнета гильд-энергии бабла и тоже решил дауншифнуться почитывая геометрические доклады про сигма слоения и их пи сечения.

Поэтому я решил написать этот пост. Я хочу, чтобы все кому интересно, то чем мы занимемся в Групоид Инфинити, нашли в себе силы потратить 2 часа ваших четвергов на семинары, которые проводит Вова совместно с НАН Украины :-) Для меня это площадка и возможность не придать забвению Пашину работу, а продолжить ее на академическом уровне привлекая лучших специалистов в этой области. Можете считать это моим извинением за обещанный доклад в прошлом году http://synrc.com/news/2016/groupoid.htm

В следующий четверг будет мой доклад про категорную семантику индуктивных типов, по материалам Вармо Вене, Николя Гамбино и Майкла Шульмана. На предыдущем семинаре был мой обзор Pure Type Systems и их конфигураций, по материалам Хенка Барендрехта.


Retracting Thursdays — Сергій Іванович Максименко показує відмінність ректрактів і домінації, голова відділу топології НАН України

АНОНС

Семінар
Похідні категорії та їх застосування
Гомотопічна теорія типів
15.30, Четвер, 06.04.17
Інститут математики
кім. 208 або конференц-зал 305
Максим Сохацький
Категорна семантика індуктивних типів

Бажано знайомство з теорією категорій — категорії, функтори, природні перетворення, монади — наприклад, з http://5ht.co/cat.pdf
і лямбда-численням – наприклад, з http://5ht.co/pts.pdf
Модератор: Володимир Васьльович Любашенко

Слайди з перед-семінарського обговорення:
https://groupoid.space/tex/cub/Cubical%20Type%20Theory.pdf

01 апреля 2017, 03:14

29 марта 2017

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

Групоид Инфинити открывает свой репозиторий Coq пакетов

С коком такая тема, что не все пакеты обновляются часто, никому не нужны FTC, Category Theory, CoInduction свойтва на последних коках. Последний — 8.6 — вышел в декабре 2016, а у всех пакетов в OPAM стоит жестко меньше 8.6. Они там язык тактик поменяли, и улучшлили тайпчек вселенных.

Демонстрировать кому-то всю силу кока приходится на своем компе, и простых инструкций взять и склонировать что-то для известных теорем нет. Более того, не все теоремы есть в OPAM, много просто валяются на ftp серверах унивеситетов.

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

Итак, встречайте, кодовое название проекта "Вери Мас Сач Вау" https://github.com/verimath Логотип тупо ноль — обозначает начальный уровень Кунг-фу в Зависимой теории :-)



Хочу сделать максимальный smooth экспириенс для математиков и академии, чтобы студенты могли очень просто начать разрабатывать на коке. Смешно, но даже матерые коко-писатели из НАН не знают как накатить HoTT патчи и чекнуть гомотопические теоремы.

Хочу, чтобы простая последовательность действий всегда позволяла запустить любой наш репо на последнем коке. У чуваков культуры оформления вообще никакой, какие-то перл скрипты, беш скрипты — представьте, что вы говорите математику на виндовсе поставить перл и беш, чтобы у вас работали теоремы. Вообщем, я это все повыбрасывал и оставил только coq_makefile. В репозиториях ничего кроме коковских файлов нет и все собирается простой последовательностью команд:

$ brew install opam
$ opam install coq
$ git clone http://github.com/verimath/topology && cd topology
$ coq_makefile -f Make -o Makefile
$ make

Начал я с таких тем-репозиториев — все рабочие (только ftc wip):

1. topology — общая топология + лемма Цорна
2. co — первый коиндуктивный репл-шелл на коке
3. real — действительные числа, как коиндуктивные стримы цифр
4. termination — терминальная категорная семантика коиндуктивных стримов
5. set — теория множеств Тарского-Гротендика
6. interpreter — интерпретатор гомотопической теории
7. ftc — основная теорема анализа по предложению риалити хакера
8. lambda — нетипизированное лямбда исчисление как инициальный объект категории экспоненциальных монад

Пакеты можно будет добавлять так:

$ opam repo add coq-released https://groupoid.space/opam

Делаем зависимые лямбда термы ближе к народу!

29 марта 2017, 02:20

nponeccop

Хачим oczor

31 files changed, 356 insertions(+), 462 deletions(-)

29 марта 2017, 00:12

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

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