Russian Lambda Planet

24 мая 2016

Scala@livejournal.com

Частичная явная передача implicit-параметров.

У меня есть функция с двумя implicit-параметрами. А в одном месте понадобилось один из параметров передать явно. Что-то вроде
scala> def f()(implicit a: String, b: Int) = b + a
f: ()(implicit a: String, implicit b: Int)String

scala> implicit val x = "ggg"
x: String = ggg

scala> implicit val y = 17
y: Int = 17

scala> f()
res0: String = 17ggg

scala> f()("ggg",56)
res1: String = 56ggg

scala> f()("gggg",56)
res2: String = 56gggg

scala> f()("gggg")
:14: error: not enough arguments for method f: (implicit a: String, implicit b: Int)String.
Unspecified value parameter b.
       f()("gggg")

Можно ли это как-то по-человечески сделать?
Вариант - засунуть ее в блок и в нем переопределить implicit не очень подходит, поскольку один из ее неимплиситных аргументов тоже блок, а котором эти implicit тоже используются, и мне не надо из переопределять.

написал Mike Potanin (mpotanin@gmail.com) 24 мая 2016, 14:54

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

Об универсальных языках программирования/моделирования 1

Ребята пишут про какой-то паттерн матчинг настоящий :-)
Про итеграцию и то, что это было в лиспах (ну не в лиспах, а в ACL2 — это все же не лисп). Ну и понятное дело все это пишут ебанаты, код которых так воняет по всему интернету что даже из гитхаба его удаляют :-) Невозможно понять как работает паттерн мачинг, если вы не поняли как раотает оператор J. Я написал за свою жизнь около 15 языков. И поверьте любые ваши попытки написать свой язык, в котором нет зависимых типов и бесконечного счетного количества вселенных — навсегда остануться костылями, которые никогда не будут восприниматься более-менее здоровыми психически людьми как нечно стоящее. Потратьте хотябы несколько лет в медитации, чтобы понять что А) мы (Групоид Инфинити) не занимается хуйней и Б) вы занимаетесь хуйней.

Originally posted by justy_tylor at Об универсальных языках программирования/моделирования 1
В начале века я ещё считал, что прогресс технологий работы с информацией сильно сдерживается существующими языками программирования, но достаточно заменить C++ чем-то более развитым по части функциональщины и метапрограммирования (но сохраняющим возможность генерации оптимального нативного кода), чтобы стало легко и удобно разрабатывать продукты любой сложности, уделяя внимание только проблемам предметной области, но не ограничениям предыдущего поколения инструментов. Был юный и тупой.

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

Можно сделать язык с полноценной реализацией pattern matching (а не как принято сейчас). С паттернами и комбинаторами в качестве первоклассных сущностей языка. И это уже польза. Однако.

Для определённых типов данных эффективнее создание индексов вместо полного перебора веток. Появляется выбор, либо через удобный pattern matching, либо через ручное решение с индексами. Ложный выбор. Средства метапрограммирования языка должны позволять создание подобных индексов в pattern matching, сочетая удобство написания и эффективность работы. И это ещё полезнее. Однако.

В реальном мире код работает не только с разными видами процессоров, памяти и периферии. Код работает с другим кодом. И существует множество информационных систем, где, например, выражения из паттернов/комбинаторов для регистрации на какие-то события указываются через XML-конфиг, а потом придумываются дублируемые идентификаторы, связывающие их с неким исполняемым кодом (часто тоже не нативным). И да, люди, создающие системы с ручным редактированием XML, достойны перерождения в виде жаб в Бангалоре. Но это не отменяет необходимости интеграции с такими системами. И здесь даже нет выбора. Только через конфиг. Хотя... Ведь и его можно сгенерировать. Ещё одна возможность трансляции pattern matching: что слева - в конфиг, что справа - в код.

То есть, язык, решающий проблемы разработки, должен решать проблемы интеграции. Поддерживать в процессе компиляции как пользовательские compile-time алгоритмы, так и описания таргетов из пользовательских библиотек. Здесь конфиг, там HTML, а кому-то вообще кусочек COBOL на мейнфрейм сгенерировать надо.

Но зачем тогда вообще писать что-то на COBOL (Java, C++, SQL, XML, bash, make, whatever...), если это можно сгенерировать из единой исполняемой спецификации, гарантируя отсутствие расхождений на стыках языков? Да, всё так, они оказываются лишь артефактами старых систем. Настоящий язык программирования должен быть универсальным, и заменить сразу все неуниверсальные. Что не значит, что он будет единственным (таким). Будут и другие универсальные, возможно (точнее: когда-то) лучше.

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

24 мая 2016, 12:56

22 мая 2016

nponeccop

Мега-СУБД: указатели, плотная упаковка и строки кеша

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

Массив с бинарным поиском - чуть меньший идиотизм, потому что всё равно отравляет кэш. Допустим, у вас 4-байтовые ключи и строка кэша 64 байта. Первое обращение к массиву вытянет 16 ключей (строку кеша, содержащую "серединный" ключ), из которых 15 будут бесполезны и занимать драгоценное место.

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

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

Условно, если есть 100 связных структур по 600 узлов одинакового размера - то можно узлы для всех них аллоцировать в одном массиве из 60к элементов, а вместо указателей использовать двухбайтовые индексы в этом массиве. Можно даже gc организовать локальный.

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

а) длинных указателей мало
б) алиасинг под контролем - на большинство живых узлов ровно один указатель
в) системное ПО - можно один раз потрахаться, а потом 100500 раз хипсторам продать

22 мая 2016, 02:22

Мега-СУБД: интерфейс мапредьюса

Мне тут пришла в голову идея запилить узкоспециализированную СУБД под свои нужды. Это больше похоже на библиотеку ридонли-контейнеров с интерфейсом мапредьюса.

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

GET - это ночное окошко в аптеке. Клиент пришёл, сказал что ему нужно, продавец закрыл окошко и пошёл искать. Если пришло 2 клиента - то продавец не разговаривает со вторым, пока не отпустит первого.

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

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

22 мая 2016, 01:02

20 мая 2016

nponeccop

Чем закончился хайп вокруг UML/Rational Rose?

Я так понимаю, SysML, BPMN и MBSE живее всех живых, но хипсторам неизвестны. Хипсторы предпочитают не заниматься такой ерундой, как проектирование и документирование дизайна, и используют вариации того, что древние именовали XP.

Что там вообще на ниве CMM происходит, что сейчас рекомендуется для достижения высокой мачурити? Куда читать, чем облачка с квадратиками соединять, какой бюрократией ни в чём не повинных девов облагать?

20 мая 2016, 19:15

Языки в тренде, согласно tiobe.com

Java, PHP, Ruby, Perl, Delphi/Object Pascal, Assembly language, Swift, Groovy, D

Это языки, чья доля заметно выросла с прошлого года. В принципе, начиная с 4-й позиции фейспалм можно не отпускать, и лишь чуть-чуть приопустить на D.

Уменьшилась доля у:

C, C++, C#, Javascript, VB.Net, Objective-C, R

Тут всё соответствует внутренним предрассудкам, кроме, может, проседаний шарпа.

Рейтинг (известных мне) около-ФЯ:

R, Matlab, Scheme, Lisp, Scala, Prolog, F#, Haskell, Erlang, Q

Ну тут тоже без сюрпризов:
- R, Matlab - для прикладных математиков
- Scheme, Lisp, Prolog - лигаси
- Scala, F# - выезжают на поддержке вендоров, инструментальной поддержке и интеграции с успешным рантаймом
- Haskell, Erlang, Q - наши друзья замыкают процессию

20 мая 2016, 16:23

Dee Mon journal

Покровы сорваны!

Группа ученых под руководством Дэниела Лебреро из Лаборатории Торговых Программных Интерфейсов британской компании IG Markets Ltd провела статистическое исследование о связи числа баг-репортов и языков программирования на базе информации об открытых проектах на сайте "Центр деятельности мерзавцев" (GitHub.com, организация разрешена в России, за исключением некоторых периодов, когда она запрещена). Выяснилось, что наличие статической типизации и продвинутой системы типов не помогает в уменьшении ошибок, а порой даже вредит, в то время как меньше всего ошибок получается в программах на максимально простых языках.

Плотность багов у проектов с 10 звездами и более:


Теперь научно доказано, что theiced был прав: типы не нужны, а писать надо на Кложури. А также Эрланге и Го. Адептам сложных языков и развитых систем типов надлежит раскаяться, одуматься и перестать уже своими надуманными неработающими идеями отвлекать благородных донов, занятых TDD.

