Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

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

Я давно слежу за попытками объединить линейную логику и зависимые теории типов. Тому есть пара банальных технических мотиваций программиста: линейная логика, это логика, где помимо 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), а у сцепленного массива кубитов эти внутренние степени свободы когезивны.
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments