buka

У нас есть некоторые результаты

Сетоид с зависимыми типами на чистом CoC, который проходит тайпчекинг (c) Zeit Raffer
Пока самый умный чувак с кем мне приходилось работать :-)

Originally posted by zeit_raffer at это одноточечный сетоид
user@athlon ~/github/zraffer/CoC-over-PTS/cat $ morte < Unit/PointOk
∀(AND : *) → ∀(pair : ∀(aaa : ∀(UnitElType : *) → ∀(UnitElProp : UnitElType → *) → ∀(UnitEqu : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → *) → ∀(UnitEquRefl : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → UnitEqu a aok a aok) → ∀(UnitEquTrans : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → ∀(c : UnitElType) → ∀(cok : UnitElProp c) → UnitEqu a aok b bok → UnitEqu b bok c cok → UnitEqu a aok c cok) → ∀(UnitEquSym : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → UnitEqu a aok b bok → UnitEqu b bok a aok) → ∀(UnitPoint : UnitElType) → ∀(UnitPointOk : UnitElProp UnitPoint) → UnitElProp UnitPoint) → ∀(bbb : ∀(XUnitElType : *) → ∀(XUnitElProp : XUnitElType → *) → ∀(XUnitEqu : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → *) → ∀(XUnitEquRefl : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → XUnitEqu a aok a aok) → ∀(XUnitEquTrans : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → ∀(c : XUnitElType) → ∀(cok : XUnitElProp c) → XUnitEqu a aok b bok → XUnitEqu b bok c cok → XUnitEqu a aok c cok) → ∀(XUnitEquSym : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → XUnitEqu a aok b bok → XUnitEqu b bok a aok) → ∀(XUnitPoint : XUnitElType) → ∀(XUnitPointOk : XUnitElProp XUnitPoint) → ∀(YUnitElType : *) → ∀(YUnitElProp : YUnitElType → *) → ∀(YUnitEqu : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → *) → ∀(YUnitEquRefl : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → YUnitEqu a aok a aok) → ∀(YUnitEquTrans : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → ∀(c : YUnitElType) → ∀(cok : YUnitElProp c) → YUnitEqu a aok b bok → YUnitEqu b bok c cok → YUnitEqu a aok c cok) → ∀(YUnitEquSym : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → YUnitEqu a aok b bok → YUnitEqu b bok a aok) → ∀(YUnitPoint : YUnitElType) → ∀(YUnitPointOk : YUnitElProp YUnitPoint) → ∀(onElType : XUnitElType → YUnitElType) → ∀(onElProp : ∀(el : XUnitElType) → XUnitElProp el → YUnitElProp (onElType el)) → ∀(onEqu : ∀(elA : XUnitElType) → ∀(okA : XUnitElProp elA) → ∀(elB : XUnitElType) → ∀(okB : XUnitElProp elB) → XUnitEqu elA okA elB okB → YUnitEqu (onElType elA) (onElProp elA okA) (onElType elB) (onElProp elB okB)) → ∀(onPoint : YUnitEqu (onElType XUnitPoint) (onElProp XUnitPoint XUnitPointOk) YUnitPoint YUnitPointOk) → YUnitEqu (onElType XUnitPoint) (onElProp XUnitPoint (aaa XUnitElType XUnitElProp XUnitEqu XUnitEquRefl XUnitEquTrans XUnitEquSym XUnitPoint XUnitPointOk)) YUnitPoint (aaa YUnitElType YUnitElProp YUnitEqu YUnitEquRefl YUnitEquTrans YUnitEquSym YUnitPoint YUnitPointOk)) → AND) → AND

