Система субструктурных типов

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

Различные системы подструктурного типа

Несколько типовых систем возникли в результате отказа от некоторых структурных правил обмена, ослабления и сжатия:

	Обмен	Ослабление	Сокращение	Использовать
Заказал	—	—	—	Ровно один раз по порядку
Линейный	Допустимый	—	—	Ровно один раз
Аффинный	Допустимый	Допустимый	—	Максимум один раз
Соответствующий	Допустимый	—	Допустимый	Хотя бы один раз
Нормальный	Допустимый	Допустимый	Допустимый	Произвольно

• Системы упорядоченного типа (обмен отбрасыванием, ослабление и сжатие): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
• Системы линейного типа (допускают обмен, но не ослабление и сжатие): каждая переменная используется ровно один раз.
• Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
• Соответствующие системы типов (допускаются обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
• Системы нормального типа (допускают обмен, ослабление и сжатие): каждая переменная может использоваться произвольно.

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

Система упорядоченного типа

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

Системы линейного типа

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

Язык программирования Clean использует типы уникальности (вариант линейных типов) для поддержки параллелизма, ввода/вывода на месте и обновления массивов .

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

Свойство единственной ссылки делает системы линейного типа пригодными в качестве языков программирования для квантовых вычислений , поскольку оно отражает теорему о запрете клонирования квантовых состояний. С точки зрения теории категорий , отказ от клонирования — это утверждение о том, что не существует диагонального функтора , который мог бы дублировать состояния; аналогично, с точки зрения комбинаторной логики , не существует K-комбинатора, который мог бы разрушать состояния. С точки зрения лямбда-исчисления переменная x может появляться ровно один раз в термине.

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

Системы аффинного типа

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

Соответствующая система типов

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

Интерпретация ресурса

См. также: Linear_logic § The_resource_interpretation.

Номенклатура, предлагаемая системами субструктурных типов, полезна для характеристики аспектов управления ресурсами языка. Управление ресурсами — это аспект языковой безопасности, обеспечивающий каждого выделенного ресурса освобождение ровно один раз. Таким образом, интерпретация ресурса касается только использования, которое передает право собственности – перемещение , где право собственности – это ответственность за освобождение ресурса.

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

	Отказ от движения	Обязательный ход	Переместить количественную оценку	Принудительный конечный автомат вызова функции
Нормальный тип	Нет	Нет	Любое количество раз	Топологическое упорядочение
Аффинный тип	Да	Нет	Максимум один раз	Заказ
Линейный тип	Да	Да	Ровно один раз	Заказ и завершение

Ресурсно-аффинные типы

Согласно интерпретации ресурса, аффинный тип не может быть потрачен более одного раза.

Как пример, один и тот же вариант торгового автомата Хоара можно выразить на английском, логике и на Rust :

Торговый автомат

Английский	Логика	Ржавчина
Монета может купить тебя конфета, напиток, или выйти за рамки.	Монета ⊸ Конфета Монета ⊸ Напиток Монета ⊸ ⊤	fn buy_candy(_: Coin) -> Candy { Candy{} } fn buy_drink(_: Coin) -> Drink { Drink{} }

Что это значит для В этом примере монета должна быть аффинным типом (что так и есть, если только она не реализует Признак копирования ) заключается в том, что попытка потратить одну и ту же монету дважды — это недопустимая программа, которую компилятор имеет право отклонить:

let coin = Coin{};
let candy = buy_candy(coin); // The lifetime of the coin variable ends here.
let drink = buy_drink(coin); // Compilation error: Use of moved variable that does not possess the Copy trait.

Другими словами, система аффинных типов может выражать шаблон состояния типов : Функции могут использовать и возвращать объект, завернутый в разные типы, действуя как переходы состояний в конечном автомате , который сохраняет свое состояние как тип в контексте вызывающего объекта — typestate . API может использовать это для статического обеспечения того, чтобы его функции вызывались в правильном порядке.

Однако это не означает, что переменную нельзя использовать без ее использования:

// This function just borrows a coin: The ampersand means borrow.
fn validate(_: &Coin) -> Result<(), ()> { Ok(()) }

// The same coin variable can be used infinitely many times
// as long as it is not moved.
let coin = Coin{};
loop {
    validate(&coin)?;
}

Что Rust не может выразить, так это тип монеты, который не может выйти за рамки — для этого потребуется линейный тип.

Ресурсно-линейные типы

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

{
    // Must be passed on, not dropped.
    let token = HotPotato{};

    // Suppose not every branch does away with it:
    if (!queue.is_full()) {
        queue.push(token);
    }

    // Compilation error: Holding an undroppable object as the scope ends.
}

Привлекательность линейных типов заключается в том, что деструкторы становятся обычными функциями, которые могут принимать аргументы, могут давать сбои и так далее. Это может, например, избежать необходимости сохранять состояние, которое используется только для уничтожения. Общее преимущество явной передачи зависимостей функций заключается в том, что порядок вызовов функций (порядок уничтожения) становится статически проверяемым с точки зрения времени жизни аргументов. По сравнению с внутренними ссылками, это не требует пожизненных аннотаций, как в Rust.

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

Ресурсно-нормальные типы

Согласно интерпретации ресурса, нормальный тип не ограничивает количество раз, из которого можно перемещать переменную. C++ (в частности, семантика неразрушающего перемещения) попадает в эту категорию.

auto coin = std::unique_ptr<Coin>();
auto candy = buy_candy(std::move(coin));
auto drink = buy_drink(std::move(coin)); // This is valid C++.

Языки программирования

Следующие языки программирования поддерживают линейные или аффинные типы. :

• АТС
• Чистый
• Идрис
• Меркурий
• Ф*
• ЛинейныйML
• Милостыня
• Haskell с компилятором Glasgow Haskell (GHC) 9.0.1 или выше
• Гранулы
• Ржавчина
• Свифт 5.9 и выше

См. также

• Система эффектов
• Линейная логика
• Аффинная логика