20 мая 2016, 08:31

18 мая 2016

nponeccop

Ничего не напоминает?

New features proposed include concurrency and atomics, zero-copy binary data transfer, more number and math enhancements, syntactic integration with promises, observable streams, SIMD types, better metaprogramming with classes, class and instance properties, operator overloading, value types (first-class primitive-like objects), records and tuples, and traits

18 мая 2016, 06:16

17 мая 2016

rssh

Видео со #scalaua

Появились первые записи докладов. Плейлист - https://www.youtube.com/playlist?list=PL-RBtv_a80i6xwA_yGGXzEjScSYuuT-YF .

Вот индекс первого блока:


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

17 мая 2016, 05:55

15 мая 2016

ru_declarative

Вопрос про Agda:

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

PS: И тот же вопрос про Idris, хотя тут менее интересно.

написал kouzdra 15 мая 2016, 03:41

14 мая 2016

nponeccop

ES6 style guide

https://github.com/airbnb/javascript

Впервые вижу руководство по стилю, призывающее использовать фичи. Чаще запрещают.

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

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

14 мая 2016, 06:34

Автоподбор параметров

Пилим тут https://github.com/streamcode9/node-discrete-spsa

An implementation of the Discrete Simultaneous Perturbation Stochastic Aproximation algorithm.

See Stacy D. Hill, "Discrete Stochastic Approximation with Application to Resource Allocation", 2005 http://www.jhuapl.edu/SPSA/PDF-SPSA/Hill_TechDig05.pdf

Cам алгоритм на 5-й странице step1-5, прост как палка.

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

Это всё равно бесконечная игра с подбором learning rate, но наверное получше будет, чем наивный подход "просемплировать всё пространство состояний с заданным шагом, используя статистически значимые бенчмарки".

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

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

14 мая 2016, 05:17

12 мая 2016

nponeccop

Языки под задачи и хаскельный элитизм

Если кратко - то языки выбирают не тогда, когда задача уже есть. Их выбирают загодя и обкатывают. Когда задача вот она стоит перед предприятием - только то, что обкатано.

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

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

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

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

В моём случае С++ я знал "со школы", а "заделами" являлось изучение Perl (это был 1998 год, PHP был относительно маргинальным, а Perl - проверенным решением) и Haskell.

Пилотным для Perl был проект сайта брачного агентства, который сделал одногруппник, а я мейнтейнил (т.е. заметьте, безрисково!). JS учил в проекте с одногруппником, который более-менее его знал. А Haskell я учил по сути все 15 лет последние, с пилотной обкаткой на опенсорсных хобби HNC и N2O.hs и небольших утилитках в продакшене.

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

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

Т.е. я намеренно, в течение 15 лет сменял специализацию. "Элитизм" тут проистекает из зарплат порядка 100 дол в час, достижимых на ниве хаскель кодерства.

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

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

Короче, "языки под задачи" - это для
а) джуниоров, берущихся за что попало;
б) начинающих контор, берущихся за что попало;
в) при поиске субподрядчика.

12 мая 2016, 16:02

11 мая 2016

nponeccop

Протокол однопоточного воркера

Художественная резьба по диаграммам дала частичный ответ на вопрос об оптимальности однопоточного протокола. Оказывается, если нет ненужных блокировок, разные реализации отличаются всего лишь последовательностью пакетов в половине TCP-соединения, направленной от воркера к гирману (обозначенной как send).

Send и Recv - половины TCP-соединения.
Source и Sink - половины гирмана. Сорс раздает работы, синк принимает результаты.
Grabber и CPU - половины воркера.

исходник

11 мая 2016, 22:28

10 мая 2016

nponeccop

Усиленная версия протокола

В общем случае воркер однопоточный и подключен по WAN, т.е. надо раздавать более 1-й работы (active) и заполнять "трубу" bandwidth x latency (queued). start() точка старта, говорим какие типы работ принимаем. grab - "подпрограмма", используемая в 2-х местах: по выходу из сна и по окончанию работы. run - по окончанию работы и по приходу новой
invariant active + grabbing + queued <= max_active + max_queued
invariant active < max_active && queued == 0
invariant active >= 0 && active <= max_active
invariant queued >=0 && queued <= max_queued
invariant grabbing >=0

max_active = ...
max_queued = ...
grabbing = 0
active = 0
queued = 0

run():
	dequeueJob()
	active++
	queued--
grab():
	<- GRAB_JOB
	grabbing++
start():
	<- CAN_DO test_tube
	<- PRE_SLEEP
-> NO_JOB:
	grabbing--
	if grabbing == 0
		<- PRE_SLEEP
-> NOOP:
	assert grabbing == 0
	while (active + grabbing + queued < max_active + max_queued)
		grab()
-> JOB_ASSIGN:
	grabbing--
	queueJob()
	queued++
	if active < max_active
		run()
-> workComplete:
	active--
	if (queued > 0)
		run()
		assert active == max_active
	grab()
	<- WORK_COMPLETE
-> workData:
	<- WORK_DATA
Основной вопрос - как убедиться, что спецификация корректна? И это всё ешё упрощённый протокол. Так как если в сети congestion - то надо говорить воркерам "горшочек, не вари". В апстриме этого не делается и получается жопа.

10 мая 2016, 20:34

Протокол Gearman

Gearman.org - это такой task queue server, один из вариантов request-response. Идея в том что есть "клиенты", раздающие работу, и "воркеры", выполняющие работу. Клиенты отправляют реквесты, получают респонсы. Воркеры - наоборот. Сервер форвардит.

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

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

<- GRAB_JOB
-> JOB_ASSIGN
<- WORK_COMPLETE
-> NO_JOB

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

GRAB_JOB (JOB_ASSIGN WORK_COMPLETE GRAB_JOB | NO_JOB GRAB_JOB) *

Однако, его можно "улучшить":

GRAB_JOB (JOB_ASSIGN GRAB_JOB WORK_COMPLETE | NO_JOB GRAB_JOB) *

Непонятно, как вообще формализовывать понятие "хорошести".

10 мая 2016, 17:40

Task queue курильщика

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

Сейчас я нашёл подходящий для этого строительный блок.

С его помощью задача 10к раз применить toUppercase() к строке "abc" занимает 700 секунд! Т.е. 70мс на каждый вызов.

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

Эти "abc" ставятся в task queue, и задействованы 3 процесса, соединенные через локалхост: клиент, сервер очереди сообщений типа request/response, и воркер.

Я так понимаю, внутри очереди есть какие-то квадратичные алгоритмы, не рассчитанные на 10к сообщений в очереди, причём, скорее всего во всех 3-х компонентах. Достоверно известно, что там точно всё написано по принципу наивного неконкурентного программирования - т.е. двойных буферизаций, учета bandwidth*latency и прочих трюков нет.

Интересно, где зарыта собака окажется.

Upd: сделал бенчмарк, с квартилями, нормализацией, усатыми графиками и шлюхами. Выяснилось, что исправление, которое умозрительно не может замедлять код, его таки замедляет, причём аж на 8%. Но замедляет только говнореализацию сервера на локалхосте. Нормальную реализацию которая на С++ - не замедляет, как и подсказывает нам голова. А сишную нормальную реализацию по WAN даже ускоряет, собственно ради WAN всё затевалось. Говнореализацию по WAN не тестил, но там думаю ускорение в 270% победит замедление в 8%.

10 мая 2016, 06:52

08 мая 2016

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

Немного Мадхьямики в MLTT сеттинге



В тибетской традиции есть такое понятие — Дхармадхату — пространтсво всех Дхарм. Это пространство всех мыслей которые существуют вне контекстов. Представить сложно — понятное дело. Но у нас есть MLTT теория которая поможет это представить.

Представьте себе пространство всех языков программирования — понятно дело все знают про лямбда исчисление. Но не многие же рубисты или ПХП программисты задумываются, что они пишут на языке пространства — которое с точностью до битов моделируется теорией типов Мартина Лефа (надо только вселенные правильно отконфигурировать, это научились делать в 2001 году, когда Coq все дружно писали). Конечно я сам в это по началу не верил, и думал что есть все-таки ограничения и что Данила Мастер, который вручную все сам делает вместо того чтобы экстрактить это из Инфинити Топоса делает ненапрасный труд. Мне пришлось написать прувер чтобы понять — таки да, каждый Данила Мастер, который считает себя инженером — производит временный и бесполезный труд, давая ярлыки феноменам не видя их сути.

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