λ(AND : *) → λ(pair : ∀(aaa : ∀(UnitElType : *) → ∀(UnitElProp : UnitElType → *) → ∀(UnitEqu : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → *) → ∀(UnitEquRefl : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → UnitEqu a aok a aok) → ∀(UnitEquTrans : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → ∀(c : UnitElType) → ∀(cok : UnitElProp c) → UnitEqu a aok b bok → UnitEqu b bok c cok → UnitEqu a aok c cok) → ∀(UnitEquSym : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → UnitEqu a aok b bok → UnitEqu b bok a aok) → ∀(UnitPoint : UnitElType) → ∀(UnitPointOk : UnitElProp UnitPoint) → UnitElProp UnitPoint) → ∀(bbb : ∀(XUnitElType : *) → ∀(XUnitElProp : XUnitElType → *) → ∀(XUnitEqu : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → *) → ∀(XUnitEquRefl : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → XUnitEqu a aok a aok) → ∀(XUnitEquTrans : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → ∀(c : XUnitElType) → ∀(cok : XUnitElProp c) → XUnitEqu a aok b bok → XUnitEqu b bok c cok → XUnitEqu a aok c cok) → ∀(XUnitEquSym : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → XUnitEqu a aok b bok → XUnitEqu b bok a aok) → ∀(XUnitPoint : XUnitElType) → ∀(XUnitPointOk : XUnitElProp XUnitPoint) → ∀(YUnitElType : *) → ∀(YUnitElProp : YUnitElType → *) → ∀(YUnitEqu : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → *) → ∀(YUnitEquRefl : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → YUnitEqu a aok a aok) → ∀(YUnitEquTrans : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → ∀(c : YUnitElType) → ∀(cok : YUnitElProp c) → YUnitEqu a aok b bok → YUnitEqu b bok c cok → YUnitEqu a aok c cok) → ∀(YUnitEquSym : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → YUnitEqu a aok b bok → YUnitEqu b bok a aok) → ∀(YUnitPoint : YUnitElType) → ∀(YUnitPointOk : YUnitElProp YUnitPoint) → ∀(onElType : XUnitElType → YUnitElType) → ∀(onElProp : ∀(el : XUnitElType) → XUnitElProp el → YUnitElProp (onElType el)) → ∀(onEqu : ∀(elA : XUnitElType) → ∀(okA : XUnitElProp elA) → ∀(elB : XUnitElType) → ∀(okB : XUnitElProp elB) → XUnitEqu elA okA elB okB → YUnitEqu (onElType elA) (onElProp elA okA) (onElType elB) (onElProp elB okB)) → ∀(onPoint : YUnitEqu (onElType XUnitPoint) (onElProp XUnitPoint XUnitPointOk) YUnitPoint YUnitPointOk) → YUnitEqu (onElType XUnitPoint) (onElProp XUnitPoint (aaa XUnitElType XUnitElProp XUnitEqu XUnitEquRefl XUnitEquTrans XUnitEquSym XUnitPoint XUnitPointOk)) YUnitPoint (aaa YUnitElType YUnitElProp YUnitEqu YUnitEquRefl YUnitEquTrans YUnitEquSym YUnitPoint YUnitPointOk)) → AND) → pair (λ(UnitElType : *) → λ(UnitElProp : UnitElType → *) → λ(UnitEqu : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → *) → λ(UnitEquRefl : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → UnitEqu a aok a aok) → λ(UnitEquTrans : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → ∀(c : UnitElType) → ∀(cok : UnitElProp c) → UnitEqu a aok b bok → UnitEqu b bok c cok → UnitEqu a aok c cok) → λ(UnitEquSym : ∀(a : UnitElType) → ∀(aok : UnitElProp a) → ∀(b : UnitElType) → ∀(bok : UnitElProp b) → UnitEqu a aok b bok → UnitEqu b bok a aok) → λ(UnitPoint : UnitElType) → λ(UnitPointOk : UnitElProp UnitPoint) → UnitPointOk) (λ(XUnitElType : *) → λ(XUnitElProp : XUnitElType → *) → λ(XUnitEqu : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → *) → λ(XUnitEquRefl : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → XUnitEqu a aok a aok) → λ(XUnitEquTrans : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → ∀(c : XUnitElType) → ∀(cok : XUnitElProp c) → XUnitEqu a aok b bok → XUnitEqu b bok c cok → XUnitEqu a aok c cok) → λ(XUnitEquSym : ∀(a : XUnitElType) → ∀(aok : XUnitElProp a) → ∀(b : XUnitElType) → ∀(bok : XUnitElProp b) → XUnitEqu a aok b bok → XUnitEqu b bok a aok) → λ(XUnitPoint : XUnitElType) → λ(XUnitPointOk : XUnitElProp XUnitPoint) → λ(YUnitElType : *) → λ(YUnitElProp : YUnitElType → *) → λ(YUnitEqu : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → *) → λ(YUnitEquRefl : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → YUnitEqu a aok a aok) → λ(YUnitEquTrans : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → ∀(c : YUnitElType) → ∀(cok : YUnitElProp c) → YUnitEqu a aok b bok → YUnitEqu b bok c cok → YUnitEqu a aok c cok) → λ(YUnitEquSym : ∀(a : YUnitElType) → ∀(aok : YUnitElProp a) → ∀(b : YUnitElType) → ∀(bok : YUnitElProp b) → YUnitEqu a aok b bok → YUnitEqu b bok a aok) → λ(YUnitPoint : YUnitElType) → λ(YUnitPointOk : YUnitElProp YUnitPoint) → λ(onElType : XUnitElType → YUnitElType) → λ(onElProp : ∀(el : XUnitElType) → XUnitElProp el → YUnitElProp (onElType el)) → λ(onEqu : ∀(elA : XUnitElType) → ∀(okA : XUnitElProp elA) → ∀(elB : XUnitElType) → ∀(okB : XUnitElProp elB) → XUnitEqu elA okA elB okB → YUnitEqu (onElType elA) (onElProp elA okA) (onElType elB) (onElProp elB okB)) → λ(onPoint : YUnitEqu (onElType XUnitPoint) (onElProp XUnitPoint XUnitPointOk) YUnitPoint YUnitPointOk) → onPoint)


(да, я писал ЭТО руками - на основе http://zeit-raffer.livejournal.com/119247.html )
Buy for 20 tokens
Buy promo for minimal price.
buka

Эрланг Ебанаты. Выпуск #2

Ох давно такого в ЖЖ не было. Но мы спонсируем. Все говно которые вылазит из так называемых программистов вы уже можете наблюдать, собственно ради этого все и затевалось. Чтобы искренность ебанизмов полезла наружу. Что мне нравится в срачах в ЖЖ так это то, что можна увидеть истинное лицо человек. Истинную его ебанистическую натуру. Например спрашиваешь человека, скажи правду, а он увиливает и мычит что-то. Или еще хуже скатывается в днище какое-то :-) Собственно ниже дна ЖЖ уже мало что есть. Даже ДОУ более искренее. Там ебанаты какие-то "сферические в ваккуме" что-ли. А тут реально Интервата.

