?

Log in

Иномировой агент

Recent Entries

You are viewing the most recent 50 entries.

6th May 2016

12:16: Командировочное
С 15 по 28 мая буду в Нью-Йорке. Вообще по рабочим делам — но 25-го схожу, наконец, в "Мет". Что на выходных буду делать — пока не решил.

20th April 2016

12:25: Акционное
А кто знает, можно ли купить какие-то акции в эрэфии, а потом продать их в нормальной стране? Чтобы не тащить крупные суммы через границу и не светить зарубежный счёт?

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

7th April 2016

15:27: Ленивое
У нас на работе до недавнего времени использовали таск-трекер Trello. Сейчас переключаемся потихоньку на Asana; с этим делом я мало знаком, но отвращения не вызывает. Слава богу, не Rally.

Ну и я себе тоже завёл парочку борд в Trello, чтобы собственные планы расписывать. Так вот. Есть некоторое количество вещей, которые я намерен сделать... когда-нибудь. Или нет. Я их свалил в одну борду, которой некоторое время придумывал название.

Назвал "Ленивое почёсывание".

29th March 2016

17:29: Лекарственное
Если вы заболели, то нужно принимать лекарства, помогающие от вашей болезни.

Конечно, вокруг этого, довольно тривиального, утверждения тоже ведутся споры. Есть сумасшедшие, которые не будут принимать лекарства никогда и ни за что. Но в целом, мне кажется, оно достаточно верно. Даже если вы выздоравливаете, болезнь почти прошла, лечение прекращать не надо.

Другое утверждение: если вы здоровы, то принимать лекарства не надо. Это утверждение не настолько верно. Прививки — штука полезная. Да и витаминку съесть порой вполне можно. Однако в целом, всё-таки, лекарства сами по себе, для здорового человека, вредны.

Святой Августин сказал "Omnis civitas corpus est". "Всякое общество есть тело". Что нужно для существования этого тела? Хорошее здоровье.

Применяя всю эту теорию получаем, в первом приближении, что здоровому обществу лекарства не нужны, а больному (и даже выздоравливающему) — необходимы. Какие лекарства? Зависит от болезни, разумеется.

К чему я веду? К тому, что обществу, больному расизмом (и даже выздоравливающему, как сказано выше), нужны лекарства под названием "affirmative action". Обществу, больному гомофобией (опять же, даже выздоравливающему), необходимы лекарства под названием "гей-парады". Да, и то, и другое вызывает некоторое раздражение (у любого лекарства есть побочные эффекты). Но, судя по результатам, достигнутым одним из пациентов, помогает. Да, это немного, но... пациентов всего-то пара сотен, даже меньше, причём у многих из них есть гораздо более серьёзные проблемы. Работаем с тем, что есть.

26th February 2016

11:15: СУПоводческое
В СУПе явно сидят полные уроды. В половине журналов не показываются комменты. Причём я посмотрел JS — не понимаю, как такое могло получиться случайно. Пока решил проблему установкой GreaseMonkey и такого скрипта:
// ==UserScript==
// @name        LJ
// @namespace   migmit
// @include     *.livejournal.com/*
// @version     1
// @grant       none
// ==/UserScript==
window.show = function(){}
window.unshow = function(){}

Вроде, теперь работает.

Кроме того, ссылки на форму создания нового поста тоже нигде нет. Решается установкой закладки на http://www.livejournal.com/update.bml .

Update ( exler подсказал): похоже, фишка в том, что эти суки удалили тему XColibur. Если её поменять на Horizon, то всё начинает работать. Другой вопрос, что смотрится этот Horizon отвратно по сравнению с.

31st January 2016

12:28: Падучее
Уже в нескольких местах рассказывал одну и ту же байку. Надо бы оформить постом, и потом только ссылку давать.

Итак. Года два-три назад писал я на Эрланге. И вот возник один баг: некий процесс, скажем, Игрек, через некоторое время после запуска вдруг падает. Причём, скотина, падает даже без каких-либо сообщений в логах. А так как занят он довольно важным делом — теряется куча информации. Соответственно, релиз пришлось откатить (то ещё удовольствие) и начать разбираться.

Как оказалось, падает Игрек только под нагрузкой, так что скормить ему какие-то простенькие входные данные и аккуратно отследить, где именно его скрючит, не представляется возможным. Добавленные во все мыслимые места логи показывают, что падает процесс, в общем-то, где попало. Точнее не совсем где попало, в некоей небольшой области, но не в строго определённом месте. Я поначалу грешил на оптимизатор (случалось сталкиваться с тем, что лог выведен, а предыдущая строчка таки не выполнилась из-за того, что процесс упал), но потом понял, что наш случай таки выходит за пределы бардака, который может устроить оптимизатор. А самое смешное, что, судя по логам git, ни сам Игрек, ни вообще что-либо в непосредственной близости от него, никто не трогал уже несколько месяцев. С чего он вдруг падать начал?

Что оказалось в итоге. Был некий другой процесс, скажем, Ипсилон. И он-то как раз занимался совершенно простенькой деятельностью; он принимал сообщение, смотрел, куда его сунуть, и отсылал дальше. Причём он дожидался ответа от конечного получателя ("ага, получили, спасибо"), но сам никакого ответа отправителю не возвращал. Реализован он был через gen_server, но реально никакого внутреннего состояния там не было; если точнее, внутреннее состояние всегда оставалось [].

Но какой-то гений, который его писал (я уже не помню, кто это был) слегка ошибся. Если кто не знает, то gen_server требует, чтобы в сервере была реализована функция handle_cast, которая, собственно, и решает, как именно следует реагировать на поступившее сообщение. Бизнес-логику реализует, если угодно. Так вот, эта функция должна была бы возвращать {noreply, []} (говоря тем самым "ответа не будет, новое состояние []"), но вместо этого возвращала {ok, []}. Нарушение типизации такое, ага.

gen_server такого ответа не понимает. Ну, тупой он, не знает, что ok — значит, типа, всё здорово, давай дальше в том же духе. Поэтому, по завершении handle_cast, он, в полном соответствии с идеологией Erlang "let it crash" (т.е., "гори оно огнём") падает. Но дальше, опять-таки в полном соответствии с упомянутой идеологией, в дело включается супервизор. Который видит, что Ипсилон упал — и перезапускает его. А так как состояния у Ипсилона нет — всё работает как и должно. Вместо того, чтобы сидеть и дожидаться нового сообщения, Ипсилон падает, стартует заново, и дальше сидит и ждёт нового сообщения. И так оно работало не то чтобы месяцами — годами.

И вот что изменилось: сам Ипсилон мы тоже не трогали — а вот в одном из конечных получателей кое-что таки подкрутили и пооптимизировали. В результате ответ Ипсилону стал приходить гораздо быстрее. И Ипсилон стал, в результате, работать быстрее. А так как его работа — это постоянные падения, то и падать он стал чаще. Если под нагрузкой, конечно; когда приходит одно сообщение в час, то он и падать будет раз в час.

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

27th January 2016

13:08: Техподдержечное
Мы сейчас на работе делаем один побочный проект — в общем, часть нашего контента пихаем на фейсбук.

Контент мы представляем в виде более-менее HTML, и нам нужно, чтобы фейсбук посмотрел на этот контент и сказал "OK". Естественно, у них там кое-какие замечания, мы их исправляем; порой нам тоже не нравится, как выглядит опубликованный контент, и мы немножко его меняем. Рабочий процесс.

И вот, кто-то заметил, что цитаты (<blockquote>) выглядят не очень-то здорово: между абзацами (<p>) в них нет интервалов. Некрасиво.

Понятно, что это — проблема оформления, а не содержания. Будь это наш сайт, мы бы поправили стилевые правила, и контент вообще не трогали бы. Но это фейсбук; доступа к стилям у нас почти нет.

Я обратился к их техподдержке: что нам делать? Вскоре пришёл ответ: вставьте между абзацами <br> (насильственный перевод строки).

На этом месте и я и мои коллеги нервно сглотнули. Проблему оформления предлагается решать изменением содержания? Ладно, я добавил соответствующий код. Упс — не помогает.

Я снова в техподдержку: ребята, ваш ответ, во-первых, дурацкий, а во-вторых не работает. От них приходит новый совет, причём от того же "консультанта": вставьте ДВА <br>.

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