У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.

Не многие знают, что имя линии передачи, которую мы официально представляем в Киеве, называется Лонгчен Ньингтик. KLONG по тибетски — это пространство, пространство всех феноменов, KLONG CHEN NYING THIG обширное пространство сердечной сущности. Так же как Инфинити Топос — это пространство всех MLTT типов, которое объединяет континуум и дискретное, а также проглатывает всю математику со всеми ее логиками и теориями, так как все математики разговаривают уже давно на этом языке кванторов и бесконеченых вселенных.

Так вот, точно также как все языки рождены из этого пространства, так же и мысли все рождаются из одного пространства, и все они проименованы, точно также, как проименованы все типы во всех вселенных. Рождаются тут условно, так как List не рождается, его можно обнаружить понять, но он всегда присуствует в Топосе во всех уровнях вселенных. Все типы являются несозданными, пока их не объявит программист в виде аксиом MLTT. Но если их рассматривать через призму нечистого видения — нетипизированного лямбда исчисления, то рассмотреть их не получится или очень сложно (Алонсо Черч и Боем с Берардуччи не смогли этого сделать). Ну а аналогия просветления — это выход в эту мандалу, где видны все типы сразу, или куда не кинешь взор, видишь везде похожие паттерны. Послушай функциональный программистов — натуральные же шизофреники, видят какие-то катаморфизмы там, где обычный человек видит while или for; видят группы, там где обычный человек видит record; чему обычные инженеры дали уже тысячу ярлыков. Знаете есть такое в духовных практиках быть остраненным и не вешать ярлыки на феномены, потому что это бессмылсенно. Это тоже самое что List/Cons и Stream/Mk — миллионы програмистов дали разныне названия этим штукам, но штуки эти существуют сами по себе и увидеть их можно при индуктивном рассмотрениии заполнения пространства типами начиная с Unit, и сделать это можно начиная уже с третьего шага.

Вообщем аналогии настолько прочные, что я могу в священных тибетских текстах заменять Дхармадхату на "Инфинити Топос", SEMS или Ум на "правила вывода" (кстати один из переводов SEMS — это вычислитель) или на "компютешинал аксиомы", CHOS или DHARMA (Феномен) на Тип и ничего почти не изменится. Процесс мышления — это то как вы конструируете теоремы, как вы выстраиваете рекурсивные цепочки, т.е. как вы композируете мысли (рекурсия и индукция). Если у типа нет рекурсора, значит вы не можете пустить мысль по этому феномену. А пустить мысль по феномену означет его осознание т.е. освобождение в дхармакае, что впринципе соотвествует этимологии слова элиминатор.

Пора положить конец спорам различных школ Мадхьямики (модели сватантрик) и описать все эти логики в виде MLTT программ.

08 мая 2016, 02:03

07 мая 2016

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

Erlang Killer Apps

В Эрланг среде принятно считать, что RabbitMQ и Riak, или по крайней мере riak_core — являются киллер приложениями Erlang. Я сам помню на начале своей карьеры тоже поставил на эти продукты и еще на Nitrogen. С нитрогеном я разобрался быстро (он уже история — все используют N2O уже давно). Настала очередь Riak или RabbitMQ, не знал за что взяться. Взялся сразу за распределенную базу, но так быстро на распределенные алгоритмы не наскочишь, а тестами покрывать распределенные системы — это не в этой жизни, может в следующей, если плохо себя вести буду. Вообщем исследование Chain Replication завело меня в тупик зависимых типов и я начал пить™.

Расскажу какие мысли у меня были во-первых по Riak. Riak после всего что я видел до него поверг меня в шок стоимостью обслуживания продакшина. Я с легкостью строил кластера пока не понял что они мне совершенно не нужны. Из riak нужно реально только riak_kv, riak_core и riak_pipe. Причем я даже собирал Riak без bitcask полностью (он вшитый в ядро) и многие другие штуки делал типа порт Riak под Windows 8. Собственно KVS появился как штука чтобы не ебаться с голым riak. В Riak вы храните бинари, а в KVS типы-рекорды описаные в схемах. Это потом в KVS появились бекенды.

Паралельно у меня был кластер из трех RabbitMQ. Тогда уже я понял что производительность RabbitMQ высокая только если они работают в шардах (не кластер, потому что интерконнет хуйовый у эрланга). Т.е. реально RabbitMQ используют все просто как ETS с красивым дашбордом для админов. Забейте хуй на RabbitMQ, эта штука покрыта кольцами как и Riak. Счас есть гораздо емкостные MQ типа emqtt.io (gproc в качестве деливери, mnesia — для дюрабилити), тоже причем с красивыми дашбордами. У меня кстати есть заказ от Остинелли на порт emqtt.io с gproc на syn.

Но я не об этом.

Спросите себя почему MQ и KV сервера в вашем окружении (а они у вас все равно есть, какое бы вы приложение не писали) находятся в разных приложениях. Ведь в вашем приложении MQ обслуживает клиентов, и KV обслуживает клиентов. Поэтому тут работатет data locality, а значит можно посадить это на одни и теже воркеры vnode. Но почему у всех ПОГОЛОВНО MQ и KV сервера — это разные продукты? Почему так? Ответа не нашел. Продуктов нет (разве что redis). Поэтому я подумал написать (еще два года назад) MQ + KV сервер работающий на одном ядре. И ядро это KVS.

KVS отвечает за durability, MQ должен хранить сабскрипшин меш своих подписок а также все сообщения (если очередь скажем персистента или нужны ACK или нужна транзакционность). Вполне очевидно что это можно хранить в том же KVS. Уверен что все люди которые используют RabbitMQ (илии другие MQ продукты) дублируют и синхронизируют свой сабскрипшин меш приложения и состояние подписок в mnesia таблицах RabbitMQ. Нахуя? Незнаю, в моем MQ такого дублирования не будет.

Какие я могу обеспечить показатели MQ сервера на KVS:

1) ну я могу выжать из мнезии 40K RPS на данных которые помещаются в RAM, и 20K RPS на данных которые не ограничиваются ничем. async_dirty естественно.

2) Data Locality. И серверы очередей и серверы данных будут обслуживать на одних и тех же vnode (по 64 или 128 на ноду), т.е. вычислятся хешом по идентификатору пользователя, а значит исчезает необходимость в синхронизации, так как все сообщения от MQ и KV протокола будут помещены в одну и туже очередь пользователя (линеаризация во имя консистентности).

3) Благодаря KVS, и MQ сервер и KV сервер будут поддерживать все бекенды которые поддерживает KVS: mongoDB, SQL, Riak, mnesia, redis.

4) доступ к очередям можно получать напрямую читая их из базы, если нужно. Еще был план написать универсальный REST эндпойнт к KVS как в Riak и CouchDB, и чтобы этот же эндпойнт был API для MQ сервера.

Ну и этот конструктор не имеет ограничений. На KVS можно лепить уже более сложные API и системы. Пример CR хоть и заезженный, но рабочий.

Вообщем надо соединять MQ и KV сервера, мое мнение, а вы делайте как хотите :-)

07 мая 2016, 03:36

nponeccop

Poor man's IOmeter

Вот ещё задача. Есть файл более 4 гб и во много раз превышающий ОЗУ, состоящий из блоков фиксированного размера. Надо написать прогу, читающую из него в течение X минут блоки размера Y со случайным номером c конкурентностью Z.

Должно работать на линуксе i686 и винде x64 и поддерживать блоки размером от 64кб до 16 МБ (c большими блоками может быть минижопа). В виде бонуса - обеспечить чтобы прочитанные страницы не отравляли системный дисковый кэш.

Опять же - как бы делали и какие трудозатраты?

07 мая 2016, 00:00

06 мая 2016

nponeccop

Poor man's ZMQ_PAIR

http://api.zeromq.org/4-0:zmq-socket

В ZeroMQ есть тип соединения ZMQ_PAIR. Идея в следующем: пользователь библиотеки видит постоянно открытое виртуальное соединение между узлами. В него можно слать байтики и принимать байтики. Ошибок пользователь не видит никаких.

Внутри это виртуальное соединение реализовано с помощью TCP. Клиент бесконечно пытается переподключиться. Сервер знает, что клиент у него всего один, и при подключении нового TCP-соединения отрубает старое. Если отправлены данные с серверной стороны на клиентскую, а никого не подключено, сервер бесконечно ждёт.

Как бы вы такое делали, на чём, и какие примерно трудозатраты чисто на сервер, придуряющийся единственным вечносоединённым двунаправленным сокетом?

Допустим, что секьюрити, message semantics/framing layer, application level keepalive и слежение за отсутствием дыр и дубликатов в данных не нужны.

06 мая 2016, 23:47

05 мая 2016

nponeccop

Как научиться хачить Om/Exe/HNC

Центральной идеей Om является теорема о том, что используемых в нём 4-х конструкций (звездочки, лямбды, квантора и вызова функции) достаточно для записи спецификаций программ. Например, из этих 4-х конструкций можно слепить как из атомов массивы и записать утверждение о том, что некая функция на вход принимает массив и функцию сравнения, а на выходе возвращает его же, но упорядоченный. Собственно, сомнения были в том, что можно описать понятия "он же" и "упорядоченный".

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

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

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

Далее надо научиться писать на хаскеле. Там и алгебра, и геометрия, и группы на каждом шагу.

Пресловутые монады - это вариации на тему групп. А также моноиды и решётки. В HNC оптимизатор использует т.н. верхние полурешётки. Для эффективной работы на хаскеле нужна некоторая практика, чтобы видеть за кодом абстрактные интерфейсы, вроде того как за трансформером стрима в node.js видеть Duplex, а за ним Writable. Только интерфейсы там очень обобщённые, типа тех, что в теории групп.

После хаскеля можно начинать читать книжки по системам типов и системам перезаписи, например TAPL Пирса и Functional programming and parallel graph rewriting

После книжек можно пробовать языки с зависимыми типами - я бы рекомендовал Idris, Lean, Agda. Ну и более продвинутые книжки, вроде Programming in Dependent Type Theory

Ну это довольно полная программа по Type Theory

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

Я столько математики не знаю, и вот пока не придумал, как мне теорию категорий освоить. Но это как бы высший пилотаж. То, что делает zeit_raffer, со своим изобретённым способом выражать спецификациии - это передний край мировой математики. Аналог Маска с его посадкой ракеты на струю. Принципиально ничего нового Маск не сделал, но никто этого не делал раньше в таких масштабах. Так же и у нас, что в Om, что в HNC.

Но глубокое понимание требуется, только чтобы дизайнить Om или HNC. Для того, чтобы писать код, требуется только общее понимание технологий компиляторостроения. И то, это только в случае HNC, который достаточно высокотехнологичен. Ом же на коленках слеплен, там код простой как пробка.

В HNC я использую parser combinators, attribute grammars и уже упоминавшийся lattice dataflow analysis. Ну, и уже упоминавшиеся "абстрактные интерфейсы", вроде использования F-алгебры в качестве итератора по дереву. Оно всё реально код сокращает.

05 мая 2016, 18:20

Языки в проде

У меня 4 рабочих языка: С++, Perl, Javascript, Haskell. Для нового кода выбор невелик: либо Typescript, либо Haskell. В продакшене крутятся все 4.

nodejs достаточно качественно сделан. У того же хаскеля под Windows рантайм-библиотека (реализация ввода-вывода из зелёных потоков) весьма плохонькая, написанная людьми, незнакомыми с системным API.

Учитывая что JS я знал раньше, а нормальные зеленые потоки под Windows мне неизвестны, альтернатива писать event driven на ноде выглядит очень даже.

После хаскеля учить и использовать какой-нибудь C#, F# или Go желания никакого нет. Не говоря уже о незрелых маргинальных поделках, вроде ATS и Idris, у которых на винде совсем-совсем плохо. А в GHC можно будет патч отправить, там вроде почти всё на мази, даже зачатки IO Completion Ports вроде как есть (это высокопроизводительный API для ввода-вывода, аналог epoll)

05 мая 2016, 18:14

Dee Mon journal

все-таки можно!

Говорили, на ноль нельзя делить, а вот британские учоные научились! Берешь хаскель и делишь себе, получаешь конкретные числа:
Prelude> floor (1/0)
179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216


Для 1, -1 и 0 ответы разные выходят.

05 мая 2016, 02:48

04 мая 2016

"Записки программиста"

Сборка проектов на Haskell при помощи Stack

Прошло некоторое время с тех пор, как я последний раз писал в этом блоге что-то про Haskell. И вот, мне стало интересно, что успело измениться в мире этого языка. Изменилось, насколько я понимаю, не так уж и много, но вот вместо Cabal для сборки своих проектов теперь все используют какой-то Stack. Давайте же попробуем разобраться, [...]

написал Eax 04 мая 2016, 07:00

03 мая 2016

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

Орнаменты

На меня снизошел очередной микро-инсайт-просветление и я сразу же спешу с вами ним поделиться. Абсоюлтно очевидная и прекрасная вещь. Признаюсь честно, что я в глаза формулировок не видел, но вот система сразу нарисовалась перед глазами. Кто читал МакБрайда поправит меня, я уверен.

Как вы знаете, все конструкторы (ко)-индуктивных типов могут состоять из параметров и типа результата конструктора. Последний может и не находиться во вселенной этого типа, а быть типом Path. Так вот параметры этого типа могут быть всего трех видов:

1) Unit, как в типе Lazy A: () -> A или ленивом Nil: () -> List A.
2) Fixed Type как в типе первого параметра коснтруктора Cons: A -> List A -> List A.
3) Recursive Type, как в типе второго параметра tail конструктора Cons, или второго поля tail рекорда коиндуктивного Stream (они равны в MLTT).

Это называется три орнамента. Они все задаются разными профункторами P_{1,2,3}, которые описаны у Паши в блоге. Из этих орнаментов мы конструируем тела термов в наших кодировках (всех их модификациях). Круто да? Это еще не все, суть орнаментов не в этом, а в том что вы можете транзакционно добавлять новые параметры в существующие конструкторы. В современных пруверах и в ООП в операции extend применимое к структурам или рекордам действует на уровне добавления новых конструкторов только, а не модификации (версионировании) существующих. Орнаменты же позволяют делать версионирование типовых интерфейсов и структур, и позволяют избежать случает когда приходится называть линковочные интерфейсы DirectDraw2. С помощью орнаментов вы можете добавлять аргументы в существующие конструкторы или менят их тип. Я привел только три орнамента, которых достаточно чтобы покрыть все существующие базовые библиотеки всех языков программирования :-) А представьте что орнаментов может быть больше!

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

Как вам такой "внутренний лисп" пространства типов?

_______________
[1]. https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf

03 мая 2016, 20:53

Лев тоже вкурсе про то, что ядро должно быть компактным