Итак ретроспектива проекта с хуйовой кармой "Какаранет".

2010 год. Турки нанимают эрланг-ебаната Кунтара в качестве СТО и просят сделать проект который сможет держать 2 миллиона пользователей. OKEY — это игрушка в которую играют тупо поголовно все в Турции, поэтому Эрланг кажется логичным решением. Кунтар нанимает бразильцев (известную эрланг кантору) те рисуют техзадание и пишут какой-то ПабСаб (код я выкинул потому что в 2010 эта кантора учила эрланг на этом проекте). Бразильцы выставляют ниибический счет, Кунтар принимает решение не платить. Суд. Кунтар меняет заказчика на известного эрлангиста Павла Перегуда, тот ему пишет playable OKEY код и Кунтар принимает решение делать клиента на Flash. В 2010 это было решение вроде как ОК. Был уже Haxe и вприниципе можно было бы что-то нормальное запилить, если бы не наняли ебанатов-флешеров.

Кунтар нанимает Massive Solutions и генеральный директор просто охуевает от Кунтара и его идей, все заканчивается очень печально. Весь отдел что-то ебашит, в итоге 50 штук зависают в воздухе. Второе судебное разбирательство. На самом деле третье так как Перегуду тоже вроде недоплатили, просто он парень скромный в суд не подал.

2011 год. Ноябрь. Я сижу в ритрите под Москвой мне звонит Кунтар и приглашает на работу. Я приезжаю через 3 месяца (2012 Январь) в Киев и знакомлюсь с Кунтаром. Надо сказать что Кунтра веселый и похож на Карлсона, а я как Малыш на эрланге до этого не писал ничего в жизни.

