Hinterland

9:11pm: Против аналогового секвенсора не попрешь, part 1: QuasiQuotation
На первоначальных этапах нам предстоит иметь дело с генерацией и преобразованиями С-кода, поэтому стоит поговорить о механизме QuasiQuotation.

Пусть у вас есть два языка программирования L и M (это может быть один и тот же язык). Вы хотите генерировать или преобразовывать программы на языке M функциями языка L. Пусть SM -- тип, описывающий синтаксис языка M в языке L. На практике тип SM это обычно запутанный набор взаимно-рекурсивных типов. Чтобы что-то с ним сделать вам придется изучить как он устроен и писать много довольной уродливых выражений. Гораздо удобнее иметь механизм, позволяющий вам писать куски кода на M, которые автоматически преобразовываются в выражения типа SM. Более того, вы можете иметь ``переменные'' внутри фрагментов M-кода, с соответствующей операцией подстановки. Это и есть механизм QuasiQuotation. Когда возможности подстановки нет, это называется просто Quotation.

Поясним на примере.
( Read more... )
Такие дела. На фото я.

1:43pm: Против аналогового секвенсора не попрешь, part 0
Ах да, синтостроительный блог. Все в курсе, что пресеты убивают музыку, да? Вместо того, чтобы искать интересные новые звуки, люди просто строят композиции из уже готовых. Иногда это уместно, но когда я снова и снова слышу драм-машину TB-808, хочется ``блевануть, прыгнуть с обрыва, броситься по автобус''. Симфонический оркестр, панк-тройка это все виды пресетов. Кроме того, думаю ясно, что инструмент (в широком смысле) накладывает определенные ограничения на конечный результат. Здесь должна быть релевантная цитата из Миши про кубейс, но я ее почему-то не нашел.
( Read more... )
Такие дела, на фото я.

2:46pm: Fires within fires
Надо отметить, что этот мистический пожар гораздо интереснее предыдущего.
Особенно про убитых черкассов понравилось.

9:34pm: Amnesty (I)
Пацаны, у Crystal Castles новый альбом вышел.
(на самом деле еще нет, но на трекерах уже есть)

8:35pm: Володя - потусторонний шофёр
Интресное.

Then I was surrounded by a group of logisticians who trusted the connection
between type theories and set theory on faith and who tried to convince me
and others that mathematicians should do likewise.
It is only less than a year ago and due to the steadfast refusal of the
mathematical community to do so that I was able to disentangle myself from
them and to continue the work interrupted in 2009.

Прежде, чем объединяться, и для того, чтобы объединиться, мы должны сначала решительно и определенно размежеваться:

There is a theory that logicians developed that is based on concepts such as
meaning explanation or strong normalization that provides consistency proofs
for some sample type theories but it leads to the isolation of type theory from
the rest of mathematics rather than to their integration.

Если кто не верит в сильную нормализацию, это нам кафиры, короче.

На фото Владимир Воеводский переосмысливает теории Мартин-Лефа с точки зрения современной математики:

9:44pm: Worse than random generated syntax
Пользователь ketmar вновь поднимает важный вопрос. От себя добавлю ссылку на статью Subtleties of the ANSI/ISO C standard. Краткое содержание: ``there is no C program for which the standard can guarantee that it will not crash''. Типа, все что нужно знать о языке С.

Язык С -- не для людей, но есть области, в которых он хорош. Поэтому его можно использовать в качестве целевого языка, работая внутри другого языка. В Haskell, например, для этого можно использовать механизм QuasiQuotes. Очень удобно. Экспериментирую тут с музыкальными модульными синтами. Каждый модуль это небольшой кусочек С-кода, прописывается вручную. Есть комбинаторы для разных видов композиции модулей. Haskell-программа делает из кусочков полноценные функции. Плюс следит за совместимостью модулей, строит (когда возможно) преобразование синтаксически неэквивалентных структур и т.п. Плюс возможность иметь модули, параметризованные более-менее чем угодно. Ну и так далее. Пока я в самом начале; иншаллах, здесь будет синтостроительный блог. Называться будет ``Против аналогового секвенсора не попрешь'', конечно же.

Tip: Когда вы знакомитесь с языком, смотрите как в нем реализована (если вообще) прямая сумма.

Такие дела, на фото я.

6:22pm: As Live As You Can Get
Lazyweb, может быть кто-нибудь встречал или может составить сам по личному опыту список полезных советов по поводу мастеринга цифрового файла для записи на кассетную пленку? Интересует все, что вы можете сообщить. Punk/post-punk split, tipa. ``Всему хутору расскажем про вашу доброту'' и т.д.

10:40pm: Ричард Карп писал о совсем другом
Великие CS мастера древности такие как Кнут или де Бройн были еще и матерыми комбинаторщиками. Связь между алгоритмической сложностью и комбинаторикой, думаю, ясна (вообще-то нет, тут надо бы большую врезку сделать). К сожалению, успехи микроэлектроники заметно снизили необходимость в тщательном анализе алгоритмов, в результате чего теория сложности была захвачена тварями из черной лагуны и по большей части оказалась в аду неконструктивности. Мне всегда казалось это странным, потому что речь в обоих идет о совокупности конструктивных объектов. Если сказать точнее, я был очень удивлен, что перечислительная комбинаторика в действительности не перечисляет, а только считает объекты.

Обычный вопрос звучит так: сколько есть объектов типа X, обладающих свойством P. Обычный ответ дает какую-нибудь формулу подсчета и нудное доказательство в котором смешаны объяснения на естественном языке, формулы, рисунки всякие идиотские. Т.е. в доказательстве есть алгоритм построения объектов, но нет подходящего языка, чтобы формально его описать, вместе с доказательством корректности.

И здесь в игру вступает теория типов.

( Read more... )

Такие дела, на фото я.

1:03pm: Type Refinements for the Working Class
Есть два мотива: синенький и рыженький.

Рыженькие определения вычислимости основаны на языке (или лучше сказать на понятиях выражения, переменной, подстановки и сокращений), а синенькие -- на понятии машины. Рыженькие языки программирования -- это те, семантику (или большую ее часть) которых можно объяснить в терминах самого языка, а для объяснения семантики синеньких нужно вводить дополнительные сущности (типа нельзя объяснить программу на Си, не упоминая о том, что есть машина, на которой она выполняется). Рыженькие конструктивные объекты -- это корневые деревья (as in abstract syntax tree), а синенькие -- это простые неориентированные графы. В пользу последнего говорит многое. Например, наименее уродливые программы на рыженьких языках для неориентированных графов в первую очередь строят дерево его обхода, а потом уже делают рекурсию по этому дереву.

Что касается комбинаторных объектов, то тут... часть записи утеряна... переписать как рыженький.

Иллюстрация ко всему вышесказанному:

8:45pm: Сrystal Сastels. Новый трек.

Типа вот:

11:20pm: Виталий Даркфолк рекомендует
Вся ``структурность'' в четырехчасовом фильме. Много хороших людей, о которых вы вероятно никогда не слышали.



Среди прочего есть запись возмутительного нападения врагов свободы на группу ПКМН во время выступления.

10:40pm: Записал песню с новой вокалисткой Эдит
Между тем, Crystal Castles выпустили новый трек. Без няши Элис, ага. Впрочем вокал у них всегда так сильной обработан, что это почти незаметно. Вот странно, что технология вокалоидов не нашла применение в такого рода ситуациях. Если вы все равно собираетесь накладывать кучу эффектов, зачем вам возиться с живым человеком? Очень неудобно. Опять же захотелось текст поменять, это ж снова сессию организовывать, вызванивать там всех... бр... Музыка это слишком важная область, чтобы доверять ее людям. Впрочем, вокалоиды как они сейчас есть тоже неудовлетворительны, поскольку основаны на большой библиотеке семплов. Честный подход, на мой взягляд, это articulatory synthesis. Было бы здорово еще к тему иметь технологию калибровки, типа по записям оценивать необходимые параметры модели речевого тракта. Seems feasible.

8:22pm: Пять высоченных девушек-моделей
Министерство финансов США ввело санкции против Евразийского союза молодежи.

Поздравляем отцов и мать основательницу!

Будущее создается тобой, но не для тебя.

Впрочем, все это уже не имеет значения.

8:58pm: Кто воюет за унивалентность, тот нам кафир, короче
Зашел посмотреть как дела в унивалентном джамаате. А там уже фитна, конечно:

I don’t know who your sources are, but they are not accurate. Michael Warren was my student and we were working together. This was always presented as joint work, and anyone who was present at the early talks will confim this. Perhaps someone will volunteer a confirmation on this list, but I don’t really think it is appropriate to have this sort of discussion here. I only reply now because I cannot allow you to continue to spread such falsehoods in public without any rebuttal. My contributions are a fact beyond doubt, known to many people who were involved in the early development, and I think that your attempts to dispute them are a dishonest and unethical abuse of your influence which should not be tolerated.

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

10:51pm: Булева слепота
Юзер ketmar поднимает важную тему. В самом деле, сколько можно это терпеть? Как известно, булев тип -- это тип, который имеет ровно два значения. Если вы используете его, чтобы проверить выполняется ли некоторое условие (предикат), то вы оказываетесь в весьма глупом положении, потому что эти значения сами по себе никак не связаны с условием, которые вы хотите проверить. Это явление известно как булева слепота.

Механизм зависимых типов позволяет излечиться от булевой слепоты.

( Read more... )

Незатейливый теоретико-типовой юморок:

10:02pm: Polya enumeration theorem
А кто-нибудь знает / может придумать альтернативное определение циклического индекса, чтобы такое же простое, но без полиномов?

КДПВ:

12:45pm: Крестовый поход детей
Сегодня, как известно, годовщина новогоднего штурма Грозного:



In April 1995, General Kvashnin told me in Grozny: ≥We will beat the Chechens to pulp, so that the present generation will be too terrified to fight Russia again. Let Western observers come to Grozny and see what we have done to our own city, so that they shall know what may happen to their towns if they get rough with Russia. But you know, Pavel, in 20-30 years a new generation of Chechens that did not see the Russian army in action will grow up and they will again rebel, so we'll have to smash them down all over again.≤ (отсюда)

What could possibly go wrong?



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

``Этот остров необитаем''.

10:16pm: Break up your fallow ground, and sow not among thorns.
В январе 2014 года чел из университета Токио разместил работу, в которой улучшил показатель степени для сложности быстрого матричного умножения с 2.3729269 до 2.3728639. В 2014 г. Да еще и в ворде статью написал. Можно было бы отнести в разряд курьезов, но давайте посмотрим на список того, что считают главными нерешенными проблемами в computer science. Быстрое матричное умножение (с упоминанием этого чела) там сразу после P=?NP и односторонних функций. Если вам нужно было определение словосочетания ``ссаный позор'', то вот по-моему неплохой кандидат.

( Read more... )

На самом деле я настроен весьма оптимистично. В Haskell community полно полностью поехавших гиков, которые, вдоволь наигравшись с Хаскеллем, переходят на более тяжелые наркотики. А это означает, что more crazy shit coming soon along w/ some other cool stuff.

10:31pm: All Concepts are Kan Extensions, Part 0
Решил изучить continuation-passing style, call/cc, codensity monad, вот это все. Прочитал статью, в которой в числе прочего утверждается, что многие оптимизирующие преобразования программ суть реализации категорной конструкции под названием правое расширение Кана. Типа вся сущность СиПиЭс была изложена в упражнениях к десятой главе известной книги ``Categories for the working mathematician''. Хорошо бы понять так ли это.

Сегодня будет разогрев.

( Read more... )

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

Картинка для привлечения внимания:

8:17pm: И ты, Брут, продался большевикам?
Новости из унивалентного мира:

Applications are invited for two postdocs and one PhD student to work on the recently funded EPSRC grant "Homotopy Type Theory: Programming and Verification" obtained by Professor Neil Ghani and Dr Conor McBride (University of Strathclyde), Dr Thorsten Altenkirch (University of Nottingham) and Dr Nicola Gambino (University of Leeds). One postdoc and will work on more theoretical aspects of the project in Nottingham, while the other postdoc will work on implementation issues in Strathclyde. Nevertheless, the reality is that we will be working as a team with frequent visits expected between ourselves and our collaborators.

Homotopy Type Theory (HoTT) is a revolutionary new approach to type theory where types are interpreted as spaces, terms as points and equalities as paths... Ну и так далее.

Короче говоря, МакБрайдушка теперь тоже с ними. Шаг, конечно, понятный -- у ребят проблемы с совместимостью унивалнтности и dependent pattern matching, а МакБрайд в последнем большой специалист. Однако, видимо, никакой другой теории типов кроме гомотопической в ближайшее время не будет. Есть конечно Эдвин Бреди, есть Роберт Эткей, есть ученик МакБрайда Пьер ``МакДаг'' Даган, есть наконец зеленая поросль аспиров, ``поднявшихся на здоровой закваске'', но думалось, что в бой против унивалентной чумы поведет их МакБрайд. Но нет, видимо вместо ожидавшегося второго Эпиграмма и прорывов в области refinement types нас ждут сотни страниц с диаграммами, симплициальными множествами и т.п. Ну может людям, который занимаются приложениями, вроде Ксавье Лероя надоест писать тактики в Ltac и они начнут заниматься, скажем, доказательством через рефлексию. Было бы здорово.

Есть еще Абель, Нилс и Ульф, но они вроде рубятся за sized types, а православный путь -- это memo-структуры или Bove-Capretta method.

Вот так, если у тебя есть премия Филдса, то ты можешь войти в любую область и наводить там свои порядки. Интересно посмотреть на становление гомотопической теории типов через призму приматологии науки. Ткачев слегка поехавший, but he's got a point. Всем сила и власть, пацаны!

Картинка для привлечения внимания:

11:39pm: Воеводские выкормыши не успокаиваются: доклад про кубическую теорию типов. Оказывается, чтобы вычислять нужны кановские кубические множества (чтобы это не значило). Ужас и моральный террор. Ну ладно, на самом деле там чтобы вычислять в присутствии аксиомы унивалентности. Не знаю, нужны или нет, но думаю, что сперва следует задать вопрос: а нужна ли аксиома унивалентности? Так говорил МакБрайд:

It's clear that function extensionality, quotients, and working up to isomorphism (and other weak equivalences) are important things to have a handle on. However, univalence does not have a monopoly on approaches to those concepts. As an axiom with no computational behaviour, I find univalence deeply troubling. But I shall cheerfully applaud a computational theory with decidable equality and typechecking judgments which validates the axiom and computes canonical values.

Это называется "ясный левацкий взгляд". Вычислительная интерпретация унивалентности сейчас построена с помощью этих самых кубических множеств (с каноничностью не все ясно). Но вопрос в том, мне лично трудно представить ситуацию, когда бы занадобилось переносить конструкции между, например, натуральными числами и бинарными деревьями. В то же время, было бы крайне удобно подменять различные способы описания, скажем, графов по ситуации. Унивалентность может тут помочь, но не является необходимой для этого. Мне МакБрайдовские подходы (views, ornaments) гораздо симпатичнее (они ведь из программирования растут). И еще цитата:

But I'm happy if there's some well managed way to talk about types at a finer level than isomorphism, e.g., by encoding types in a universe: equality of codes might well be finer than isomorphism of the types codes mean. I'd be really pleased if the types we wrote down were automatically internal syntactic objects, so that we could choose to interpret them in a variety of interesting ways, each with its own notion of equality. It may well be that uniqueness of equality proofs for the syntactic objects is sustainable alongside a multiplicity of isomorphisms between the underlying sets, as long as we are clear which we mean.

Делать универсальный язык или систему доказательств -- это все таки дикость и двадцатый век. Нужно учиться строить интересные универсумы и продвигать политипическое программирование. Ради этого можно даже с настоящим параметрическим полиморфизмом попрощаться.

А еще у них грант на семь с половиной лимонов от ВВС США. What would Grothendieck do?

10:05pm: Что касается свирелей, струн и барабанов, на которых играют женоподобные мужчины...
Аллах запрещает VST-инструменты, но не VST-эффекты.

10:02pm: Метатели стрелок в ковариантную сторону
На реддите очередной срач на тему ``нужна ли теория категорий программисту''.

Вот разные умные люди размышляли над концептом ``data''. И пришли к интересным вещам типа индуктивных или индуктивно-рекурсивных семейств. Их можно рассматривать как начальные F-алгебры для функторов F в некоторых категориях, обладающими свойством ``строгой положительности''. А можно этого не делать. Например, попытки явно описать, что же это за категории приводят к конструкциям громоздким и для многих совершенно непрозрачным. В оригинальных работах же все это строилось как расширение теории Мартин-Лефа с помощью правил введения/исключения. Просто, конструктивно и понятно.

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

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

5:20pm: Кавер на CC