Через некоторое время приходит очередная пачка замечаний от фейсбука по поводу нашего контента. Среди них такой: у вас в тексте слишком много <br>.

Разработчики ругаются в голос. Я переоткрываю вопрос и пишу: ребята, вы там вообще определитесь, куда двигаться?

Окончательный ответ: "тогда заткнитесь и привыкайте жить без интервалов". И вопрос снова закрыт.

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

21st January 2016

14:36: Уголовное
Пишут, что, простите, обмудсмен Астахов предлагает в целях профилактики водить детей на экскурсии в СИЗО.

Ну, это ладно; это, естественно, никуда не пройдёт. А вот в конце заметки любопытное:

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

Гм. То есть, если вы засняли на телефон, как вашего соседа избивают менты, то выложить на youtube это дело вы уже не сможете. Точнее, сможете, но в итоге сядете. Вот это — имеет все шансы превратиться в закон.

13th January 2016

16:32: Психологическое
Посмотрел в википедии статью про эффект Даннинга-Крюгера (чтобы выяснить, как именно пишутся фамилии; остальное я и так знаю). Обнаружил там замечательную байку: некий МакАртур Уилер ограбил несколько банков, перед ограблением натирая себе лицо лимонным соком. Поскольку лимонный сок можно использовать как невидимые чернила, он решил, что на видеокамерах его физиономия отображаться не будет.

Нет, то есть, теоретически я знаю, что 99% людей на планете — полные идиоты, но конкретные проявления этого факта меня до сих пор поражают.

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

12th January 2016

11:16: Годовщина
Ну вот, уже год, как я живу в Венгрии.

Что произошло за это время? Ну, не сказать, чтобы многое.

Съездил на пару конференций. Одна дурацкая (Joy of Coding — но с этой паршивой овцы получилась футболка с надписью "I've seen JC"), одна отличная (CodeMesh). Раньше по конференциям не шастал вообще, я уж молчу о том, чтобы ездить по ним за счёт фирмы.

Занялся экстремальным туризмом — скатался в эрэфию несколько раз.

Впервые нанял адвоката.

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

Впервые въехал в Шенген не по визе.

Видел сирийских беженцев. На расстоянии вытянутой руки.

Побывал в Венской опере.

Начал составлять бюджет — на месяц и на год. Кстати, бездефицитный. Поискал приложения для этого; в конце концов остановился на текстовом файле.

Начал носить часы.

В общем — жизнь идёт.

10th January 2016

23:21: Последовательное
Тут уже почти все интернеты обошла история некоей мадам из, кажется, Ялты, которая была всей душой за покражу Крыма, состояла в ПЖиВ, а затем поехала в Херсон оформлять украинский загран, чтобы получить визу в США (ибо крымчанам в эрэфовские паспорта американцы визу не ставят). И куча народу изумляется — ах, боже мой, какое лицемерие.

А вот по-моему чего-чего, а лицемерия нет и в помине. То есть, да, поддержка оккупантов выдаёт в человеке в лучшем случае полного идиота. Но почему, собственно, не получить ничего не значащую бумажку, если в результате могут случиться вполне реальные и серьёзные ништяки? Она ж не жить на Украину переезжает.

30th November 2015

11:57: Свободное
Как обычно, навеяло недавними дискуссиями.

Есть такая часто цитируемая фраза Франклина: "Тот, кто жертвует свободой в пользу безопасности, не достоин ни свободы, ни безопасности". См. историческую справку в конце поста.

Так вот, это полная чушь. Нет подобной дихотомии. Я утверждаю, что:
1) Не бывает свободы без безопасности;
2) Не бывает безопасности без свободы.
Конечно, процентное соотношение может "гулять", но в целом эти два понятия ходят рука об руку.

Почему?

1) Что такое свобода? На этом понятии оттоптались все, кому не лень, включая ублюдка Энгельса с его "осознанной необходимостью" (впрочем, говорят, что и де Спиноза к этому приложил руку).

Не претендуя на абсолютную точность определения, всё же скажу, что "свобода" — это возможность выбора. Возможность совершать нелогичные поступки, сообразуясь со своим желанием, а не с потребностями.

"Вы говорите: я не свободен. А я поднял и опустил руку." Тот, кто может поднять руку (а может и не поднимать) — более свободен, чем тот, у кого руки связаны.

Тот, кто может поехать на какие-нибудь Мальдивы (а может и не ехать) — более свободен, чем тот, у кого слишком мало денег, так что ему остаётся только Египет Турция да что ж такое, блин Крым (нет, это уж слишком) сарай в пригороде.

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

2) Наоборот, человек, не имеющий свободы, не имеет и безопасности. Теоретически возможно представить себе государство, регламентирующее каждый шаг своих граждан, но зато гарантирующее им безопасность. Практически попытка воплотить это дело в жизнь порождает НКВД и десять миллионов доносов.

Если я совершенно не свободен — это означает, что другие могут сделать со мной что им угодно. О какой безопасности можно вести речь?

Так что вот. В некотором смысле цитата права — но только в том, что "тот, кто отказывается от одного в пользу другого не получит ничего".

Историческая справка
Франклин этой фразы не произносил (и не писал). На самом деле он писал вот что: "Тот, кто жертвует СУЩЕСТВЕННОЙ свободой ради НЕЗНАЧИТЕЛЬНОЙ ВРЕМЕННОЙ безопасности, не достоин ни свободы, ни безопасности". У него "свобода" и "безопасность" НЕ противопоставлены; напротив, они почти идентичны: "свобода" в данном контексте означала "возможность обороняться от индейцев", а "безопасность" — собственно, "безопасность от индейцев". Противопоставлены у Франклина "существенность" и "незначительность" (вместе со "временностью"). Там кипеш шёл, насколько я понимаю, вокруг того, следует ли тратить много денег на закупки оружия, или немного денег чтобы откупиться.

23rd November 2015

17:14: Аббревиатурное
Навеяно комментами у avmalgin.

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

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

И равным образом такой человек — русскоговорящий с рождения — не может не знать сокращение "СССР". Или "КГБ". Это не просто часть языка, это часть культуры, с этим языком связанной. Это книги, фильмы, статьи, всё, что угодно. Эти аббревиатуры не нужно расшифровывать "при первом использовании", как по ГОСТу.

И мне кажется, что аббревиатуры "СТО" и "ОТО" очень близко к этому культурному слою.

Как полагаете?

6th November 2015

13:20: CodeMesh
Я вернулся. Запишу кое-какие впечатления, для памяти.

Конференция была на порядок круче, чем недавняя JoyOfCoding. Хорошая организация, много интересных докладов. Я завёл несколько новых знакомых; самое интересное знакомство — со Стефани Вайрих (или Уэйрич, я не знаю, как произносить её фамилию, по-немецки или по-английски), которая делала доклад про Dependent types in Haskell.

По пунктам.

День 0: Tutorials.
1) Building Web Services in Haskell! - Allele Dev
Отстой. Содержание доклада — веб-сервис на фреймворке Spock, который на базовом уровне не отличается от Happstack. Подача — докладчик три с половиной часа бубнит себе под нос возле экрана. Напомню, это tutorial — то есть, аудитория тоже должна что-то сделать, своими руками. Нифига. Я в конце концов стал читать книжку с flibusta.me.

По-видимому, надо было пойти на Concatenative Programming - William E. Byrd & Rob Martin.

2) Getting started with Elm - Evan Czaplicki
А вот это было здорово. Эван, как оказалось, работает в венгерской Prezi, куда я пытался интервьюироваться (неудачно). Тут были и hands-on, и юмор, и общение с аудиторией (вплоть до того, что аудитория голосованием решала, чем заниматься дальше). И Elm — интересная штука, своего рода Haskell, но с компиляцией в JS. Плюс собственный веб-сервер для дебага. Плюс time-travelling debugger (можно посмотреть всё, что происходило раньше). Плюс интеграция с внешним JS. В общем, вкусно.