[ Лирическое отступление: Кроме LDAP сервера для fprog #7, который меня попросил оформить в виде статьи Кирпичев и неудачного проекта с еще одним Эрланг-Ебанатом Олегом Смирновым, на этом проекте работал еще Соловьев Кложурист с известным видео в сети, проект ебанистический, назовем его условно "малайзиский", никому не заплатили, мне висят 5 штук до сих пор). Сразу после этого проекта я разосрался с Олегом, но это никого не касается: Олег считает что я ебанат, я что он. Все по чесному ].

Были еще на этом проекта ситуативные эрланг-ебанаты и флеш-ебанаты, которым Кунтар нихуя не платил и выгонял через месяц работы. Впринципе я тогда был человек наемный и просто получал деньги, изучая riak, erlang, код Павла Перегуда (который по сути с правками Сергея так и составил основу гейм сервера). Нитроген, Риак, erlando, gettex, mochiweb и еще 30 библиотек, которые предыдущие эрланг-ебанаты втащили в проект. Понемногу начинаю понимать, что все вокруг полные дибилы.

2012 Август. Я еду в паломнический тур по 22 монастрымя ваджраяны в Индии. Возвращаюсь и еду в Турцию знакомиться с заказчиками, там живу в отеле наслаждаюсь пахлавой и донерами, катаюсь на корабликах и ем клубнику, черешни и фиги, паралельно исследуя возможность стресс тестирования гейм сервера и веб фремворка. Я готовлю тщательно нагрузочное тестирование чистого ковбоя и нитрогена (именно тогда я начал готовить статью http://maxim.livejournal.com/392587.html) которую опубликовал в январе 2013 после того как ко мне приехала Маша и вдохновила меня. После публикации статьи понимаю что Нитроген как идея суперохуенен, но как реализация полное дерьмище. С этого момента я тверд решимости клонировать Нитроген и полносью его нахуй переписать, потому что на Эрланг-ебаната Джесси Гамма (майнтейнера нитрогена) нет никакой надежды. Новый год праздновали с Машей в Стамбуле.

2013 Февраль. Уже к этому времени у нас работал Сергей, которому было поставлена задача полностью переписать и оформить гейм сервер. Кроме Сергея гейм сервер никто после этого не трогал. У меня было чем заниматься, тогда у нас был кластер из 9-х серверов риака и 3-х RabbitMQ и трех инстансов с glusterfs. Тогда у меня закралась идея выбросить это все нахуй, или хотя бы не выбросить а прототипировать на чем-то попроще, например на mnesia, а когда выходить впродакшин уже кроли и риак. Так родилась идея KVS, абстрактной библиотеки для KV бекендов — протипируешь на мнезии, в взлетаешь на риаке.

Турки вызывают меня и говорят мне открыто и чесно, что Кунтар их заебал. Что он потратил все их бабки и они хотят уволить и спрашивают готов ли я взять все на саой контроль. Я говорю говно вопрос. Кунтар сам уходит, потому что это все его заебало еще больше. Шутка ли он хотел полностью повторить всю функциональность фейсбука. Я анонсирую Туркам свое видение проекта — отказать от фейсбук-идеи и ебашить только игру. Турки не соглашаются и просять отставить форумы, лайка, посты, группы, подписки, и всю эту ебалу. В это время у нас работал akalenuk, он не даст соврать, что это все реально его заебывало. Но что делать упоротый заказчик платит. Естественно мы это все не потягивем и турки нам зависают быбло, все разъезжаются по домам в Апреле 2013.

2013 Май. Я вернулся в Киев и мы c doxtop открываем s.r.o. Снимаем офис и ставим себе задачу написать N2O и KVS и писать на них сайтики. Берем проект у Калифорнийских долбоебов, Доктор им пишет CMS на N2O, нам недоплачивают и проект уходит в архив. С доктором мы просидели до осени. Доктор понимает, что на N2O и KVS жену не прокормишь и уходит в Плейтек израильский. Покупает себе Туарег и отстраняется от Эрланга и переходит на Scala. Я зависаю с Кириловым, провожу тренинги и мастер классы, развиваю N2O и KVS потому что свято верю что у меня все получится. К нам приезжают турки и слезно просят продолжить проект мы ласково с доктором их шлем нахуй через перводчицу, они выплачивает неполную сумму, половину из которо мы отдаем Сереге, а вторую делим пополам. Все по чесному, Сергей на нас не в обиде.

2014 Март. Турки делают мне приглашение от которого я не могу отказаться продолжить заниматься проектом. Они оплачивают мне поезду в калифорнию, где я покупаю себе Макбук, выступаю с докладом по N2O, а турки в свою очередь отказывають от идеи Фейсбука и согласны на просто игру. Но нужно же что-то делать с флешовым клиентом, его пора уже выбрасывать. Так как у нас в N2O уже есть BERT и вебсокеты, поэтому я советую туркам не платить мне бабки, вкинуть все в профессиональных художников и JavaScript программистов. Я нахожу студию Intersog одесскую и Вячеслав Потравный хуярит новый OKEY клиент а я делаю к нему бекент, и сокращаю (фактически выбрасываю встроенный фейсбук) бекенд до 400 строк (все остально за счет N2O). База 120 строк. Сервер остался Сергея (10K LOC) потому что он тупо работал и там дохуища функциональности. Там были турниры, которые я подозреваю что Эрланг-ебанат Джамшут хуй реализовал так как надо, раз он сократил там все в 3 раза. Я просто не верю что у него работают турниры. Пусть покажет мне работающие турниры (это я вам скажу в любой игре турниры дохуя кода займут, кто писал MMORPG тот знает). Но ладно оставим Джамшуда в покое, хватит насиловать труп. Счас речь идет о других эрланг-ебанатах. Так вто этот прототип без фейсбука на новом N2O и KVS этот проект он публичный https://github.com/synrc/games Этот проект я сделал за 1 месяц сам (ну кроме клиента, который Intersog писали и рисовали). Но склеивал все я сам за неделю, паралельно изучая джаваскрип и беря уроки у Юлии Пучниной. А потом оказалось что ошибок там столько что еще пару неделек я это все багфиксал, но то такое играть можно было уже через месяц.

2014 Май. Турки висят мне опять бабло. И у меня просходин нервный срыв. Одной половиной мозга я понимаю, что все это не напрасно и что я доказал самому себе что я могу сам сделать игрушку на джаваскрпте и испробовал N2O в реальном бою. Второй половиной мозга я хочу разломать череп Синану и Ахмеду. Я возвращаюсь в Киев и забываю про турков навсегда.

Новая история. Солнцеликий ПриватБанк (БЕЗ Эрланг-Ебанатов, но с нормальными пацанам)

2014 Осень. Меня находят мои прекрасный друзья из Приватбанка и дают мне неограниченную власть в своем отделе. Я туда привожу N2O, KVS, BPE, UPL, FORMS, MAD и весь свой стек. За 2 месяца я делаю прототип который представляю лично СТО Приватбанка. СТО дает добро уволить отдел Python-ебанатов у которых 100 SQL таблиц на джанго и проект стартует 10 минут, бесконечное колчество ошибок. Наш проект стартует за 1 секунду и занимет в 100 раз меньше места в виде исходиников (счас всего лишь в 10) и может обслужить весь дневной объем клиентов за 7 секунд. За историю нашего проекта в Привате не было ни одного инцидента на продакшине. Все в ахуе и мы тоже.

2015. Через нашу систему в ПриватБанке было открыто депозитов на 20 миллиардов. Каждый клиент ПриватБанка, который пользуется депозитами (через касиров или сам) пользуется нашей системой написанной на N2O. У нас три вкладки в интернет банке Приват24.

2016. Я решаю посвятить себя написанию языка с зависимыми типами, чтобы доказывать свойства KVS и N2O и предствить миру первый в истории прувабл веб фреймворк, паралельно родив язык не хуже Scala для виртуальных машин BEAM и LING.
buka

Новая Рубрика: Эрланг Ебанаты. Выпуск #1

Иногда захожу в ЖЖ и ищу слова "Erlang" и "Эрланг" в поиске. Только эти. Если вы увидели у себя в каментах меня, скорее всего я пришел к вам по этим словам. Новый персонаж это jamhed, которого турки (которые висят Massive Solutions (которые LING сделали между прочим!) 50 тонн) взяли на работу вместо меня. До этого он терся у меня в каментах и пытался "дискутировать" в духе Зефирова. Я его сразу нахуй послал, не подумав. А этот хуй оказывается злобный ебанашка. Устроился к туркам на работу взял наш код и пробует его "рефакторить" и учить эрланг. Паралельно вспоминая как я его послал нахуй и периодически вырыгивая у себя в ЖЖ что-то типа Эрланг за 2 недели (сколько можно Валкина цитировать, не заебало еще) или Срывает покровы имплементации нашего гейм сервера, который написал Сергей (Если бы Богатырь Сергей при встрече увидел этого Моджахеда он бы его вогнал по пояс в землю), или вот еще прекрасное: Посчитал сколько он туркам бабла сэкономил. Ну и вот блядь Неофиты. Мы неофиты :-)

Напоминаю Джамшуду, что вот эту хуйню я сделал за 1 человеко-месяц. Сам прототип пацанам из Intersog нарисовал на JavaScript как йобаный раб (а то они хотели мне это все на css и png сделать), заодно дизайнерам ихним Sketch показал, а то они до сих пор бы ебались в илюстраторе с экспортом SVG:

http://ns.synrc.com:8080/static/app/index.htm

А он уже там работает вроде как скоро год и у него пока только вот эта хуйня http://kakaranet.com которая позволяет, чтобы на столе было больше 15 карт :-)

Если задумаете нас тролить, сначала взвесьте все за и против, ребята. Посмотрите на свой гитхаб и наш :-)
buka

Прелюдия Здорового Человека

Логотип HoTT-совместимого функционального языка с зависимыми типами в котором существуют только две первоклассные конструкции enum (для индуктивных зависимых типов) и record (для зависимых первоклассных модулей). Без тайпклассов и рекурсии, но с паттерн мачингом.



-------------------------------------------------------------------------
Polynomial       Polynomial
Non-dependent    Non-dependent          Non-Polynomial    Non-Polynomial
Non-Recursive    Recursive              Non-Recursive     Recursive      
Cartesian        Functorial             DepTypes/Kinds    Dependent Types
                 F-(Co)Algebras                Fibrational F,G-Dialgebras
---------------- ---------------------- ----------------- ---------------
SUM              INDUCTIVE              ?                 ENUM
- Bool           - Nat                  - Eq              - Vector
- Option         - List                 - Exists          
- Unit           - IO
---------------- ---------------------- ----------------- ---------------
PRODUCT          COINDUCTIVE            SIGMA/RECORD      RECORD
- Pair           - Stream               - Pure            - InfGraph
                 - Process              - Functor         - InfGroupoid
                 - Effect               - Applicative     
                                        - Monad
-------------------------------------------------------------------------


           record equ (e: *): * := (rel: e → e → Prop)
           record setoid (e: *) extend equ
                      := (refl:  rel e e)
                         (trans: rel e1 e2 → rel e2 e3 → rel e1 e3)
                         (sym:   rel e1 e2 → rel e2 e1)

             enum unit: * :=
                  (make: () → unit)

             enum bool: * :=
                  (true: () → bool)
                  (false: () → bool)

             enum IO: * :=
                  (out: list num → () → IO)
                  (in:  () → list num → IO)

             enum option: (A:*) → * :=
                  (none: () → option A)
                  (some: A → option A)

             enum product: (A:*) → (B:*) → * :=
                  (make: (a:A) → (b:B) → prod A B)

             enum sum: (A:*) → (B:*) → * :=
                  (make: (a:A) → (b:B) → sum A B)

             enum nat: * :=
                  (zero: () → nat)
                  (succ: nat → nat)

             enum list: (A:*) → * :=
                  (nil: () → list A)
                  (cons: A → list A → list A)

             enum vector: (A:*) → nat → * :=
                  (nil: () → vector A)
                  (cons: (n: nat) → A → vector A n → vector A (succ n))

           record lists: (A B: *) :=
                  (len: list A → integer)
                  ((++): list A → list A → list A)
                  (map: (A → B) → (list A → list B))
                  (filter: (A → bool) → (list A → list A))

           record infgraph: * :=
                  (ob: *)
                  (hom: ob → ob → infgraph)

             enum eq: (A:*) → A → A → * :=
                  (refl: (x:A) → eq A x x)

             enum exists: (A:*) → (A → *) → * :=
                  (exists-intro: (P: A → *) → (x:A) → P x → exists A P)

           record pure (P: * → *) (A: *) :=
                  (return: P A)

           record functor (F: * → *) (A B: *) :=
                  (fmap: (A → B) → F A → F B)

           record applicative (F: * → *) (A B: *)
           extend pure F A,
                  functor F A B :=
                  (ap: F (A → B) → F A → F B)

           record monad (F: * → *) (A B: *)
           extend pure F A,
                  functor F A B :=
                  (join: F (F A) → F B)
buka

Phoenixframework vs N2O

http://erlang.org/pipermail/erlang-questions/2016-January/087452.html

Получил такое письмо только что. Думал сразу ебануть ответочку в рассылку, но сначала тезисно в ЖЖ, и начну этот ответ так.

