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... )
Такие дела, на фото я.

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?