Одна забавная вещь. В Elm нет тайпклассов (что, ИМХО, хорошо), но ограничивать полиморфизм как-то надо (OCaml-овское полиморфное сравнение — это бомба замедленного действия), так что чуть-чуть тайпклассов всё-таки есть: если имя переменной типа начинается с, например, comparable, то это как если бы к ней был контекст Ord. Свои тайпклассы делать нельзя, свои инстансы тоже.

День 1.
1) Keynote: Grace Murray Hopper: The Original Pirate Hacker - Melissa Pierce
Снова отстой. Больше феминистического активизма, чем чего-то интересного.

То, что Пирс очень похожа на Фредерику Лаундс из сериала "Ганнибал", причём и внешне и по голосу, не добавляет интереса.

2) The Road to Running Haskell at Facebook Scale - Jon Coens
Sales pitch. Неплохой, надо признать. Не думал, что Хаскель настолько "готов для десктопапродакшена". А у них реально хаскельные продукты обрабатывают миллионы запросов в секунду.

Ложка дёгтя: у них, всё-таки, работает Саймон Марлоу. Интересно, далеко ли они уехали бы без него?

3) CRDTs in Practice - Marc Shapiro, Nuno Preguiça
М-м-м... странно.

Они пытаются выполнять определённые операции асинхронно, ни разу не останавливая процессинг для синхронизации, а только обмениваясь данными. Это всё хорошо, но вот пример, который они показали, вызвал у меня устойчивые ассоциации с Operational Transformation. Когда я задал вопрос, Шапиро сказал, что единственная связь между их подходом и OT в том, что они рассматривают OT как пример "как не надо делать". Но выглядит всё равно очень похоже; у меня ощущение, что они разбили OT на части и запрятали их в разные места. Доказать не могу, это чисто ощущение, и больше ничего.

Возможно, дело в том, что OT я реализовывал в процессе трудоустройства в JetBrains (прерванный по моей инициативе), и это такой молоток, из-за которого мне всё кажется моими пальцами. Надо ещё почитать и подумать.

4) From Irrational Configuration System to Functional Data Store — Rob Martin
Ничего интересного. Что-то вроде отчёта о проделанной работе. Плюс у Мартина явно паттерн-ориентированное мышление.

Впрочем, ничего более интересного в это время не было.

5) Function-Passing, A New Model for Typed, Asynchronous and Distributed Programming - Heather Miller
Идея достаточно любопытная, чтобы не задумываться о возможных применениях. Миллер, кстати, сама сказала, что это pet project, и не факт, что из этого что-то выйдет.

Фишка в том, что вводится новая монада (хотя Миллер не произнесла это слово), но не в категории типов, а в её подкатегории, где морфизмами являются сериализуемые функции. То есть, функция сама по себе чистая, и всё, что она замыкает, обязано быть сериализуемым. Тогда можно хранить данные на разных нодах — причём данные уже могут быть не сериализуемыми. fmap понимается просто как передача функции туда, где лежат данные, и применение там (ленивое). (>>=) чуть сложнее, но, в общем, та же фигня. Реально интересно.

6) Accidentally Concurrent - Evan Czaplicki
И опять Эван. Он начал с того, что замоделировал мутабельную переменную как процесс (в стиле pi-calculus), после чего убеждал народ, что мутабельность — плохо, потому что в результате мы получаем разветвлённую сеть параллельных процессов, в которой сам чёрт ногу сломит, и всё влияет на всё. Он был прав, и опять забавен, пусть даже и не сообщил ничего реально нового.

7) Coordination-Free Designs for Mobile Gaming - Christopher Meiklejohn
Э-э-э... вообще не помню, о чём он говорил. Кажется, это опять был "отчёт о проделанной работе". Скучно.

8) Keynote: Propositions as Types - Philip Wadler
Старая гвардия. Лямбда-мэн рассказывал об истории, поминал Чёрча, Гёделя, Тьюринга и прочих, рассказывал анекдоты (как Гёдель придумал своё определение алгоритма в пику Чёрчу, Чёрч доказал, что их определения эквиваленты, сказал Гёделю: "вот, подавись", на что Гёдель ответил "ну, значит, моё определение неправильное"). Весело, и отлично подходит для полуфинала.

День 2.
1) Keynote: Why Functional Programming Matters - John Hughes Mary Sheeran
Хьюджеса я уже видел, на приснопамятной JoyOfCoding — он тогда всех веселил. На этот раз веселил всех Вадлер, а Хьюджес говорил довольно мало. Большую часть времени говорила Ширан, и это было скучно. Из её слов стало понятно, что функциональное программирование — это круто, потому что мы не знаем, сколько компараторов нужно, чтобы отсортировать 32 числа.

2) Beyonds Lists: High Performance Data Structures - Phil Trelford
Правильнее было назвать "Data Structures 101". Юзайте, дети, B+-деревья, и ваши волосы будут мягкими и шелковистыми.

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

3) Transactions: Myths, Surprises and Opportunities - Martin Kleppmann
Реально круто. Клеппманн говорил о том, какие гарантии предоставляет механизм транзакций в известных СУБД. Я не знал, что всё настолько плохо.

4) FRP and Functional Game Programming - Elise Huard
Ниачём. Возьмите любую вводную статью по FRP, косноязычно перескажите середину, и вот оно.

Вроде, ничего приличного в это время не было.

5) Depending on Types - Stephanie Weirich
Миленько. По сути, то же самое, что я показывал здесь, только не про списки, а про RB-деревья. А вот вторую часть мы с ней сейчас обсуждаем в почте.

6) Into Production - Jamie Winsor
Опять отчёт о проделанной работе, но несколько более занятный. Не знаю, может, я просто много кофе выпил.

7) My Little Pony - Darach Ennis, Sylvan Clebsch
Рассказывали о языке Pony. Много и хорошо шутили, потратили почти всё время на объяснение базового синтаксиса, после чего реально содержательную часть (разные виды ссылок) за недостатком времени скомкали до полной невозможности. Кстати, введения в Pony, которые мне случалось видеть, грешат тем же. Так и не узнал, насколько же этот язык крут.

8) Panel Discussion - Joe Armstrong, Don Syme, Bruce Tate, Josh Watzman, Tony Hoare
И опять на закуску старая гвардия. Веселее всех был Хоар, который повторил своё общеизвестное признание про "ошибку ценой в миллиард долларов", уточнив "миллиард долларов в год" и добавив, что это ОЧЕНЬ оптимистическая оценка.

Резюме. Из 18 выступлений разного сорта было 4 однозначно полезных, одно весьма спорное, 4 просто забавных, и всего пара-тройка откровенно дурацких.

23rd October 2015

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

Так вот, со 2 по 4 ноября я буду на конференции CodeMesh в Лондоне. Как и в прошлый раз, программа выглядит очень интересно.

Вообще, надо бы прояснить один момент. В нашей конторе на каждого сотрудника выделяется три тонны зелёных президентов в год, которые он имеет право тратить на конференции по своему выбору. Оплачиваются: участие в конференции, проживание, транспорт (главное — уложиться в бюджет). Не оплачиваются: визовые сборы, питание, ну и вообще всё, что не входит в список "оплачиваются". Имеется список конференций — не знаю, что будет, если выбрать конференцию, в список не входящую. По моим личным впечатлениям, её просто добавят в список — но я пока не пробовал.

19th October 2015

12:42: Идиотское-2
В очередной раз убеждаюсь, что количество разума на планете — величина постоянная.

Прислали мне ссылку на некую статью, касающуюся отчёта голландских следователей о сбитом "Боинге". Оттуда я вышел на оригинал статьи — он же пост в ЖЖ. Там было перечислено несколько пунктов, первый из которых звучал так:

Это, к сожалению, ошибка, возникшая при переводе с голландского на английский. Её уже обсосали со всех сторон, поэтому вскоре в том же посте появилось дополнение. Удивительным образом это "дополнение" одновременно и признаёт ошибку, и старается её нивелировать:

Пассаж о "surgical clips" меня заинтересовал. Я забил это дело в гугль и выяснил, что surgical clips — это, по сути, скрепки, которые при некоторых операциях очень часто оставляются в теле, не причиняя вреда. Не знаю, чувствуют ли их металлодетекторы в аэропортах, но на рентгене они очень чётко видны.

Я написал об этом, а потом ещё посмотрел, куда ведёт ссылка на "поправку", якобы опубликованную The Guardian, и добавил пояснение на эту тему:

На этом месте мне уже стоило бы сообразить, что, когда человек так много внимания уделяет форме, в ущерб содержанию, то это "ЖЖЖЖ" неспроста.

Вторым звонком стало исчезновение последнего коммента, который со ссылками. Он просто взял — и исчез.

Дальше пошло веселеее.

Мне немножко странно, когда человек сначала спрашивает "вы уверены?", а потом говорит "да наплевать, с чего вы уверены". Однако, я предложил приемлемые для меня условия пари. Они не были приняты, а мой аккаунт забанен. И, естественно, по существу никаких возражений не появилось. Я слегка озлился и ответил через Facebook:


Собственно, вот. Оставляю, дабы глупость каждого видна была.

Update: Чуть не забыл упомянуть: скриншоты сделаны системой http://www.sciweavers.org/free-online-web-to-image — я только вырезал из них нужное.

15th September 2015

20:54: Идиотское
Один довольно популярный жужист выложил вот эту картинку:



У меня возник, как мне казалось, довольно логичный вопрос: а какие услуги рекламируются, если по-серьёзному? Полагая, что человек, выложивший это, вероятно, знает больше меня, я задал вопрос. Дальше получилось забавно:



Последнее он удалил.

Кстати, никто не знает, что именно рекламируется?

9th September 2015

11:10: Текстологическое
Люди в интернете, в основном, пишут тексты. Есть, конечно, те, кто выкладывает исключительно фотографии без подписей, но таких довольно мало. ИМХО.

Тексты бывают разные. Есть тексты шуточные (как, например, такой: http://pipokipp.livejournal.com/44735.html) — а в шутке, мне кажется, допустимо вообще практически всё. Шутка может оказаться плохой, но это уже мелкие детали.

Есть тексты, передающие чью-то прямую речь. Тут тоже понятно, из песни слова не выкинешь, разве что можно "запикать" нецензурщину.

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

Например, если вы написали: "вместе с беженцами в Европу пролезут боевики ИГИЛ", то дальше у нас с вами есть повод для разговора — ну, если вы не против, конечно. Мы можем обсудить, насколько серьёзна эта угроза, насколько эффективны действия немецкой или австрийской полиции, и прочая, и прочая.

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

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

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

Если вы пишете: "загнать этих чурок за колючую проволоку, пусть там интегрируются", то, опять же, у нас нет повода для разговора.

Как-то так.

8th September 2015

18:47: Беженское
Мне тут стали говорить, что в Будапеште — где я живу — сплошной кошмар, сирийские беженцы чуть ли не уличные бои устраивают, и вообще Венгрия скоро гикнется, а за ней и вся Европа.

Так что я в воскресенье собрался и съездил-таки на Восточный вокзал (то бишь, Келети), где как раз основное место кучкования этих самых беженцев. Read more...Collapse )

24th August 2015

14:32: Архивное
Всё-таки вебархив — замечательная штука. Вот посмотришь в статью — и не находишь, к чему придраться. Ну, на первый взгляд, по крайней мере.

А смотришь то же самое на вебархиве всего-то за позавчерашний день (за вчерашний нету) — и сразу видишь, где оне проговорились:
Также, Правительством России было принято важное решение о денежной компенсации военнослужащим, принимавшим участие в военных действиях на востоке Украины.

30th July 2015

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

Покупая Apple Watch, я специально думал о том, что так делать не буду (гм... второй пост подряд. Ну да ладно). Так вот: люди, которые так поступают — полные идиоты. Потому что когда раз в два-три дня кто-нибудь из коллег замечает у тебя на руке эти часы и говорит "вау, да у тебя Apple Watch" — после чего, разумеется, можно тут же рассказать ему все подробности, ибо сам напросился — это гораздо приятнее, чем в первый же день рассказать всем, а потом сосать лапу.

25th July 2015

23:11: Не прошло и года
...и я таки понял, что был неправ.

Конкретно это вот про этот пост: http://migmit.livejournal.com/55397.html

То есть, нет, частично я был прав — я попробовал iPhone 6 (без плюса) в магазине и понял, что пользоваться им не могу. Но вот по поводу часов я таки ошибался.

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

Модель взял маленькую — у меня тонкие кисти, так что большая смотрелась на руке странно (да, я померил обе).

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

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

Как ни странно, диктовка работает хорошо. Когда, например, меня упоминают в Trello, мне приходит на часы уведомление; при этом я могу прямо с часов надиктовать короткий ответ. Забавно, что при этом знаки препинания надо проговаривать, типа "oh comma cool exclamation point".

1Password умеет часть паролей засовывать на часы. То есть, если мне нужно, например, посмотреть номер своей карты, я могу просто запустить приложение на часах.

Батарейка живёт день. Мне вполне достаточно — ну, ещё один девайс нуждается в зарядке, большая разница. Спать в часах я всё равно не собираюсь.

Посмотрим, что принесёт watchOS 2.

2nd July 2015

20:57: Происходящее
Так, чтобы зафиксировать, что сейчас происходит.

Кто сказал "Путин"? Тьфу на вас. Не о том речь.

В общем, я сейчас работаю в компании Kinja, которая, по сути, является Будапештским офисом компании Gawker. Да-да, той самой, которая публикует всякие слухи и сплетни, называя это дело "новостями".

И есть такой товарищ по имени "Халк Хоган" (нет, нифига не настоящее). Я лично его знаю только по (убогому) сериалу "Гром в раю", который когда-то крутили по ящику и я на него иногда попадал (в то время, когда ящик был ещё не "зомбо-").

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

Подчеркну, что эту запись сделали не мы. Мы также её не украли, не заплатили кому-нибудь, чтобы он украл её для нас, и так далее. Тем не менее, Х требует от нас (теперь уже нас) 100 миллионов долларов.

У нас столько нет.

Дело будет слушаться во граде Санкт-Петербурге. !. Правда, в том, который во Флориде. Насколько я могу судить, наша основная защита — первая поправка (предупреждаю: я не юрист). Если мы проиграем, то, вероятно, контора всё-таки не закроется, но поменяет владельцев.

На текущий момент слушанье, назначенное изначально на 6 июля, перенесено на неопределённый (пока) срок — там какая-то бюрократия, я не понял точно.

16th June 2015

14:45: Доказательное, часть II
Продолжаем наши игры. Мы переходим к более интересной части: теперь мы будем не только следить за длиной списка, но и позаботимся, чтобы в конце список оказался отсортированным.

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

Первое, что приходит в голову — это каким-то образом поднять значения на уровень типов. Например, если значения — это числа, то можно представить их в виде Пеано (что мы, кстати, и делали). Или можно закодировать в типах их двоичное представление.

Сделать это всё, конечно, можно. А вот сделать это полиморфным образом — чтобы не требовать от типа ничего, кроме упорядоченности — уже нельзя. Никак. Да и вообще, это весьма сомнительный трюк. Как же тогда быть?