Лев называет это принципом де Брейна, хотя я такое не встречал в литературе, если кто видел где, покажите, я буду цитировать. Того самого де Брейна, учителя Барендрехта, который первый в мире автоматический прувер сделал AUTOMATH 1967 — голандская школа логиков (они еще записывали самые известные 100 теорем математики для всех систем на то время — http://www.cs.ru.nl/~freek/100 ); HOL/LCF 1972 это второй большой проект — британская школа, который дал миру ML и Хаскель тоже по сути британская школа, как и Агда и Идрис; и первый из современных пруверов Coq (инфинити предикативные вселенные и одна импредикативная внизу aka pCIC) — французкая школа.

https://youtu.be/c_S_bAdv4A0?t=719

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

03 мая 2016, 11:04

nponeccop

Левая развёртка косписков, anyone?

Код ниже на современном (с arrow functions - это ES5?) джаваскрипте. У натуральных чисел и списков есть, кроме обычного катаморфизма, такая же "штука с алгеброй", но "хитрая", соответствующая левой свёртке:
natCata = (algebra, i) => {

        if (i == 0)
	{
		return algebra(null)
	}
	else
	{
		return algebra(natCata(algebra, i - 1))
	}
}

natCata2 = (algebra, i) => {

	var ret = algebra(null) 
	while (i-- > 0)
	{
		ret = algebra(ret)
	}
	return ret
}
Вот у меня 3 вопроса в связи с этим:
1. Какие ещё структуры обладают этим "левым катаморфизмом"? Должны быть линейными, а ля

data O a = O a (E a) | ONil
data E a = E a (O a) | ENil

и неизоморфными хитрым спискам. Например O a неизоморфен списку из data RR a = OO a | EE a

2. Выразимы ли эти "периодические верёвки" как фиксированные точки функторов? Как вообще выглядит всё это разнообразие верёвок, т.е. какие варианты возможны? вот один, выразимый фиксированной точкой: data XList a b = XCons a (Xlist a b) | XNil b

3. Есть ли дуально "хитрые штуки с коалгеброй", у каких структур данных, и чему они соответствуют.

03 мая 2016, 05:32

02 мая 2016

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

OM/EXE Подкаст. Выпуск #1

В будущем самый крутой подкаст про лямбду от Groupoid Infinity:
OM/EXE Подкаст. Выпуск #1:



https://soundcloud.com/maxim-sokhatsky/omexe-podcast

02 мая 2016, 22:33

Андрей Байер тоже за минимальные ядра

Вот тут Андрей Байер (может быть известный программистам по Programming Languages Zoo — сборнике имплементаций ML вариаций), в лекции посвященной элиминатору индукции и равенству выраженному в чистой лямбде, в секции ответов на вопросы, говорит, что критически важно иметь простое ядро прувера:

https://youtu.be/IlfQjWqrK6I?t=3690

02 мая 2016, 07:37

01 мая 2016

nponeccop

Новости HNC

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

1. Что такое HNC

HNC - это аналог PureScript для С++, оптимизирующий компилятор из промежуточного языка HN в человекочитаемый С++. На HN можно будет писать вручную, или использовать в качестве бэкенда для более высокоуровневого языка вроде Om.

Ключевые фичи:
1. Человекочитаемость и относительная идиоматичность выходного кода. Сравните выходной Javascript у PureScript и у тех же Elm/Fay/GHCJS.
2. Первоклассный интероп с С++, включая отсутствие чужеродных схем управления памятью (GC, особый аллокатор, подсчёт ссылок и пр)
3. Наличие серьёзного оптимизатора
4. Hackable кодобаза малого размера (до 6к строк).

Основная исследовательская задача - можно ли написать такой оптимизатор из ФЯ, выходной код С++ которого бы проходил ревью человеком, и если нет - насколько можно приблизиться.

С++ выбран как наиболее трудный таргет. Имея рабочую версию для С++, перенацелиться на какой-нибудь Javascript будет просто.

2. Зачем HNC

Борьба с лигаси-кодом на С++. Дописывание компонентов в системы на С++. Быстрое прототипирование для С++. В перспективе расширение идеи на другие языки.

3. Что позволит делать

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

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

4. На чём написано

- Хаскель
- атрибутные грамматики UUAG (с атрибутами на хаскеле)
- библиотека HOOPL для написания оптимизаторов
- библиотеки парсинга и структурной унификации (последяя нужна в выводе типов)

5. В каком окружении работает

Компилятор работает везде, где есть GHC 7.10 (Win,Lin,Mac). Программы работают везде, где есть приличный компилятор С++ (MSVC считается приличным). Собственного рантайма и стандартной библиотеки нет. Прикручиваете по FFI нужные типы и функции и вперёд.

6. Писать работающие программы на нем будет можно? Опердени, высоконагруженные сайты с котиками, видеостримминговые серверы, что-нибуть еще?

В первом приближении - можно использовать в проектах, где в коде есть высокоуровневая часть, которую можно было бы написать на Lua, но нельзя, потому что он тормозит (или Lua не нравится, или религия не позволяет - у С++-ников найдется миллион причин разной степени объективности)

7. Какие платформы поддерживает (сможет поддерживать)?

Сможет практически всё. JavaScript, C#/Java, хоть Perl.

8. Какой интероп? Поддержка нативных типов платформы будет?

Пока можно вызывать функции в обе стороны (С++ <-> HN). Типы только нативные для платформы (в HN можно только функции писать - нельзя объявлять типы. Оверхед интеропа сводится к необходимости заворачивать методы в функции, но это ограничение текущей реализации, а не принципиальное.

Ccылки по теме:

https://github.com/nponeccop/HNC/wiki
https://github.com/nponeccop/HNC/wiki/PaperDraft
https://code.google.com/archive/p/inv/
https://code.google.com/archive/p/inv/wikis/Manifesto.wiki

01 мая 2016, 00:40

30 апреля 2016

Фонд Поддержки Функционального Программирования

Отчёт о мартовском конкурсе по ФП

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

Конкурс по ФП в марте 2016 года: взлом пропорционального шифра

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

написал Dark Magus (noreply@blogger.com) 30 апреля 2016, 18:12

darkus

Отчёт о мартовском конкурсе по ФП

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


Конкурс по ФП в марте 2016 года: взлом пропорционального шифра


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

30 апреля 2016, 16:11

29 апреля 2016

David Sorokins WebLog

Айвика для кластера и суперкомпьютера

В прошлую субботу выпустил первую версию [5] своей Айвики, которая позволяет создавать и обсчитывать параллельные распределенные дискретно-событийные модели на кластере и/или суперкомпьютере.

В общем, идея такая. 

У меня есть основная версия [2] обще-целевой библиотеки, о которой я много писал у себя в блоге. Она построена на основе стандартного вычисления IO. Самая быстрая версия. Можно автоматизировать вывод графиков и таблиц. Есть документация [1] в формате PDF. Много примеров.

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

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

Так родилась версия [4] для вложенных имитаций. Это когда из «настоящего» мы можем относительно дешево и быстро заглядывать в «будущее» модели столько раз, сколько необходимо, а потом на основе полученной информации принимать решения уже в «настоящем». Конек в относительной дешевизне создания вложенных имитаций и в том, что это по-прежнему обще-целевая библиотека имитационного моделирования.

Теперь же воплотил в жизнь еще и версию [5] для параллельного распределенного имитационного моделирования. Тоже обще-целевая библиотека моделирования. Здесь независимые узлы могут обмениваться друг с другом асинхронными сообщениями, привязанными к временным меткам. Если на узле уже «будущее», а приходит сообщение в «прошлое», то происходит прозрачный откат до «прошлого» модели. Все сообщения, которые были посланы узлом и стали устаревшими, отменяются, и, соответственно, рассылаются так называемые «анти-сообщения». Короче, реализована оптимистичная стратегия с прозрачными, возможно, каскадными откатами на основе идей метода «деформации времени» (англ. «time warp»), датируемого началом 80-х.

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



написал dsorokin (noreply@blogger.com) 29 апреля 2016, 10:41

27 апреля 2016

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

Вопросы на Подкаст

Друзья, перед Первым Категорным Митапом (где Groupoid Infinity будет презентовать свой тайпчекер языка с зависимыми типами и базовой рантайм библиотекой, где все это компилируется в Эрланг) мы решили сделать разогревочный подкаст.

В подкасте планируются такие учасники:
0. Влад Кириллов (@darkproger) — Lagrange Inversion, модератор
1. zeit_raffer — Groupoid Infinity
2. maxim — Groupoid Infinity
3. nponeccop — HNC

1. Знакомство. Все обсуждают текущие свои проекты. Чем они занимались до этого. Я рассказываю про приватбанк, распределенные алгоритмы и их доказательства. Как я через CR пришел к EXE и нашел Пашу. Паша рассказывает про себя. Влад про себя, Процессор про себя.

2. Немного ввод в теорию. Тут каждый рассказывает свое понимание проблемы должно быть нематематично, а эмоционально — интроспекция духовных лямбда поисков. Но может и математично, например про парадоксы, как появились вселенные, про универсумы Гротендика, про HoTT и HIT.

3. Дальше мы обсуждаем архитектуру OM/EXE. Тут все рассказывают со своей стороны, Андрей рассказывает про HNC, мы рассказываем про кодировки, рассказываем про HIT, HoTT и обсуждаем тему божественности MLTT. Готовим людей к тому чтобы слушать доклад про кодировки.

4. Обсуждаем приложения OM/EXE: распределенные алгоритмы, как кафедральный прувер для лабораторных работ. Не забываем что основной задачей подкаста найти людей которые хотят хачить OM/EXE.

Если кто хочет перевести эту беседу или добавить ручайков в русло — пишите, или учавствуйте в подкасте. Или просто оставляйте вопросы к посту, на которые хотите услышать ответ.

27 апреля 2016, 13:01

rssh

Лог выступлений

Я редко используя Jav-у, но когда использую - получается как-то так: https://www.youtube.com/watch?v=f0IR5j53WEg
Это было в марте на cut&code в Хмельницком. Там хорошо - небольшой город, все community друг-друга знают, в таких тусовках как-то исчезает расстояние между людьми. душевно пообщались. Еще там очень классная коллекция скульптур Миколи Мазура из металлолома: http://ua-travels.in.ua/2014/11/22/xmelnickij-metalevi-monstri-mazura/

Несколько простых скала-трюков с типами, доступных для простых смертных: https://www.youtube.com/watch?v=uwRf_avkFns&list=PLvk98GxP10UkzxsmSch46fzcQKAn8dnk3&index=3
(Это со Java/Scala Labs в Одессе 16-го апреля. Вот, кстати - все: https://www.youtube.com/playlist?list=PLvk98GxP10UkzxsmSch46fzcQKAn8dnk3 ) Жалею что пришлось сразу уехать (какое-то убыстрение времени). Приеду в Одессу подробнее в июне на AI & BigData Labs http://geekslab.co/events/61-konferentsiya-aibig-data-lab - попытаюсь хотя-бы вечер не спешить ...

Видео со #scalaua -- скоро будет ...


27 апреля 2016, 04:03

26 апреля 2016

Dee Mon journal

FP design patterns

Неплохое и не без юмора совсем вводное введение в ФП для ОО программистов, верующих в дизайн паттерны:

26 апреля 2016, 13:28

25 апреля 2016

swizard

Геймификация скучных процессов

13 апреля я опубликовал пост с текстом интересной, как мне тогда казалось, вакансии, и он провисел неделю. Много ли за эту неделю заинтересовалось ей людей? Нуль!
19 апреля я предложил развлекательную тестовую задачку для потенциальных кандидатов и им сочувствующих, и внезапно за одну такую же неделю мне наприсылали какие-то полчища резюме, что я даже немного впал в ступор :) Честно говоря, начал даже понимать профессиональных эйчаров, это не такая уж и простая работа, оказывается.

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

25 апреля 2016, 20:18

22 апреля 2016

"Turtle//BAZON Group"

Тяжести разработки под Android и HTML5

Наконец-то опубликовали нашу простенькую игру Пузыри в гугл плей - (официальный пресс-релиз). Немножко под катом - игра основана на технологии HTML5, а в Javascript компилируется Clojurescript. Причём, использование ClojureScript открывает широкие возможности по написанию кода и отлаживанию его. Кстати, всё это работает и в браузере. В целом, в Android используется тот же браузер, но есть нюансы. Первый - этот браузер (системный WebView) везде разный и на что-то положиться особо нельзя. Да и более или менее приличный идёт только начиная с Android 5.0. Чтобы выйти из этой ситуации, в приложении тащим Chromium, который весит уже поболее. Хотя, в наше время это не так критично, но всё же. С другой стороны, я посмотрел, все так делают. Да и к этому нужно было прийти. Есть проекты типа cordova, которые бы позволили опубликовать это легко и удобно, но и там свои нюансы. Например с фуллскрином и сплешскрином. Из нормальных - coconjs, но он весь такой из себя облачный, что вносит свои неудобства. Ну и главный препон - это технологическое развитие. Я имею в виду всякие WebGL, с которыми всё быстре и которое нормально будет работоать с 5.0 Android. Хотя, терпимо работает и на 4.4. В общем, опубликовали, в итоге. :)


написал turtle (noreply@blogger.com) 22 апреля 2016, 01:14

21 апреля 2016

nponeccop

Велкам ту риал ворлд

У меня тут внезапно вылез real life вариант задачи swizard. Прямо в продакшене.

3 типа исполнительных устройств:
- A: 6 операций A1-A6
- B: одна операция B
- C: одна операция С

3 типа узлов разной стоимости: A, ABC, AC.

Исполнительные устройства независимы. Т.е. на узлах ABC и AC с более чем одним устройством загрузка одного из устройств не влияет на производительность других.

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

Операции занимают случайное время (но со стационарным распределением). Большое количество операций "насыщает" устройство - т.е. загрузка большего количества операций перестаёт увеличивать скорость. Есть феномен "медленных" операций, не насыщающих устройство. Т.е. насыщение, условно, происходит после загрузки 10 быстрых операций или 100 медленных, причём
быстрота или медленность неизвестна до загрузки в операции в устройство. Представьте, например, что устройство B - это кластер, проверяющий зашифрованное число на простоту. Если идут одни чётные - упираемся во внутренний bandwidth устройства, а если одни произведения
двух близких простых сомножителей - упираемся в процессоры. Но т.к.ключ известен только устройству, мы перед загрузкой сами ничего проверить не можем.

Более того, устройство не умеет сообщать внутренние bandwidth и cpu usage, мы можем о них только догадываться, измеряя время. Например, грузим инструкции, засекаем время исполнения каждой. Если результат инструкции, загруженной 30 секунд назад, не получен - помечаем
инструкцию "медленной". Грузим ещё инструкции, пока "кол-во медленных * X + кол-во неизвестных < Y"

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

Теперь о вычислениях.

На входе у нас неограниченный поток однотипных задач T.

Представьте, что у нас T - это теоремы, а операции - это стратегии, сводящие одни теоремы к другим.

Общий воркфлоу такой:

Приходит теорема, мы скармливаем её стратегии A5. Она может либо сразу ответить, что типа противоречие, или выдать нам список лемм [A5R] ("A5 Result").

Лемма A1R сводится стратегией A2 к набору лемм [A2R]. И так далее.

Некоторые тривиальные стратегии Sx реализованы "софтварно". Они исполняются мгновенно без загрузки в узлы.

Формализуется композицией монад списка и исключений. Я просто списки для простоты буду использовать.

Всю схему тоже заебусь формализовывать, сделаю только hot path, показывающий использование всех устройств, но не всех инструкций:

S1 :: T -> ([S1R1], S1R2)
A5 :: S1R2 -> [A5R]
A1 :: A5R -> [A1R]
B :: A1R -> ()
C :: S1R1 -> [S1R1]

Тут ещё проблема, что имеющиеся у нас леммы нельзя доказывать в произвольном порядке.

Представьте что мы консультанты по строительству, T - это проект дома с адресом, а наша задача - определить, можно ли построить дом или нельзя. Практически всегда можно.

A - это юридический отдел. B - геологи, а C - занимаются коммуникациями.

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

Заниматься коммуникациями имеет смысл не тогда, когда готовы все документы для коммуникаций, а когда вообще все документы в порядке.

Т.е. каждый отдельный проект проходит последовательно 3 стадии: A -> C -> B.

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

И сложения можно начинать делать только тогда, когда все умножения закончились. Даже те, которые не являются зависимостями.

Отделу А надо выбирать между A5 S1R2 и A1 A5R в очереди. Если B загружен, а простаивает А - имеет смысл делать A5. Если наоборот - имеет смысл делать A1. Ещё надо контролировать количество проектов, застрявших на стадии A - т.е. отдавать приоритет доделыванию существующих проектов. При недогрузе B имеет смысл в первую очередь ставить A1 из проектов с почти готовой стадией A, а не рандомно.

21 апреля 2016, 21:03

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

Покрой консистентность тестами!

http://highload.guide/blog/saga-cluster.html

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


Чуваки за 15 лет не смогли написать распределенный координатор транзакций, я уже молчу про горизонтальное масштабирование. Если добавить к этому утверждению коре разработчика (который думает что в XA чтение не может быть целостным) то, что у них вместо теорем — покрытие кода тестами, то получится что Постгрес пишут три долбоеба, что и говорить про остальных?

P.S. Даже если я допишу свой CR через 15 лет, все равно я буду на шаг впереди индустрии. Да, на самом деле, EXE/OM появился как продукт необходимый для доказательства распределенных алгоритмов и их экстрактов.

21 апреля 2016, 16:42

swizard

Задачка для интересу

Чёто вакансия вызвала интерес у удивительно малого количества народу, я даже затрудняюсь объяснить этот феномен :) Все так недолюбливают Эрланг? Но у меня же ещё Elm и Rust, и вообще, потенциально определённая свобода в этом плане. Пишите, когда ещё вам предложат попрограммировать с пользой на чём-то неунылом за деньги :)