Я обычно избегаю постить в расслылку про использвание N2O и продуктов на N2O (это кстати чистая правда, вы там от меня один пост только найдете). Но если вам нужны Вебсокеты, то вот что я могу сказать по этому поводу (кроме https://websockets.erlang.one конечно, это было сказано миру благодаря zamotivator, храни его боженька).

1. N2O поддерживает фолбек начиная с версии 2.3, как известно из истории. Зачем? Только три китайца в мире из провинции Хуй Пиз Ды знают зачем нужен фолбек, ну и в Бразилии очевидно тоже нужен. Еще Валкин говорил, что в США нужен у AT&T оператора. Хотя у меня в штатах вебсокеты работали без SSL, хуй знает какой у меня оператор был.

2. Кросс-орижин? Поддержку этого в N2O занимает ровно четыре строки. Зачем это выделять в отдельный пункт и хвастаться этим — мне неясно.

3. Поддержка IE8 без вебсокетов? В N2O XHR fallback настолько маленький, что я могу привести его имплементацию полностью в этом посте!

$xhr = { heart: false, interval: 100, creator: function(url) { $conn.url = xhr_url(url);
         $xhr.channel = { send: xhr_send, close: xhr_close }; $conn.onopen();
         return $xhr.channel; }, onheartbeat: function() { xhr('POST',{});} };

transports = [$ws,$xhr];

function xhr_header(request) { request.setRequestHeader('Content-Type','application/x-www-form-urlencoded; charset=utf-8'); }
function xhr_url(url) { return url.replace('ws:', 'http:').replace('wss:', 'https:'); }
function xhr_close() { $conn.onclose(); clearInterval(heartbeat); }
function xhr_send(data) { return xhr('POST',data); }
function xhr_receive(data) { if (data.length != 0) $conn.onmessage({'data':data}); }
function xhr(method,data) {
    var request = new XMLHttpRequest();
    request.open(method,$conn.url,true);
    xhr_header(request);
    request.onload = function() { console.log(request.response); xhr_receive(request.response); };
    request.send(data);
    return true; }


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

4. Возможность использовать только SSL? Вроде как любой может вебсокеты на SSL поднять, попробуйте поднимите без SSL у AT&T провайдера. Почему Вебсокет должен блокировать SSL, а не скажем nginx или тот кто терминирует — мне не понятно.

5. Ниибически крутые якобы каналы на gen_server (доказано на какой-то мегаксеон тачке, на которой 2 миллиона конекций ковбой держал). Я вообще не понимаю как каналы на gen_server могут быть быстрее N2O, который ВООБЩЕ НЕ СОЗДАЕТ НИКАКИХ ПРОЦЕССОВ. N2O работает исключетельно в процессах ковбоя, мы не спавним для интерконнекта вообще ничего. Более легковесной хуйни вы просто не придумаете. А мы придумаем! Мы уже написали вебсокет сервер, чтобы выбросить нахуй уебищный ковбой. Мы вам такие цифры нарисуем на обычном BEAM (про LING на Xen я вообще молчу), что вы ебанетесь.

6. Распределенная ПабСаб система для каналов? С первой версии N2O поддерживает кастомные ПабСаб системы. В качестве дефолтной используется gproc от Ульфа. Я конечно люблю Жозе, но вряд ли он ебанул что-то круче gproc + unsplit (кстати эта хуйня у меня работала успешно 3 года назад). Работает в дистрибютед режиме? RLY? Интересно, рассказали ли об этом https://aphyr.com, а то пацаны то и не знают. Каждый месяц вижу новый распределенный ПабСаб на эрланге на ETS таблицах на гитхабе. И все думают, что это персистетный(!), распределенный(!) пабсаб. Уверены в этом!

7. Феникс — 7600 LOC, N2O — 1200 LOC. Долго искал что феникс умеет такое, что N2O не умеет, но так и не нашел. Вроде как на Эликсире короче должно быть? Я помню как мы с Кирилловым решали на перегонки тестовое задание для того, чтобы устроиться на работу к Валкину. На эликсире тот игрушечный toy_leader занял 170 строк, на Эрланге 70. С тех пор у меня ощущение, что с Эликсиром хиспеторв наебуют.

Но вприципе это похуй, все равно хипстеры этот ЖЖ не читают, так что я думаю не сильно им подпорчу репутации. Когда будете сравнивать также не забудьте, что для того чтобы поставить Феникс вам придется скачать Эликсир!!! А это не 7 с хуем, а уже 75 тысяч строк кода :-) Напомню, что n2o вытаскивается с гитхаба, билдится вместе с рабочим примером и запускается полностью за 50 секунд (все вместе).

8. Что есть в N2O чего нет в Фениксе? Незнаю есть ли у них вот такой крутой File Upload, который может ебашить 25Мегобайд в секунду прямо с браузера? http://5ht.co/ftp.htm Поддерживает докачку и обрывы со стороны клиента и сервера, занимает 80 строк кода. Можно портировать на чистый ковбой, если есть мозг. Вообще имея 80 строк рабочего кода, можно портировать куда угодно.



Эту хуйню написал doxtop, за что храни его Лямбдагарбха, здоровья ему и долголетия. Он счас на Scala пишет с чуваками которые любят Java, поэтому здоровье ему понадобится.

9. N2O поддерживает разные форматтеры: JSON, XML, BERT и можете другие подключать. Врядли Феникс такое умеет, везде JSON по вебсокетам ездит. Кто пишет так называемый Hiload (это модно счас так говорить или уже нет?) тот знает, что любой JSON парсер на стороне сервера хуже чем никакого парсера. Но хипстеры любят JSON, а банкам похуй, поэтому в банках работает N2O, а на фениксе я пока ни одного сайта не видел где было бы 2 миллиона пользователей (как заявлено в интернетах), а N2O обслуживает 30 миллионов украинчегов в самом большом банке страны.

