Система субструктурных типов
| Типовые системы |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
Системы субструктурных типов — это семейство систем типов, аналогичных субструктурной логике , где одно или несколько структурных правил отсутствуют или допускаются только при контролируемых обстоятельствах. Такие системы могут ограничивать доступ к системным ресурсам, таким как файлы , блокировки и память , отслеживая изменения состояния и запрещая недопустимые состояния. [1] : 4
Различные системы подструктурного типа
[ редактировать ]Несколько типовых систем возникли в результате отказа от некоторых структурных правил обмена, ослабления и сжатия:
| Обмен | Ослабление | Сокращение | Использовать | |
|---|---|---|---|---|
| Заказал | — | — | — | Ровно один раз по порядку |
| Линейный | Допустимый | — | — | Ровно один раз |
| Аффинный | Допустимый | Допустимый | — | Максимум один раз |
| Соответствующий | Допустимый | — | Допустимый | Хотя бы один раз |
| Нормальный | Допустимый | Допустимый | Допустимый | Произвольно |
- Системы упорядоченного типа (обмен отбрасыванием, ослабление и сжатие): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
- Системы линейного типа (допускают обмен, но не ослабляют и не сокращают): каждая переменная используется ровно один раз.
- Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
- Соответствующие системы типов (допускаются обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
- Системы нормального типа (допускают обмен, ослабление и сжатие): каждая переменная может использоваться произвольно.
Объяснение систем аффинных типов лучше всего понять, если перефразировать его следующим образом: «каждое появление переменной используется не более одного раза».
Система упорядоченного типа
[ редактировать ]Упорядоченные типы соответствуют некоммутативной логике, где обмен, сжатие и ослабление отбрасываются. Это можно использовать для моделирования распределения памяти на основе стека (в отличие от линейных типов, которые можно использовать для моделирования распределения памяти на основе кучи ). [1] : 30–31 Без свойства обмена объект можно использовать только тогда, когда он находится на вершине смоделированного стека, после чего он удаляется, в результате чего каждая переменная используется ровно один раз в том порядке, в котором она была введена.
Системы линейного типа
[ редактировать ]Линейные типы соответствуют линейной логике и гарантируют, что объекты используются ровно один раз. Это позволяет системе безопасно освободить объект после его использования. [1] : 6 или для разработки программных интерфейсов , которые гарантируют, что ресурс не может быть использован после его закрытия или перехода в другое состояние. [2]
Язык программирования Clean использует типы уникальности (вариант линейных типов) для поддержки параллелизма, ввода/вывода на месте и обновления массивов . [1] : 43
Системы линейных типов допускают ссылки , но не псевдонимы . Чтобы обеспечить это, ссылка выходит за пределы области действия после появления в правой части присваивания , тем самым гарантируя, что одновременно существует только одна ссылка на любой объект. Обратите внимание, что передача ссылки в качестве аргумента функции . является формой присваивания, поскольку параметру функции будет присвоено значение внутри функции, и поэтому такое использование ссылки также приводит к ее выходу за пределы области действия
Свойство одиночной ссылки делает системы линейного типа пригодными в качестве языков программирования для квантовых вычислений , поскольку оно отражает теорему о запрете клонирования квантовых состояний. С точки зрения теории категорий , отказ от клонирования — это утверждение о том, что не существует диагонального функтора , который мог бы дублировать состояния; аналогично, с точки зрения комбинаторной логики , не существует K-комбинатора, который мог бы разрушать состояния. С точки зрения лямбда-исчисления переменная x может появляться ровно один раз в термине. [3]
Системы линейных типов являются внутренним языком закрытых симметричных моноидальных категорий , во многом так же, как просто типизированное лямбда-исчисление является языком декартовых замкнутых категорий . Точнее, можно построить функторы между категорией систем линейного типа и категорией замкнутых симметричных моноидальных категорий. [4]
Системы аффинного типа
[ редактировать ]Аффинные типы — это версия линейных типов, позволяющая отбрасывать (т.е. не использовать ) ресурс, соответствующий аффинной логике . Аффинный ресурс можно использовать не более одного раза, а линейный — один ровно раз .
Соответствующая система типов
[ редактировать ]Соответствующие типы соответствуют соответствующей логике, которая допускает обмен и сжатие, но не ослабление, что означает, что каждая переменная используется хотя бы один раз.
Интерпретация ресурса
[ редактировать ]Номенклатура, предлагаемая системами субструктурных типов, полезна для характеристики аспектов управления ресурсами языка. Управление ресурсами — это аспект языковой безопасности, обеспечивающий каждого выделенного ресурса освобождение ровно один раз. Таким образом, интерпретация ресурса касается только использования, которое передает право собственности – перемещение , где право собственности – это ответственность за освобождение ресурса.
Использование, которое не передает право собственности ( заимствование ), не входит в сферу применения этой интерпретации, но семантика срока службы еще больше ограничивает эти использования между распределением и освобождением.
| Отказ от движения | Обязательный ход | Переместить количественную оценку | Принудительный конечный автомат вызова функции | |
|---|---|---|---|---|
| Нормальный тип | Нет | Нет | Любое количество раз | Топологическое упорядочение |
| Аффинный тип | Да | Нет | Максимум один раз | Заказ |
| Линейный тип | Да | Да | Ровно один раз | Заказ и завершение |
Ресурсно-аффинные типы
[ редактировать ]Согласно интерпретации ресурса, аффинный тип не может быть потрачен более одного раза.
Как пример, один и тот же вариант торгового автомата Хоара можно выразить на английском, логике и на 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.
}
Привлекательность линейных типов заключается в том, что деструкторы становятся обычными функциями, которые могут принимать аргументы, могут давать сбои и так далее. [5] Это может, например, избежать необходимости сохранять состояние, которое используется только для уничтожения. Общее преимущество явной передачи зависимостей функций заключается в том, что порядок вызовов функций (порядок уничтожения) становится статически проверяемым с точки зрения времени жизни аргументов. По сравнению с внутренними ссылками, это не требует пожизненных аннотаций, как в Rust.
Как и в случае с ручным управлением ресурсами, практическая проблема заключается в том, что любой ранний возврат , что типично для обработки ошибок, должен привести к такой же очистке. Это становится педантично в языках, в которых есть размотка стека , где каждый вызов функции является потенциальным ранним возвратом. Однако, если провести близкую аналогию, семантика неявно вставленных вызовов деструктора может быть восстановлена с помощью отложенных вызовов функций. [6]
Ресурсно-нормальные типы
[ редактировать ]Согласно интерпретации ресурса, нормальный тип не ограничивает количество раз, из которого можно перемещать переменную. 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++.
Языки программирования
[ редактировать ]Следующие языки программирования поддерживают линейные или аффинные типы. [ нужна ссылка ] :
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Перейти обратно: а б с д Уокер, Дэвид (2002). «Системы субструктурного типа». В Пирсе, Бенджамин К. (ред.). Расширенные темы по типам и языкам программирования (PDF) . МТИ Пресс. стр. 3–43. ISBN 0-262-16228-8 .
- ^ Бернарди, Жан-Филипп; Беспфлюг, Матье; Ньютон, Райан Р.; Пейтон Джонс, Саймон ; Спивак, Арно (2017). «Линейный Haskell: практическая линейность в полиморфном языке высшего порядка» . Труды ACM по языкам программирования . 2 : 1–29. arXiv : 1710.09756 . дои : 10.1145/3158093 . S2CID 9019395 .
- ^ Баэз, Джон К.; Останься, Майк (2010). «Физика, топология, логика и вычисления: Розеттский камень». В Спрингере (ред.). Новые структуры для физики (PDF) . стр. 95–174.
- ^ Эмблер, С. (1991). Логика первого порядка в симметричных моноидальных замкнутых категориях (доктор философии). Университет Эдинбурга.
- ^ «Видение Вейла» . Проверено 6 декабря 2023 г.
Высший RAII — форма линейной типизации, позволяющая использовать деструкторы с параметрами и возвращаемыми значениями.
- ^ «Идите по примеру: отложите» . Проверено 5 декабря 2023 г.
Defer используется для обеспечения того, чтобы вызов функции выполнялся позже во время выполнения программы, обычно в целях очистки. defer часто используется, например, в обеспечении и, наконец, будет использоваться в других языках.
- ^ «6.4.19. Линейные типы — Glasgow Haskell Compiler 9.7.20230513 Руководство пользователя» . ghc.gitlab.haskell.org . Проверено 14 мая 2023 г.
- ^ [1]