На помощь приходят уникальные типы. Да-да, в Хаскеле есть уникальные типы — то есть, такие типы, что в программе возможно только одно значение этого типа (ну, до тех пор, пока мы не начали использовать unsafeCoerce и тому подобные вещи). Да, все значения одного типа неотличимы — но если у типа только одно значение, то они к тому же и в рантайме будут гарантированно равны. Итак, как получить уникальный тип в Хаскеле?
> {-# LANGUAGE GADTs #-}
> module Tag(Tag(untag), Tagged(Tagged), tag) where
Наш уникальный тип — это, по сути, тот же тип, что и раньше, только с навешенным на него "тэгом" — фантомным типом.
> newtype Tag t a = Tag {untag :: a}
Что же делает его уникальным? То, что конструктор Tag мы не экспортируем. Только сам тип и функцию untag. Поэтому, если мы каким-то образом обеспечим возможность создать значение данного типа, но только одно — то наша задача выполнена. Все значения такого типа, созданные вне данного модуля, будут равны.

Чтобы это сделать, мы воспользуемся всё теми же GADT-ами. Именно, мы спрячем этот самый "тэг" под экзистеншиал:
> data Tagged a where Tagged :: Tag t a -> Tagged a
Теперь мы не будем создавать сам Tag t a, мы будем создавать Tagged a:
> tag :: a -> Tagged a
> tag a = Tagged (Tag a)
Таким образом, мы можем создать кучу значений типа Tagged a — но, распаковав их с помощью паттерн-матчинга, мы получим значения типов Tag t a с разными t. То есть, мы можем создать кучу "тэгированных" значений, несущих внутри себя одно и то же a — но сами по себе они будут разных типов. Мы даже не сможем сравнить их на равенство: равенство действует только в пределах одного типа.

И как же это поможет нам со сравнениями? А вот как. Мы не можем сделать тип 3 < 5 — так как 3 и 5 это значения, а не типы. Но если есть уникальный тип, содержаший значение 3 с тэгом t, и уникальный тип, содержащий значение 5 с тэгом s, мы вполне можем соорудить тип t < s.

Однако, можно также образовать и тип s < t. Как мы гарантируем, что это не происходит? Точно так же, как и в случае тэгов: экспортируя не конструктор, а функцию, проверяющую неравенство.
> {-# LANGUAGE GADTs, TypeOperators #-}
> module Ord(
>   (:=), refl, symm, eTrans,
>   (:<), (:>), mirrorLG, mirrorGL, lTrans, gTrans,
>   Comparison(..), comparison
>   ) where
> import Tag
Но для начала, прежде чем заняться неравенствами, мы займёмся равенствами.
> data t := s = Equal
Напомню, что мы сравниваем тэги, а не сами значения.

Равенство будет, как обычно, рефлексивными, симметричным, и транзитивным. Ничего из этого нам не понадобится, но для полноты картины пусть будет. Кстати, рефлексивность можно интерпретировать как "если есть два значения с одним тэгом, то они равны".
> refl :: t := t
> refl = Equal

> symm :: t := s -> s := t
> symm Equal = Equal

> eTrans :: t := s -> s := r -> t := r
> eTrans Equal Equal = Equal
Переходим к неравенствам. Достаточно было бы, конечно, ввести одно из них, но я введу оба, и "больше", и "меньше". С симметричными вещами проще работать.
> data t :< s = Less

> data t :> s = Greater
Заметьте, что конструкторы Less и Greater мы не экспортируем, чтобы не допустить прямого создания этих типов вне данного модуля.

Разумеется, эти отношения эквивалентны с точностью до перестановки аргументов:
> mirrorLG :: t :< s -> s :> t
> mirrorLG Less = Greater

> mirrorGL :: t :> s -> s :< t
> mirrorGL Greater = Less
Оба они транзитивны:
> lTrans :: t :< s -> s :< r -> t :< r
> lTrans Less Less = Less

> gTrans :: t :> s -> s :> r -> t :> r
> gTrans Greater Greater = Greater
Остаётся показать, как именно мы будем создавать их. Когда мы сравниваем два значения, может получиться три варианта ответа: первое больше второго, первое равно второму, первое меньше второго. Соответственно, мы введём тип для такого ответа:
> data Comparison t s = CL (t :< s) | CE (t := s) | CG (t :> s)
И, наконец, напишем функцию, которая это сравнение производит.
> comparison :: Ord a => Tag t a -> Tag s a -> Comparison t s
> comparison ta sa =
>   case compare (untag ta) (untag sa) of
>    LT -> CL Less
>    EQ -> CE Equal
>    GT -> CG Greater
Отмечу одно обстоятельство. Мы используем здесь класс Ord, инстанс которого может быть написан неправильно. Например, сравнение может быть нетранзитивным. В этом случае, используя функцию lTrans, мы можем, в принципе, выразить в типах неверное сравнение. Это никак не обойти: транзитивность сравнений нам действительно будет нужна. Но, с другой стороны, если сравнение реализовано неправильно, то и QuickSort будет работать неправильно.

Итак, вся машинерия готова. Теперь со всем этим мы попробуем взлететь.
> {-# LANGUAGE GADTs, TypeOperators #-}
> module QuickSort where
> import Num
> import Ord
> import Seq
> import Tag
Вспомним ещё раз, как делается QuickSort. Для начала мы делим наш список на два, в одном — маленькие элементы, в другом — большие. При этом на сей раз за такими ограничениями мы должны следить. Значит, простой Seq нам не подойдёт, нужен другой тип, который, во-первых, имеет эти самые ограничения сверху и снизу, а, во-вторых, содержит значения вместе с тэгами, без которых мы не можем отслеживать порядок.
> data BoundedSeq l u n a where
>   ZBSeq :: BoundedSeq l u Zero a
>   SBSeq :: Tag t a -> l t -> u t -> BoundedSeq l u n a -> BoundedSeq l u (Succ n) a
То есть, мы храним не только значения с тэгами, но и свидетельства того, что эти значения удовлетворяют наложенным ограничениям.

Правда, изначально никаких ограничений нет. Поэтому нам понадобится "пустое" ограничение:
> data Whatever a = Whatever
Ну и, чтобы старый Seq переделать в новый BoundedSeq, нам понадобится простенькая функция:
> fromSeq :: Seq n a -> BoundedSeq Whatever Whatever n a
> fromSeq ZSeq = ZBSeq
> fromSeq (SSeq a as) = case tag a of Tagged ta -> SBSeq ta Whatever Whatever (fromSeq as)
Далее, в списке могут случиться повторяющиеся элементы. То есть, одно из ограничений — сверху или снизу — должно быть нестрогим.
> data t :<= s = L (t :< s) | E (t := s)
Идём дальше. Что мы собираемся получить на этом первом этапе? В предыдущем варианте у нас был тип TwoSeq, специально придуманный ради этого. Не будем нарушать традиции. Единственное, что нужно добавить — это, опять-таки, ограничения сверху и снизу.
> data TwoSeq l u n t a where
>   TwoSeq
>     :: BoundedSeq l ((:>) t) m a
>     -> BoundedSeq ((:<=) t) u k a
>     -> Plus m k n
>     -> TwoSeq l u n t a
К сожалению, инфиксные операторы на уровне типов не позволяют делать секции, иначе можно было бы писать не ((:>) t), а просто (t :>).

Функция, разделяющая список на два, выглядит почти так же, как и в предыдущем случае:
> split :: Ord a => Tag t a -> BoundedSeq l u n a -> TwoSeq l u n t a
> split _ ZBSeq = TwoSeq ZBSeq ZBSeq ZPlus
> split ta (SBSeq ta' lt ut as) =
>   case split ta as of
>    TwoSeq sl sg p ->
>      case comparison ta ta' of
>       CL l -> TwoSeq sl (SBSeq ta' (L l) ut sg) (sPlus p)
>       CE e -> TwoSeq sl (SBSeq ta' (E e) ut sg) (sPlus p)
>       CG g -> TwoSeq (SBSeq ta' lt g sl) sg (SPlus p)
Единственное, о чём нужно позаботиться — это о том, чтобы аккуратно свести случаи "меньше" и "равно".

Теперь второй этап. Мы хотим получить на выходе отсортированную последовательность. Значит, нам потребуется для этого отдельный тип.
> data SortedSeq l u n a where
>   ZSSeq :: SortedSeq l u Zero a
>   SSSeq :: Tag t a -> l t -> u t -> SortedSeq ((:<=) t) u n a -> SortedSeq l u (Succ n) a
Ну и, для преобразования отсортированной последовательности в обычную, простенькая функция:
> toSeq :: SortedSeq l u n a -> Seq n a
> toSeq ZSSeq = ZSeq
> toSeq (SSSeq ta _ _ as) = SSeq (untag ta) (toSeq as)
Теперь — о функции слияния. Тут есть один занятный момент.

Мы склеиваем две последовательности. Отсортированных. Но у первой из них верхняя граница — это выбранный pivot, а не та граница, которая была у исходной, неотсортированной последовательности. Значит, нам нужно как-то скастовать одну последовательность к другой, ослабив ограничение. Для этого нам послужит такой класс:
> class Lower p where lower :: p t -> t :> s -> p s
> instance Lower Whatever where lower Whatever _ = Whatever
> instance Lower ((:>) r) where lower = gTrans
То есть, мы можем либо ослабить ограничение до пустого (Whatever), либо до какой-то большей, но всё-таки существующей, границы.

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

И вот какая функция получается. По чисто техническим причинам мне удобнее склеивать не две последовательности сами по себе, а две последовательности и pivot между ними.
> append3
>   :: Lower u => SortedSeq l ((:>) t) m a
>   -> Tag t a
>   -> l t
>   -> u t
>   -> SortedSeq ((:<=) t) u k a
>   -> Plus m (Succ k) n
>   -> SortedSeq l u n a
> append3 ZSSeq ta lt ut as2 p = uzPlus p (SSSeq ta lt ut as2)
> append3 (SSSeq ta' lt' ut' as1) ta _ ut as2 p = append3Succ ta' lt' ut' as1 ta ut as2 p

> append3Succ
>   :: Lower u => Tag t' a -> l t' -> t :> t'
>   -> SortedSeq ((:<=) t') ((:>) t) m a
>   -> Tag t a -> u t
>   -> SortedSeq ((:<=) t) u k a
>   -> Plus (Succ m) (Succ k) n
>   -> SortedSeq l u n a
> append3Succ ta' lt' tt' as1 ta ut as2 (SPlus p) =
>   SSSeq ta' lt' (lower ut tt') (append3 as1 ta (L (mirrorGL tt')) ut as2 p)
Причина появления дополнительной функции append3Succ — прежняя, иначе ghc будет ошибочно жаловаться на неполный паттерн-матчинг.

Наконец, собираем всё вместе.
> sort :: (Lower u, Ord a) => BoundedSeq l u n a -> SortedSeq l u n a
> sort ZBSeq = ZSSeq
> sort (SBSeq ta lt ut as) =
>   case split ta as of TwoSeq sl sg p -> append3 (sort sl) ta lt ut (sort sg) (sPlus p)
Что хотели — то и получили: из обычной последовательности делается отсортированная. Заметим, что тут уже не получится забыть рекурсивно отсортировать подсписки — компилятор тут же выдаст ошибку типизации.

Ну и, возвращаясь к обычным последовательностям, без ограничений, мы получаем функцию
> sortSeq :: Ord a => Seq n a -> SortedSeq Whatever Whatever n a
> sortSeq as = sort (fromSeq as)
Чтобы протестировать её, введём дополнительную функцию, сортирующую уже обычный, хаскельный список:
> sortList :: Ord a => [a] -> [a]
> sortList as = case fromList as of ESeq as' -> toList (toSeq (sortSeq as'))
Тестируем:
*QuickSort> sortList [5,1,3,2,4,1] :: [Integer]
[1,1,2,3,4,5]
14:44: Доказательное, часть I
Дошло тут до меня о великий царь, что, хотя в Haskell и нет зависимых типов, но его способности к доказательству на самом деле очень и очень велики.

Если говорить, например, об алгоритмах сортировки, то, обычно, приходит в голову две очевидных вещи:
1) Результат должен быть отсортирован, и
2) Результат должен иметь ту же длину, что и исходная последовательность.

Так вот, я раньше думал, что пункт (2) можно отследить типами, а вот пункт (1) — ни фига. Но оказывается...

Прежде, чем писать о пункте (1), я, всё-таки, займусь пунктом (2). Он, конечно, почти очевиден — во всяком случае, очевидно, что это МОЖНО сделать, — но, глядя, как он делается, мы можем лучше понять более сложный пункт (1).

Итак. Само собой, чтобы доказывать на Haskell выполнение пункта (2), нам нужно завести числа на уровне типов. Да, сейчас есть всякие promoted literals и всё такое прочее... но мы будем работать по простому. По сути, единственное расширение, которое нам понадобится по делу — это GADT-ы:
> {-# LANGUAGE GADTs #-}
Ну, для начала мы таки введём наши числа:
> module Num where

> data Zero = Zero
> data Succ n = Succ n
Один момент: почему тип Succ определён именно как data, а не newtype? Дело в том, что паттерн-матчинг для GADT-ов сделан не самым лучшим образом, и, зачастую, сыплет warning-ами на совершенно правильный и законный код. В частности, мы поймаем их, если используем здесь newtype. Этот баг известен; сначала его исправление назначили на версию 7.8.1, потом сдвинули на 7.10.1, потом — на 7.12.1, где он сейчас и висит.

Мы будем доказывать банальный QuickSort. И довольно простой, и довольно эффективный. Но, коли так, нам нужно будет соединять две последовательности в одну. А, значит, их длины — за которыми мы будем следить — складываются. Стало быть, нам нужно сложение чисел.

Операции над типами сейчас модно делать с помощью type families. Но мы, опять-таки, поработаем по старинке, чтобы не уйти в дебри undecidable instance-ов.

А по старинке — это те же GADT-ы:
> data Plus m k n where
>     ZPlus :: Plus Zero n n
>     SPlus :: Plus m k n -> Plus (Succ m) k (Succ n)
Здесь значение типа Plus m k n — это свидетельство того, что m+k=n. Ясен пень, что такое свидетельство можно подделать — например, явно указав в качестве него undefined — но всё-таки более-менее полагаться на него можно. Опять-таки, полноценных доказательств тут не будет, в Haskell каждый тип населён — но работать они помогают.

Нам понадобятся два факта про сложение. Во-первых, хотя из определения мы знаем, что, увеличивая первое слагаемое на единицу, мы увеличиваем и всю сумму, нам пока неизвестно то же самое про второе слагаемое. Вот и установим этот факт:
> sPlus :: Plus a b c -> Plus a (Succ b) (Succ c)
> sPlus ZPlus = ZPlus
> sPlus (SPlus p) = SPlus (sPlus p)
А второе, что нам потребуется — довольно технический факт: если f — произвольный тип (подходящего кайнда), то f (0 + n) — это то же самое, что f n. Практически тривиально:
> uzPlus :: Plus Zero k n -> f k a -> f n a
> uzPlus ZPlus fna = fna
Здесь я добавил ещё один аргумент a — по чисто техническим причинам; так будет удобнее впоследствии. Можно было и обойтись.

На этом с числами всё. Займёмся теперь последовательностями.
> {-# LANGUAGE GADTs #-}
> module Seq where
> import Num
Так как мы будем отслеживать длины последовательностей, нам нужно внести длину в, собственно, тип. Числа у нас уже есть, так что всё остальное просто:
> data Seq n a where
>     ZSeq :: Seq Zero a
>     SSeq :: a -> Seq n a -> Seq (Succ n) a
Чтобы иметь возможность посмотреть содержимое такой последовательности, сконвертируем её в обычный список:
> toList :: Seq n a -> [a]
> toList ZSeq = []
> toList (SSeq a as) = a : toList as
Обратный процесс — преобразование списка в такую последовательность — чуть более сложен. В списке не содержится его длина — так что на выходе должна быть последовательность произвольной длины, что означает дополнительный тип:
> data ESeq a where ESeq :: Seq n a -> ESeq a

> fromList :: [a] -> ESeq a
> fromList [] = ESeq ZSeq
> fromList (a : as) = case fromList as of ESeq as' -> ESeq (SSeq a as')
Добрались до, собственно, сортировки.
> {-# LANGUAGE GADTs #-}
> module QS where
> import Num
> import Seq
Нам надо будет разделить наш список на две части, при этом следя за их длинами. А что мы будем знать про их длины? Да то, что их сумма — это длина исходного списка. То есть, на выходе нашей "делительной" функции должно оказаться что-то вот такое:
> data TwoSeq n a where TwoSeq :: Seq m a -> Seq k a -> Plus m k n -> TwoSeq n a
Сама функция пишется проще простого: делим хвост списка, после чего добавляем первый его элемент куда нужно. Чтобы решить, куда именно — сравниваем этот самый первый элемент с выбранным зарание pivot-ом. Я специально не стану обобщать и делать деление списка по произвольному предикату, чтобы было более похоже на то, что будет происходит в следующем посте, про пункт (1).
> split :: Ord a => a -> Seq n a -> TwoSeq n a
> split _ ZSeq = TwoSeq ZSeq ZSeq ZPlus
> split a (SSeq a' as) =
>     case split a as of
>       TwoSeq sl sg p ->
>           if a' < a
>             then TwoSeq (SSeq a' sl) sg (SPlus p)
>             else TwoSeq sl (SSeq a' sg) (sPlus p)
Кроме того, такие последовательности придётся склеивать обратно. Для этого нам понадобится аналогичная функция:
> append :: Seq m a -> Seq k a -> Plus m k n -> Seq n a
> append ZSeq as2 p = uzPlus p as2
> append (SSeq a as1) as2 p = appendSucc a as1 as2 p

> appendSucc :: a -> Seq m a -> Seq k a -> Plus (Succ m) k n -> Seq n a
> appendSucc a as1 as2 (SPlus p) = SSeq a (append as1 as2 p)
Зачем понадобилась дополнительная функция appendSucc? Как и выше — чтобы избежать ошибочных warning-ов ghc по поводу "неполного паттерн-матчинга". Увы, ghc в этом месте довольно глуп, и не понимает, что, на самом деле, все остальные варианты паттерн-матчинга невозможны. Причём если их добавить, то он выдаст ошибку типизации (что правильно).

Заметим, кроме того, что в одном месте нам понадобилось использовать функцию uzPlus. По сути, вот из-за чего: мы знаем, что длина получающейся последовательности равна m+k и что n=m+k; но из этого не можем — автоматически — сделать вывод, что длина получающейся последовательности равна n. Приходится кое-где скастовать явно.

Ну и, наконец, вот она, сортировка.
> sort :: Ord a => Seq n a -> Seq n a
> sort ZSeq = ZSeq
> sort (SSeq a as) =
>     case split a as of TwoSeq sl sg p -> append (sort sl) (SSeq a (sort sg)) (sPlus p)
То, что и хотелось — длина списка на выходе гарантированно совпадает с длиной списка на входе. Алгоритм работает тривиально, пустой список выдаётся как есть, остальное делится на два подсписка, они сортируются отдельно, после чего соединяются (с pivot-ом посередине).

Здесь я должен признаться в одном упущении. Когда я писал этот алгоритм в первый раз, я забыл рекурсивно отсортировать подсписки. Получилось что-то в таком роде:
sort (SSeq a as) = case split a as of TwoSeq sl sg p -> append sl (SSeq a sg) (sPlus p)
Соответственно, результат получился хоть и нужной длины, но слегка не такой, как хотелось бы. Вот этим мы в следующем посте и займёмся.

Напоследок — функция для проверки всего этого добра:
> sortList :: Ord a => [a] -> [a]
> sortList as = case fromList as of ESeq as' -> toList (sort as')
Проверяем:
*QS> sortList [5,1,3,2,4] :: [Integer]
[1,2,3,4,5]

6th June 2015

21:45: Рифмованое
Из обращения президента Порошенко к Верховной Раде:
Найсвіжіший приклад правильного рішення: днями Мінекономіки виключило із списку обов'язкових до сертифікації на території України цілу низку імпортних товарів – від автомобілів і тракторів до дитячих візків і порцелянового посуду. Правду кажучи, сертифікації не було й раніше, просто брали хабарі. А тепер – брати не будуть: і хотіли б, а нема за що.
Из газеты Слава Севастополя:
С 1 июня 2015 года триста пятьдесят балаклавских и севастопольских предпринимателей, оплативших патенты за морские пассажироперевозки в бюджет Севастополя, регулярно с января пополняющих счета Пенсионного фонда, законопослушно оплативших услуги проверки своих катеров специалистами Российского речного регистра и Севастопольского морского порта для перерегистрации своих маломерных судов как коммерческих, работать... не будут.
...
на 26 мая 2015 года только одна компания Севастополя, ООО "Севастопольские транспортные системы", эксплуатирующая паромы по маршруту Артиллерийская бухта - Северная сторона, имеет с 1 января 2015 года государственную лицензию МР-2 N 001572 от 30 декабря 2014 года с правом осуществления морских пассажироперевозок.
Даже Севастопольский морской порт, владелец многочисленных катеров, перевозящих пассажиров на Северную сторону и Радиогорку, так и не смог на сегодняшний день получить эту вожделенную лицензию.

27th May 2015

12:18: Башкирское
Мне тут пришло в голову — а ведь, наверное, не все ещё видели этот башкирский мультик:

Это большое упущение.

26th May 2015

01:42: Извинения
Фотография со страусом, выложенная позавчера, принадлежит sonya_oreshnik. Приношу свои глубочайшие извинения, что не указал авторство сразу. Я присутствовал при её создании, но не создавал её сам. Ещё раз прошу простить.

25th May 2015

22:19: Роличное
Снова пишу пост для обозначения позиции.

ИМХО, когда Чулпан Хаматова публично говорит несколько слов в поддержку ВВБХ — при всей его мерзотности — в обмен получая возможность спасти десяток детей, она делает единственно достойный выбор.

Я сказал.

22nd May 2015

13:35: Verisimilitude
1. Вероятность, правдоподобие
2. Выдумка

Обожаю английский.

20th May 2015

22:13: Техподдержечное
У нас на работе в рассылку падают, в том числе, обращения в нашу техподдержку. Читать их порой забавно. На днях пришло вот такое вот (перевёл в меру сил):
все американские актёры и остальные тоже в огромном криминальном скандале, в котором участвуют миллиарды очень важных персон ресторан мадео в беверли хиллз калифорния и прочие , такие как дэвид хассельхоф мел гибсон джоли хопкинс мишель пфайфер джекниколсон и миллиарды других они вовлечены в огромный скандал из за которого все их знакомые и начальники работают над пулей в мою голову и правительство сша тоже . я хранитель печати 50 штатов сша и монарх совращающий миллиарды людей. я карен кимберли и джон маккейн сенатор от аризоны и мой единственный господин муж гарри чарльз дэвид второй сын чарльза и дианы спенсер . мы трое очень важные сегодня люди я также стану единственным федеральным правительственным монархом и единственным послом мира .смертная казнь всем американским актёрам пусть они умрут в тюрьме со всей своей семьёй.
Не могу представить, какой выдержкой нужно обладать, чтобы написать в ответ:
Если у вас есть вопрос или совет редакторам вашего любимого блога, пожалуйста, отправьте письмо в по соответствующему адресу:
(список наших основных блогов и электронных адресов)

15th May 2015

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

Упаковка чайных пакетиков, отправленная из Будапешта в Питер, не поменяла расклад: заваривается по-прежнему плохо. Может, это от качества воды зависит? Вода, естественно, кипячёная.

14th May 2015

19:22: Конференционное
29 мая я буду на конференции Joy of Coding в Роттердаме. Программа выглядит очень интересно.

13th May 2015

21:40: Ватничное
У меня есть такая нехорошая черта — склонность поддерживать начальство. Если, конечно, оно даёт к этому хоть какую-то возможность.

Да-да, правда-правда. Как сейчас помню, когда ВВБХ сделал Михалкова-старшего трижды гимнюком, я довольно долго доказывал своим родным и близким, что, дескать, ничего страшного, что оно правильно всё делает, что нам так пофиг, а старичкам, может, приятно. Ну, и так далее.

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

Так вот. В сообществе pora_valit очередная драма, один гонит на модераторов, я, как обычно, наоборот, в общем, шум, гам, веселуха, и проч. И вот на первый же мой коммент человек отвечает так:

Так вот, у меня вопрос. Не знает ли кто-нибудь, где мне получить свою долю?

12th May 2015

21:14: Парадное
Что-то меня совершенно не заботят те люди, которые вышли в этом "бессмертном полку" с чужими (или не чужими) фотографиями за деньги или из-под палки, а потом побросали эти фотографии в мусорку. Деньги — вещь нужная, фотографии на палках — нет, сама акция бессмысленна изначально.

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

On an unrelated note: Гугль снова проснулся и захотел меня поинтервьюить ещё. Вежливо, но кратко ответил, что в данный момент не заинтересован.

11th May 2015

09:38: Я не опоздал?
А то никак руки не дойдут записать прогноз на следующий ДП, а прошлое меняется быстрее, чем скала проект компилирует.

Да, прогноз: эрэфия будет праздновать совместную с Рейхом победу над фашистской Америкой.

9th May 2015

01:33: Вуайеристское
Парой постов avva навеяло.

Мне представляется, что если у сексуального акта есть зритель, то этот зритель является — пусть и в меньшей мере — его участником.

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

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

Аргумент "не хотел смотреть — мог отвернуться" является при этом типичнейшим проявлением blame the victim. Соблюдение прав человека является — по умолчанию — обязательным, даже если человек не делает ничего, чтобы свои права отстоять. Грабитель является преступником, даже если его жертва не сопротивлялась. Насильник является преступником, даже если его жертва шла в мини-юбке ночью по тёмному переулку. Другое дело — если жертва сама приложила усилия к тому, чтобы стать жертвой. Человек, обманом проникший в закрытый клуб, не имеет никакого права высказывать претензии к происходящему на сцене.

Это я всё к той парочке, которая занялась сексом на пляже во Флориде. Соответственно, ей теперь грозит пара месяцев тюрьмы (ИМХО — очень мало), ему — 15 лет, так как он раньше попадался на транспортировке наркоты; кроме того, оба попадают в sex offenders list, что очень сильно усложняет им жизнь (и это хорошо).

Да, очень сильно обозлило американскую Фемиду то, что на пляже были маленькие дети. И, по-моему, это тоже абсолютно правильно: изнасилование — всегда мерзость, но изнасилование ребёнка обычно считается мерзостью многократно большей.

5th May 2015

12:10: Хотите верьте, хотите — нет,
но этот пост делается исключительно по рабочей надобности.

15th April 2015

22:53: Беспроводное
Ещё из современных штук, от которых все тащатся, а я не понимаю. Вот беспроводная зарядка — она зачем?

Если я правильно понимаю, то беспроводная зарядка — это такая подставка, на которую надо положить телефон, после чего он начинает заряжаться. Это так?

То есть, когда я вставляю провод, я могу положить телефон куда угодно в пределах длины провода. Что более существенно, я могу взять его в руки и с ним работать. Могу позвонить кому-то. И при этом телефон будет исправно продолжать заряжаться.

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

Так нафига эта беспроводная зарядка нужна?

31st March 2015

00:49: Общее место или нет?
Есть такой треугольник из имён. Я его в своё время обнаружил сам, но, может, он всем известен:

1) Денис Давыдов. Полковник, командир партизанского отряда в войне 1812 года (и, к тому же, поэт).

2) Василий Денисов. Полковник, командир партизанского отряда в "Войне и мире" Толстого.

3) Давыд Васильев. Полковник, командир партизанского отряда в пьесе "Давным-давно" (возможно) Гладкова и фильме "Гусарская баллада" Рязанова.

Васька Денисов стихов, вроде, не писал — зато обалденно танцевал мазурку. А вот Давыд Васильев — почти писал:
Ну вот, уснул бивак наш партизанский.
Люблю картину эту, хоть пестра.
Овса кули, соломы жёлтой связки,
Ночное небо, зарево костра,
Усы, торчащие подобно острым пикам,
И храп, что пострашнее львиных рыков
И посильней архангельской трубы.
Поэзия есть в эдаком пейзаже.
             Р ж е в с к и й
Поэзия? Ну, вот ещё что скажешь!
             В а с и л ь е в
Да, брат, поэзия! Найдётся, может быть,
И среди нас достойный сочинитель,
Опишет это всё, когда пройдёт война,
И наша боевая старина
Воскреснет в сказках, что читают детям.
Current Mood:

26th March 2015

22:41: Как всегда
вариантов оказывается немного: то ли они все там анаши перекурили, то ли... на этом мысль останавливается.
Current Mood:

17th March 2015

13:31: Получил справку
что не идиот. Ещё одну. Mensa HungarIQa — как я понимаю, местное отделение Mensa International — прислала мне уведомление, что у меня IQ выше, чем у 99% людей на Земле и они готовы со всей нежностью принять меня в свои ряды.

Интересно, кроме строчки в резюме и личного удовлетворения, какие-нибудь бенефиты от этого будут?
Current Mood:

13th March 2015

12:59: Чувствую себя устаревшим.
Столько всего происходит, столько всего появляется, что у всех на устах и в компьютерах — а я понять не могу, нафига всё это надо. И не то, чтобы я не пробовал — я именно пробую... и всё равно не понимаю.

Facebook. Дофига и более народу им пользуется. У меня тоже есть Facebook (и даже два — долгая история). Я туда не хожу. Я не знаю, куда там ходить. Я не знаю, что там искать. И как искать (интерфейс у них откровенно ублюдочный). Да, я как-то попользовался ихним чатом. И, в общем-то, всё. Если мне надо что-то написать — я пишу сюда, в ЖЖ. Здесь по крайней мере есть нормальные древовидные комменты. Поставить лайк? А зачем?

Evernote. Тоже: куча народу пользуется и восхищается, как это круто. Я попробовал. Ну нифига ж не круто. Ну да, можно туда чой-то запихнуть. Даже довольно многое. А зачем? Шоб було?

IFTTT. Идея выглядит очень круто: автоматизировать работу с телефоном — в ограниченных масштабах, но это-то и хорошо, а то люди начнут видеорендеринг на этом деле писать. Ну что ж, поставил. ОЧЕНЬ долго пытался придумать ХОТЬ ЧТО-НИБУДЬ, что эта штука может, чтобы мне это было нужно. Не придумал. Всё, что предлагают — это штуки типа "если вы лайкнули что-то в фейсбуке — написать об этом в твиттер". НАХРЕНА???

Смарт-часы. Я благословляю того человека, который догадался, что мобильный телефон должен показывать время. Потому что это позволило мне наконец избавиться от этой тяжёлой, неуклюжей, безумно лишней штуки на запястье. Впрочем, не совсем: некоторое время я носил часы на цепочке. Это было ещё более-менее. А тут Тим Кук со сцены объявляет: я, дескать, с детства мечтал отвечать на телефонные звонки с часов. Я как представлю, как надо руку вывернуть, чтобы запястье оказалось рядом с ухом...

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

В общем, да. Консерватор я. Совершеннейший.

10th March 2015

17:45: Наконец нашёл время поискать ответ...
...и нашёл.

Функция x\sqrt{x^2+y^2} дифференцируема по x и по y всюду, но вот смешанная производная существует не везде.

Этот мой затуп примечателен тем, что тянется как минимум с 1996 года. Я периодически о нём вспоминал, думал, что надо бы что-то с ним сделать, отвлекался и забывал снова.

9th February 2015

13:19: Про самодонесение
В общем-то, тему донесения на себя о наличии второго гражданства (или ПМЖ) обсосали уже со всех сторон. Я просто хочу привести одну цитату, которая, мне кажется, иллюстрирует мои опасения по этому поводу.

До сентября 1943 года Сен-Рафаэль был оккупирован итальянскими войсками. Они были человечны и иногда даже обуздывали усердие властей «Виши». Тем не менее начиная с лета 1942 года эти власти предписали всем французским подданным еврейского происхождения «для своей пользы» зарегистрироваться в полицейском участке по месту жительства. Туманные угрозы возмездия висели над нарушителями. Знакомые, уроженцы Франции еврейского происхождения, уговаривали меня последовать их примеру и зарегистрироваться во избежание неприятностей. Но мне казалось, что быть записанным «евреем» в полицейском участке — это уже начало неприятностей, и я воздержался. Впоследствии оказалось, что я был прав.
...
Осенью 1943 года я нашел, что достаточно примелькался в Сен-Рафаэле и что не плохо было бы переменить обстановку. Итак, в сентябре 1943 года я отправился в Гренобль,.. Я пообедал в вагоне-ресторане, где мой «визави», на которого я, очевидно, произвел хорошее впечатление, поделился со мной информацией, источником которой будто бы являлся его хороший знакомый, важный полицейский чиновник. «Всех этих евреев (он употребил другое слово), которые валяются на пляжах Ривьеры и чувствуют себя, как „у Христа за пазухой“, скоро заберут и рассадят по лагерям. Вполне возможно, что облава начнется сегодня ночью». «Я знаю одного, который от вас уйдет», — подумал я, расставаясь со своим «симпатичным» собеседником. Он был прав, и несколько несчастных, которые зарегистрировались в Сен-Рафаэле, исчезли в ту ночь.

©Анатоль Абрагам, «Время вспять, или физик, физик, где ты был» (автобиография)

Что там говорите? Проще сообщить о наличии второго гражданства и спать спокойно? Ну-ну.
Powered by LiveJournal.com