Для подогрева интереса к вакансии выкладываю тестовую задачку для потенциальных кандидатов. А то чё я её зря что ли придумывал.
UPD 2016-04-20: добавил "sample_9".
UPD 2016-04-21: пофиксил рефенсные тайминги.

Итак, задачка из трёх частей, в порядке увеличения сложности. Делать надо на эрланге, если умеете эрланг, или на чём угодно, если не умеете. Ориентировочные критерии оценки такие:
  • Если человек сделал первую часть, то хорошо: с ним уже есть о чём говорить.
  • Если получилась вторая — очень хорошо.
  • Если третья — совсем круто!

Общее условие

Дана программа в виде упрощённого S-expression (что это?), например:

sample_1() -> <<"(+ (* 4 4) (* 2 (- 7 5)) 1)">>.

где первый элемент каждого списка — это операция (всего их три вида):
  1. сложение: атом "+"
  2. вычитание: атом "-"
  3. умножение: атом "*"
Все остальные возможные атомы — это целые числа.
Ещё примеры:

sample_2() -> <<"10">>.
sample_3() -> <<"(* 10 (- 0 1))">>.
sample_4() -> <<"(- (+ 10 10) -5 0)">>.
sample_5() -> <<"(+ (- (* (+ (- (* 1))))))">>.
sample_6() -> <<"(* 2 (+ (- 10 9) (- 3 (* 2 1))) (+ (- 10 9) (- 3 (* 2 1))))">>.
sample_7() -> <<"(+ (* 2 1) (+ 8 8) (- (+ 4 3 2 1) (* 3 3) (* 2 2)) (* 5 7))">>.
sample_8() -> <<"(- (+ (+ 3 3) (- 3 3) (+ 3 3) (- 3 3)) (* 2 2))">>.
sample_9() -> <<"(+ (- 6 1) (+ 0 1 1) (- 7 2) (* 3 4 5) (- 3 1) (+ 2) (- 0 10))">>.