10. Персистенс, CRDT? Это блядь смешно. Имея такую офигенскую базу данных как mnesia, искать прибежища в хуйовом riak_core это нужно постараться. Победитель гугллового поиска "mnesia сыпется 2ГБ потрачено". Все ватники Всея Руси во главе с ебанатом Лапшой уверены, что mnesia не годится вообще. Отец Эрланга, Валкин, тоже уверен. Все уверены, а нам похуй. У нас мнезия работает 3 года, ни одного инцидента. Стопаем по CTRL+C, DETS таблицы (disc_only_copies), поднимается база за несколько секунд, терабайты. WhatsApp работает на mnesia в режиме disc_copies, а все русские мычат, что никто не умееет ее готовить. Пусть мычат. Караван идет, как говорится. Секреты раскрывать не будем, скажем только что это все у нас работает на штатном open-source продукте, KVS, это типа библиотека-компаньон для персистенса (redis, mnesia, SQL, filesystem, mongodb драйвера), которую опять же написал святой монах doxtop. Доктор вообще все написал и N2O и KVS, я просто на супорте сижу. Кстати тот HoTT совместимый язык который мы пишем — мы пишем для того, чтобы сертифицировать KVS, который занимает всего 300 строк (без драйверов).

11. Кто использует BERT.js написаный Расти тот петрушка. Потому что BERT.js был написан еще во времена, когда небыло бинарных буферов в ждваскрипте. Там на строках склеивается строка (и заявляется что это якобы бинарь). Просто потому что я могу — привожу полный текст BERT декодера который написан Андреем Мартемьяновым:

function nop(b) { return []; };
function big(b) { var sk=b==1?sx.getUint8(ix++):sx.getInt32((a=ix,ix+=4,a)); ix+=sk+1; return []; };
function int(b) { return b==1?sx.getUint8(ix++):sx.getInt32((a=ix,ix+=4,a)); };
function dec(d) { sx=new DataView(d);ix=0; if(sx.getUint8(ix++)!==131)throw("BERT?"); return din(); };
function str(b) { var dv,sz=(b==2?sx.getUint16(ix):sx.getInt32(ix));ix+=b;
                  var r=sx.buffer.slice(ix,ix+=sz); return b==2?utf8_dec(r):r; };
function run(b) { var sz=(b==1?sx.getUint8(ix):sx.getUint32(ix)),r=[]; ix+=b;
                  for(var i=0;i<sz;i++) r.push(din()); if(b==4)ix++; return r; };
function din()  { var c=sx.getUint8(ix++),x; switch(c) { case 97: x=[int,1];break;
                  case 98:  x=[int,4]; break; case 100: x=[str,2]; break;
                  case 110: x=[big,1]; break; case 111: x=[big,4]; break;
                  case 104: x=[run,1]; break; case 107: x=[str,2]; break;
                  case 108: x=[run,4]; break; case 109: x=[str,4]; break;
                  default:  x=[nop,0]; } return {t:c,v:x[0](x[1])};};


Энкодер не намного длинее, 30 LOC всего. Внимательно почитайте, а потом загляните в BERT.js.

12. Ключевые JavaScript файлы N2O если зазиповать то они занимают меньше 1400 байт. Это означает, что весь N2O/JavaScript помещается в MSS окно -- хуйня недосягаемая ни для одного веб фреймворка в мире!

13. Есть еще n2o.hs, но его специально нет на Хакадже, чтобы ебанаты-ватники типа Зефира продолжали жрать свое Хаскель говно. N2O.Haskell написал не абы кто, а сам nponeccop. Так шо вы осторожнее набрасывайте.

Пост написан специально для doxtop, чтобы он улыбнулся и выздоровел :-)
buka

Provable LING

Как вы знаете в нашем стеке все, что выше Эрланга будет сшиваться с помощью (ко)индуктивных зависимых типов, которые служат основным средством выражения различного рода аксиом, как то EQ или других. Например в ядре Morte нет произведений, поэтому само произведение — это индуктивный тип Prod с единственным конструктором:

    enum prod: (A:*) → (B:*) → * :=
         (make: (a:A) → (b:B) → prod A B)

Другие соотвествия:
    EXE            LING          LING
    Inductive      Erlang        Erlang
    Construction   Control       Type
    ------------   -----------   -----------
    #Recv        — receive
    #Process     — spawn
    #Case        — case
    #Vector                    — tuple
    #List                      — list
    #Atom                      — atom
    #Integer                   — integer
    #Port                      — port 
    #Binary                    — binary

Что касается функций, то все (ко)индуктивные типы будут закодированы через Берардуччи, поэтому fun эрланг типа тут нет. В EXE есть всего две конструкции: enum (зависимые индуктивные) и record (зависимые коиндуктивные). Просто функции такого понятия нет. Т.е. как в JVM/CLR все в клас обернуто, в Cardeli все это расписано. Чуть позже выложу описание типов и прелюдию EXE.

И если скажем заменить Morte на более расширенное ядро, в котором произведение присуствует как аксиома в ядре, то индуктивный тип Prod можно будет компилировать в эту аксиому. Т.е. различные аксиоматические уровни прувабл стека сшиваются через индуктивные типы, как естественный интерфейс взамодействия. Кроме того, например List и Nat (их их библиотеки полиморфных функций, естественных преобразований) будучи индуктивными, будут в таргет языке подменятся на соответсвующие примитивы Erlang. Существуют другие способы "сшивания" различных аксиоматических уровней, например можно доказывать, что семантики двух языков совпадают, это вообще отдельная тема для исследования. Мне кажется способ оборачивать аксиомы нижнего уровня в индуктивные конструкции верхнего уровня это отличная идея.

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

