⅋

Товарищ Jean-Yves Girard настолько крут, что за ним просто невозможно поспеть. Крутилась несколько недель в голове связь между скрещенным произведением, аддитивной "импликацией" в линейной логике и квантовой суперпозицией. Я только думал, как бы подступиться к туманным аналогиям. Придумал кейворды, загуглил. Какой удар со стороны классика: Geometry of Interaction V: logic in the hyperfinite factor (2010)! :-)

P.S. Причём, чтобы в этом сходу разобраться, я слишком туп. Я врубился, что это именно о том, но продраться сквозь технические подробности даже приблизительно (для грубого операционного понимания формализма) с наскока не удалось. Нужно где-то взять на это часов 15 потупить в публикацию, только где.

Линейные зависимые типы

Я давно слежу за попытками объединить линейную логику и зависимые теории типов. Тому есть пара банальных технических мотиваций программиста: линейная логика, это логика, где помимо values существуют entities, представляющие объекты материального мира. То есть это могут быть ресурсы, не подлежащие копированию/совместному использованию, capabilities и тому подобное. Очень основательная работа на эту тему появилась вот буквально на днях: http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf.

В работе прямо приводится в качестве примера, как в рамках этого формализма описывать императивные программы (инструкции описываются Хоаровскими тройками, есс-но) и совершать reasoning на их тему. Ежели удастся скрестить этого ужа с гомотопической теорией типов, reasoning (то есть верификация при помощи автопроверяемых доказательств тех или иных полезных свойств императивных программ) станет совсем прекрасным. Вот, кстати, пример того как нынче можно доказать ценное высказывание о программах: Type Soundness and Race Freedom for Mezzo. В Меццо как раз гибридная система типов на базе capabilities (ownership, в основном).

Однако есть ещё несколько важных причины, почему я слежу за этим "великим объединением":
- Можно описывать "невидимые" эффекты функциональных программ: потребность во времени и месте. То есть вместо sort: {T: Type} -> List T -> List T писать по взрослому: sort: {T: Type} -> {n: Nat} -> Vec n T -> TIME(12 * n * log n) -o Vec n T.
- Раз линейная логика отлично подходит для описания квантовых явлений, grand unified type theory должна на равне с обычными вычислениями подходить для описания квантовых, а также там должны естественным образом кодиться всякие некоммутативные штуки.

В линейной логике есть обычные операторы "мультипликативное и" и "аддитивное или":
(Ботинок ⊗ Шапка) это пара, из которой можно извлечь ботинок и шапку и работать с ними дальше.
(Ботинок ⊕ Шапка) это либо ботинок, либо шапка: можно при помощи match/case выяснить что именно и дальше работать с имеющимися ботинком или шапкой.

Но есть и операторы "мультипликативное или" и "аддитивное и". С аддитивным "и" всё просто?
(Ботинок & Шапка) это ящик, из которого мы можем взять либо ботинок, либо шапку, но не то и другое. Характерное использование — тип "автомата по продаже напитков": $1 -o (Кола & Фанта & Спрайт). То есть за один доллар можно взять либо то, либо другое, либо третье, но не всё вместе. А вот мультипликативное "или" это просто квантовая суперпозиция:
Ящик-Шрёдингера = (Мертвый-кот ⅋ Живой-кот).

Если у нас есть информация e: не(Мёртвый-кот), мы можем извлечь из ящика живого кота и наоборот. В противном случае чтобы преобразовать объект типа Ящик-Шрёдингера, нам надо заготовить обработчики match/case для обоих случаев, и они будут "работать параллельно" точно как в квантовой механике фотон отрабатывает все доступные пути, а результатом является интерференция этих путей.

Boolean = {True} ⊕ {False}
QBit = {True} ⅋ {False}

В работе по интеграции зависимых типов пока мало об этом. И главное срршенно непонятно, откуда должно взяться, что у кубита нетривиальная внутренняя структура (внутренняя степень свободы в виде U(1)-торсора), то есть (QBit = QBit) = U(1), а у сцепленного массива кубитов эти внутренние степени свободы когезивны.