Задача 1

Реализуйте функцию-интерпретатор "interpret/1" и вычислите результаты вышеприведённых программ.

Например:
interpret(sample_1()). --> 21
interpret(sample_2()). --> 10
interpret(sample_3()). --> -10
interpret(sample_4()). --> 25
interpret(sample_5()). --> 1
interpret(sample_6()). --> 8
interpret(sample_7()). --> 50
interpret(sample_8()). --> 8
interpret(sample_9()). --> 66

Задача 2

Представим, что все операции в программе имеют константную задержку, которая не зависит от процессора. Например, это некоторого рода длительная сетевая активность.
Итого, реализация каждой из операции теперь должна содержать вызов "timer:sleep(X)":
  • X = 2000 ms для сложения "+"
  • X = 3000 ms для вычитания "-"
  • X = 10000 для умножения "*"

Реализуйте функцию-интерпретатор "interpret_network/1", которая вычисляет результат заданной программы с минимально возможной задержкой.

Например:
interpret_network(sample_1()). --> 21 (delay 15 s)
interpret_network(sample_2()). --> 10 (delay 0 s)
interpret_network(sample_3()). --> -10 (delay 13 s)
interpret_network(sample_4()). --> 25 (delay 5 s)
interpret_network(sample_5()). --> 1 (delay 30 s)
interpret_network(sample_6()). --> 8 (delay 25 s)
interpret_network(sample_7()). --> 50 (delay 15 s)
interpret_network(sample_8()). --> 8 (delay 13 s)
interpret_network(sample_9()). --> 66 (delay 12 s)

Задача 3

Представим, что все операции в программе имеют константную задержку, которая зависит от процессора. Например, это некоторого рода тяжелые вычисления, выедающие 100% ядра процессора.
Наша машина оборудована N физическими ядрами.
Итого, реализация каждой из операции теперь должна содержать вызов "timer:sleep(X)", при этом максимальное количество "одновременно выполняющихся" операций должно быть меньше или равно N:
  • X = 2000 ms для сложения "+"
  • X = 3000 ms для вычитания "-"
  • X = 10000 для умножения "*"

Реализуйте функцию-интерпретатор "interpret_cpu/2", которая, используя процессор максимально оптимальным образом, вычисляет результат заданной программы с минимально возможной задержкой.

Например:
interpret_cpu(sample_1(), 2). --> 21 (delay 15 s)
interpret_cpu(sample_2(), 2). --> 10 (delay 0 s)
interpret_cpu(sample_3(), 2). --> -10 (delay 13 s)
interpret_cpu(sample_4(), 2). --> 25 (delay 5 s)
interpret_cpu(sample_5(), 2). --> 1 (delay 30 s)
interpret_cpu(sample_6(), 2). --> 8 (delay 28 s)
interpret_cpu(sample_6(), 3). --> 8 (delay 25 s)
interpret_cpu(sample_7(), 2). --> 50 (delay 26 s)
interpret_cpu(sample_7(), 3). --> 50 (delay 22 s)
interpret_cpu(sample_7(), 4). --> 50 (delay 15 s)
interpret_cpu(sample_8(), 2). --> 8 (delay 15 s)
interpret_cpu(sample_8(), 3). --> 8 (delay 13 s)
interpret_cpu(sample_9(), 2). --> 66 (delay 15 s)


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

21 апреля 2016, 11:31

nponeccop

Упоротое решение задачи SWizard

Если считать, что задача не на оптимизацию, а на concurrency, прокатит ли решение с компиляцией в Makefile?

$ cat Makefile
# (1 + 2) + (3 + 4)

all: op1r op1l
        sleep 2

op1r:
        sleep 2

op1l:
        sleep 2

$ time make
sleep 2
sleep 2
sleep 2

real    0m6.010s
user    0m0.003s
sys     0m0.000s
$ time make -j2
sleep 2
sleep 2
sleep 2

real    0m4.008s
user    0m0.003s
sys     0m0.000s
Upd: ловите компилер: https://gist.github.com/nponeccop/4780d7113c366c80ca04fa167f03919c там допилить вычисления башем - и дело в шляпе. Протащить в преттипринтер Op и всех делов.

21 апреля 2016, 01:40

17 апреля 2016

ru_declarative

MLton

А никто не имел дела с этим:
What is MLton?

MLton is an open-source, whole-program, optimizing Standard ML compiler.
...
Features:
...
Untagged and unboxed native integers, reals, and words.

In MLton, integers and words are 8 bits, 16 bits, 32 bits, and 64 bits and arithmetic does not have any overhead due to tagging or boxing. Also, reals (32-bit and 64-bit) are stored unboxed, avoiding any overhead due to boxing.

Unboxed native arrays.

In MLton, an array (or vector) of integers, reals, or words uses the natural C-like representation. This is fast and supports easy exchange of data with C. Monomorphic arrays (and vectors) use the same C-like representations as their polymorphic counterparts.
А то я когда-то очень давно на него смотрел - но тогда он был откровенно недоношенным, а щас на нем даже какие-то не очень тривиальные проекты вроде пишут.

Выделенные фичи в общем-то привлекательны.

написал kouzdra 17 апреля 2016, 14:09

15 апреля 2016

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

Харпер Одобряет минимальные ядра

Смотрю Харпера и нахожу подтверждение своим словам. Как только Харпер вспомнил про Fix аксиому в ядре — сразу пошел обзывать другие языки говном и мешаниной из концепций которые полностью полностью уничтожают язык. Зная Харпера, понятно что в основном это адресовано в сторону Хаскеля :-) Хотя надо понимать, что все остальные языки вообще даже квалификацию не проходят. Ну кроме его ML/LCF.

Если не верите мне, послушайте Харпера. Рекурсия не нужна!

https://youtu.be/y-lX1mx5_i0?list=PLt7hcIEdZLAnbUxKaG7XIynEWrozOBtXU&t=605

Даже Одерски немного попустился с генетическим разнообразием Scala и решил компактное DOT ядро с макросами сделать, точно также у нас EXE — это просто макросистема над OM.

15 апреля 2016, 10:20

13 апреля 2016

rssh

провели #scalaua

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

Всегда хотел прочитать на какой-то конференции толковый словарь: вот предоставилась возможность ;) [http://www.slideshare.net/rssh1/scala-jargon-cheatsheet ] еще в одном толке - рассказал, почему scala не является моим идеальным языком программирования [ http://www.slideshare.net/rssh1/why-scala-is-not-my-ideal-language-and-what-i-can-do-with-this ]. Плохо что совмещал роль спикера и организатора, к сожалению, времени на подготовку было катастрофически мало (или надо было брать отпуск с работы за месяц, а не за неделю).

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

13 апреля 2016, 11:20

09 апреля 2016

Lambda Kazan

Контест по функциональному программированию на Hackerrank

С 25 по 28 марта на Hackerrank проходил контест по функциональному программированию Lambda Calculi - March 2016. Я в нём участвовал и расскажу немного о впечатлениях.

Утром 25 марта до начала контеста я пошёл в близлежащее кафе Агафредо, чтобы подкрепиться и начать конкурс там. В первые минуты после начала контеста я занимался тем, что открывал вкладки и читал задания, пытаясь при этом не пролить кофе. Олимпиадный опыт участия и проведения ACM помог, почти про все задачи были понятно, как их решать.

Первые впечатления

  • «Functions or Not» — Ad Hoc задача — сортируем список, проверяем, есть ли дубликаты
  • «Compute the Perimeter of a Polygon» — простейшая геометрия, посчитать (внезапно!) периметр — тупо суммируем длины
  • «Compute the Area of a Polygon» — простейшая геометрия, посчитать площадь — берём соседние отрезки, считаем ориентированную площадь треугольника (она же косое произведение) и суммируем
  • «Concave Polygon» — тут я думал, что тоже простейшая геометрия, но оказалось, что она не так проста, как я думал. Об этой задаче чуть позже
  • «Tree Manager» — задача на зипперы, нужно двигаться по дереву и менять его, выполняя команды
  • «Fighting Armies» — тут я думал, что нужно будет писать дерево с балансировками и прочим, но выяснилось, что пакет containers разрешен, и можно взять стандартный Data.Map
  • «Simplify the Algebraic Expressions» — нужно упростить выражение, задача на технику

Я начал решать, и после пары ошибок компиляции понял, что стоило порешать задачи для тренировки. Решив первые три задачи, я понял, что пора бы идти на работу… Утром некоторые коллеги удивились, что я написал, что буду через час, а вроде пришёл на работу, но делаю что-то совершенно другое, сидя на диване и попивая лимонад. Увы, это помогло не слишком сильно, ни одна задача не решилась (но для некоторых был написан ввод и вывод).

Simplify the Algebraic Expressions

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

Беру Parsec, пишу парсер входных данных, пишу простейшее вычисление (поскольку полиномы не выше пятой степени, делаю на списках из шести элементов) и чуть более сложный вывод. Проходит один тест, на двух валится, на четвёртом выдаёт неправильный ответ. Думаю.

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

Думаю. Добавляю кучу скобок ко входным данных, нахожу тест, на котором программа работает неверно. Думаю. Чиню.

Все тесты проходят. На часах 931 минута, или 15:31 с начала контеста.

Concave Polygon

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

Пытаюсь писать, используя имеющийся код для ориентированной площади и проверяя сумму углов между внутренней точкой и парами соседних. Понимаю, что в коде куча подгона и костылей, и… переписываю всё на ray tracing.

Работает, всё проходит, 1004 минуты = 16:44 с начала. Смотрю на таблицу лидеров, отмечаю соперников, которые могут меня обогнать, ложусь спать.

Fighting Armies

Утром вижу, что mipt_vi002 лёг спать позже и обогнал меня. Думаю позавтракать в Агафредо и сажусь решать.

В этой задаче нужно искать максимум в наборе, удалять максимум из набора, добавлять число в набор и объединять два набора.

Пишу на Map. На последних тестах валится по таймауту. Переписываю на Set. На последних тестах валится по таймауту. Переписываю на IntMap (IntMap Int). На последних тестах валится по таймауту.

И тут я замечаю, что в задаче сказано “вход может быть очень большим”. Беру ByteString, немного шаманю — и тесты проходят. Время 1433 минут = 23:53 с начала.

Tree Manager

Мне остаётся победить один тест. Думаю аккуратно расписать случаи. В задаче можно менять значение в узле; печатать его; переходить к левому и правому брату, родителю и сыну с указанным номером; вставлять левого и правого брата и самого левого сына; удалять текущее поддерево.

Расписываю. Ничего не нахожу. Пишу случайные команды. Вижу неправильный ответ.

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

data Tree = Tree { val :: Val, children :: [Tree] }
            deriving (Eq,Show)

-- Зиппер для дерева - это:
-- - родитель (если есть)
-- - левые братья
-- - текущее дерево
-- - правые братья
data Hole = Hole { parents :: Maybe Hole
                 , lefts :: [Tree]
                 , current :: Tree
                 , rights :: [Tree]
                 } deriving (Eq,Show)

cur :: Hole -> Val
cur = val . current

changeCur :: Val -> Hole -> Hole
changeCur new (Hole ps ls c rs) =
  Hole ps ls (c { val = new }) rs

goLeft (Hole ps (l:ls) c rs) = Hole ps ls l (c:rs)
goRight (Hole ps ls c (r:rs)) = Hole ps (c:ls) r rs

-- ошибка: было ls ++ [c] ++ rs
goUp (Hole (Just p) ls c rs) =
  p { current = (current p) { children = reverse ls++[c]++ rs }}

-- ошибка: было (take (k-1) cs)
goDown k now@(Hole p ls (Tree v cs) rs) =
  Hole (Just now)
       (reverse $ take (k-1) cs)
       (cs!!(k-1))
       (drop k cs)

insertLeft x (Hole p ls c rs) = Hole p (empty x : ls) c rs
insertRight x (Hole p ls c rs) = Hole p ls c (empty x : rs)

insertChild x (Hole p ls (Tree v cs) rs) =
  Hole p ls (Tree v $ empty x : cs) rs

-- ошибка: было ls ++ rs
delete (Hole (Just p) ls c rs) =
  p { current = (current p) { children = reverse ls ++ rs }}

Отправляю, тесты проходят. На часах 1464 минуты, или 24:24 с начала контеста. Смотрю таблицу — в десятке. Успокаиваюсь, иду в Агафредо завтракать.

Итоговая таблица контеста

Итоговая таблица контеста

После завершения

Через несколько дней контест завершился, при этом я внезапно оказался на одно место выше (почему-то исчез тот, кто был на первом месте) — на шестом; когда же подвели окончательные итоги и посчитали рейтинг — я написал сюда. Жду футболку с Hackerrank…

Мансур Зиятдинов

9 апреля 2016

Включите JavaScript для участия в дискуссии.

написал Lambdasoft 09 апреля 2016, 00:00

08 апреля 2016

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

Groupoid Infinity FAQ

Ребята, я в теме, будем контрибютить вместе!

Присоединиться очень просто:
1) почитать http://gitter.im/groupoid/om и http://gitter.im/groupoid/exe
2) начать общаться в чате на гиттере
3) контрибютить в репозитории групоида
Мы всегда рады! Это Open Source.

Встреча по вопросам сотрудничества?

Если неофициально в Киеве вы хотите встретиться — для этого достаточно позвонить по телефону: +380 67 663 18 70 :-)
Если официально — можно у меня в офисе HUB4.0
Если неофициально и не лично — приходите на Митап! Будет интересно; Павел Лютко (КНУ) расскажет о кодировках и мы покажем прувер.

Чуваки, отсыпьте книжек! / Я не верю, что по двум книжкам можно написать прувер!

Что касается литературы — то там на самом деле читать очень много (чтобы дойти до такой степени безумия); конечно же я все упрощаю в блоге :-) Должна быть вышка и функан, чтобы примеры ТК были прикладными и ты чувствовал немного основные категории математики. Потом я бы начал так (каталоги неполны, список можно и нужно расширить, просто наброски):
1. Теория Категорий в полном объеме: http://rnyingma.synrc.com/publications/cat/Category%20Theory/
2. Логика и Теория Типов, Топосы
http://rnyingma.synrc.com/publications/cat/Logic/
http://rnyingma.synrc.com/publications/cat/Category%20Theory/Type%20Theory/
http://rnyingma.synrc.com/publications/cat/Category%20Theory/Toposes/
3. Прикладные языки: Нетпизированная лямбда, Система F (F-Алгебры), Зависимая теория (F,G-диалгебры).
4. Теория типов Мартина Лефа и современные пруверы Coq Agda HOL Lean F*
5. Гомотопическая теория
6. Что касается кодировок, то тут можно отметить работы Geuvers, Peng Fu и Dybjer.
7. Дополнительная литература тут: https://github.com/groupoid/om/blob/master/doc/om.tex#L777-L812 (я ее буду комментировать на митапе)


Хто ви в біса такі?

Это совместный продукт КНУ и КПИ. Из ролей у нас Паша — “академик” (КНУ), Я за организацинную часть отвечаю и имплементацию “инженер” (КПИ), Андрей — "специалист по лямбда исчислению" (ХТУ), Влад — "идейный входновитель, сыгравший роковую роль в истории проекта" (КПИ) :-)

08 апреля 2016, 01:32