Единственное, что остается открытым — это сертификация виртуальной машины LING. Она специально была написана в 60K LOC, чтобы ее можно было легко прогнать через какой-то сертифицированный C компилятор. Однопроцессорность LING здесь как раз ключевое превосходство над BEAM: сертифицировать BEAM в этом смысле тот еще ад. Есть кто в ЖЖ специализирующийся на сертификации виртуальных машин написаных на С с ASM вставками? Хочется, что-то типа CMinor или типа такого. Только не как в seL4, там как раз на Isabell доказывали изоморфность сертифицированной и не сертифицированной имплементации. Или просто переписать LING на чем-то более подходящим для прувабл стека.
buka

Чистоплюи

Сука думал уйти из ЖЖ, но по производственной необходимости нужно его вести, ЖЖ это мой рабочий журнал. Хороший мощный пост был предыдущий. Искренний, открытый. Иногда я думаю, что друзья у меня есть, но на самом деле их как и всего остального не сущетсвует. Хотлинкаете мои посты с матами, а потом просите меня быть миленьким :-) Сука один дибил думает, что ИИ на SQL напишут, второй блядь интегратор за 100 штук не может систему собрать в Санта Кларе ебучей. Я таких неудачников на каждой конференции вижу, Basho, Erlang Solutions и другие. Все когда-то были невйебенные канторами, а теперь на суппорте сидят и логотипы подрисовывают поменьше, чтобы не выйобываться. Все такие крутые были, где вы счас в ЖЖ пасетесь в каментах. Что тут нового в ЖЖ можно увидеть, что вы можете мне нового сказать? Шизопараноидальный ритм которые вы выбиваете из страха, чтобы система ваших ценнойстей не пошатнулась. Вы как испуганные дети продолжаете расставлять скобочки руками и нежно лилеете вашу мифологию, вместо того чтобы сменить язык и семантику. Да я гопник и не стесняюсь этого, кому не нравятся маты нехуй меня репостить. Кто ко мне по доброму к тому и я подоброму, кто с хуйней — я за словом в карман не полезу. Вот мое истинное лицо, если кто забыл как я без бороды выгляжу:


Фото © wizzard0

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

Пост для ivan_gandhi.
buka

Почему меня не интересуют Деньги, Женщины, Дети и Программирование

Дети

Моя тринадцатилетняя (13) дочь в прошлом году на https://www.hackerrank.com выиграла (40% решенных задач) подарочный стодолларовый сертификат на сервисы Amazon в контесте CounterCode 2015 (раздел Алгоритмы) в котором принимало участие 3035 человек. Сабмитила на Python, но Erlang уже тоже знает, просто не так лихо на нем пишет как на Питоне. Спасибо учителю Сергей Савчук, который и меня учил программированию в свое время. Что сказать, моя дочь полностью готова управлять кухонными биороботами в неотвратимом приближающемся дыхании технологической сингулярности. При этом я ребенку прочитал всего 2 лекции и Сергей прочитал курс питона (незнаю сколько лекций, но думаю не больше 10). Хотите иметь умных детей? Не пичкайте их своей хуйней и вообще не интересуйтесь ими, любите просто детей, хотя бы на расстоянии.

Женщины

Женщина как просветление, ей нельзя интересоваться. Эта фея приходит внезапно и ебашит так, что вся ваша жизнь переворачивается с ног на голову, приближение к ней убивает в вас мозг и может полностью лишить вас жизненных сил, разрушительная энергия торнадо — вот, что такое настоящая женщина! Спокойный вихрь — это женщина-муза, которая ласкает и поощряет все ваши милые нелепости, которые вы считаете самым важным делом своей жизни по глупейшей наивности. Она как учитель смотрит на вас как на дурачка и щекочет ваше самолюбие своим одобрением. Если женщина вас не сводит с ума или не одобряет, то это вообще скорее всего не ваша женщина. А если вы с ней сблизились до того, что живете под одной крышей, то вообще можете скатиться в бытовуху. Бытовуха съедает слабых и даже торнадо и муз жрет безжалостная сука. Поэтому поменьше интересуйтесь своими женщинами. Куда они выходят ночью, и кому докладывают о вас. Женщина — это дакини, просветленный ум учителя. С ней можно только слиться. Это все равно что "интересоваться" Дхармакаей. Это пространство за пределами мышления. Если вы думаете иначе, вы хуй шо поняли про женщин.

Программирование

Тот кто интерсуется программированием — тот жалок. Интересоваться нужно математикой, теориями, структурами, идеями. Какой интерс кодировать на чужом языке, то, что уже предстало в своей полной красе перед твоим взором? Это ужасно нудно и это просто работа. Да она иногда нравится, но тут нечем интерсоваться. Когда я полностью увидел програму я просто сажусь ее писать, тут чисто техническая задача. Иногда конечно хочеться руками и HTML поправить, но это не программирование, как вам рассказали на курсках по JavaScript в вашем йобаном совковом ПТУ.

Деньги

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