Линейная логика X: Изменяя мир

Linear types can change the world! 

Philip Wadler

Что может дать линейная логика программисту или проектировщику языка программирования? Слишком много, чтобы охватить всё сразу. Попытаемся рассмотреть сферы применимости, не претендуя на полноту разбора.

Вспомним, где в программировании встречаются линейные функции. Программистам знакомы понятия линейной, квадратичной, логарифмической и т.д. сложности. Речь идёт об оценке сложности алгоритмов. Линейная сложность означает, что мы можем оценить количество операций линейной функцией (от количества элементов контейнера, например).  И замечательным образом процедура, которая использует свой аргумент ровно один раз, будет обладать линейной сложностью относительно количества структурных элементов аргумента. Грубо говоря, процедура, которая принимает линейный список, сможет пройтись по элементам этого списка только один раз, что соответствует линейной сложности относительно размера списка. Это означает, что немного модифицировав правила линейной логики, можно получить языки программирования с ограничением на алгоритмическую сложность процедур. Сам Жирар предложил несколько систем типов ‒ ограниченную линейную логику (bounded linear logic, BLL), легкую линейную логику (light linear logic), элементарную линейную логику (elementary linar logic. ELL). Пока они интересны только с исследовательской точки зрения, но возможно в будущем появятся полноценные языки программирования на их основе.

Прохождение по списку в
функциональном стиле

Жирар назвал линейную логику "логикой, стоящей за логиками". Её можно представлять себе как язык более низкого уровня по сравнению с интуиционистской и классической логическими теориями. У этого языка отчетливо императивный привкус. Просто поразительно, что требование линейности, самое желанное требование для математической структуры с точки зрения исследователя, требование, которое по идее должно отдалять от реальности, приблизило логическую теорию к металлу...  Это логика в которой линейная функция естественно представляется, как процедура уничтожающая аргумент и производящая результат. Ведь если у вас есть линейное значение, то это значит, что про него более никто не знает и никто не заботится, вы можете делать с ним всё что вам заблагорассудится. Вы можете его изменить. Эта операция попросту невозможна в чисто функциональном языке, это должно звучать так же дико как изменить натуральное число. Представьте себе, что мы сегодня поменяем четыре и оно станет пятью (и дважды два станет пять). Тем не менее, если про существование данной четверки никто кроме нас не знает, мы можем её подменить пятёркой. Чем собственно и занимаются компиляторы таких языков. Они отслеживают и оптимизируют работу со значениями, которые видимы только локально. (Они могут при этом жестоко ошибиться в своих оптимизациях. Для Haskell известны программы, которые отлично работают в отладочной версии, но перестают работать при включении оптимизаций, расходуя всю наличную память. Примечательно, что одно из решений ‒ это введение примитивной операции, которая помогает сохранить линейность данных¹.)

Линейность обеспечивает очень важную вещь с точки зрения программирования ‒локальность. Если про переменную знает только одна функция, то для такой переменной не нужна сборка мусора (в том числе в виде подсчёта ссылок). Не нужны критические секции, чтоб контролировать к ней доступ в многопоточной среде ‒ ведь никто кроме нас и не будет к ней обращаться. Локальность данных делает код ясным и для программиста и для компилятора.

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

Скриббл ‒ язык описания протоколов общения,
основанный на сессионных типах

Вернёмся пока к последовательному исполнению. Кроме возможности обновлять данные линейная логика может помочь с другими возможностями, присущими императивным языкам. А они нужны, ведь у чисто функционального языка есть один недостаток: никто не будет использовать такой язык для прикладного программирования. Кому нужен язык, который даже не может вывести данные в консоль? Возникает вопрос, как интегрировать в такой язык общение с внешним миром, сохранив при этом его математическую природу. Вероятно нам нужно обозначить отдельным типом функции взаимодействующие с внешним миром. Фактически считать, что они принимают на вход состояние мира и возвращают новое. И здесь идея линейности может пригодиться, поскольку  состояние внешнего мира невозможно сохранить, скопировать, но желательно не терять².

Что интересно, идея такого использования линейных типов появилась почти одновременно с линейной логикой. Вариант линейных типов ‒ уникальные типы (uniqueness types)³ используется в языке Clean, который появился в 1988 году (работа Жирара по линейной логике опубликована в 1987). Даже не знаю, имел ли представление тогда автор языка о линейной логике. 

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

---

¹ Это операция явного копирования, которой в линейной системе типов можно присвоить тип dup: !A ⊸ A. Результат является независимой копией аргумента. В Haskell линейных типов нет, но смысл в том, что мы используем результат линейно.

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

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