Система субструктурных типов
| Типовые системы |
|---|
| Общие понятия |
| Основные категории |
| Второстепенные категории |
Системы субструктурных типов — это семейство систем типов, аналогичных субструктурной логике , где одно или несколько структурных правил отсутствуют или допускаются только при контролируемых обстоятельствах. Такие системы могут ограничивать доступ к системным ресурсам, таким как файлы , блокировки и память , отслеживая изменения состояния и запрещая недопустимые состояния. [1] : 4
системы субструктурного Различные типа
Несколько типовых систем возникли в результате отказа от некоторых структурных правил обмена, ослабления и сжатия:
| Обмен | Ослабление | Сокращение | Использовать | |
|---|---|---|---|---|
| Заказал | — | — | — | Ровно один раз по порядку |
| Линейный | Допустимый | — | — | Ровно один раз |
| Аффинный | Допустимый | Допустимый | — | Максимум один раз |
| Соответствующий | Допустимый | — | Допустимый | Хотя бы один раз |
| Нормальный | Допустимый | Допустимый | Допустимый | Произвольно |
- Системы упорядоченного типа (обмен отбрасыванием, ослабление и сжатие): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
- Системы линейного типа (допускают обмен, но не ослабляют и не сокращают): каждая переменная используется ровно один раз.
- Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
- Соответствующие системы типов (допускаются обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
- Системы нормального типа (допускают обмен, ослабление и сжатие): каждая переменная может использоваться произвольно.
Объяснение систем аффинных типов лучше всего понять, если перефразировать его следующим образом: «каждое появление переменной используется не более одного раза».
Система упорядоченного типа [ править ]
Упорядоченные типы соответствуют некоммутативной логике , в которой отбрасываются обмен, сжатие и ослабление. Это можно использовать для моделирования распределения памяти на основе стека (в отличие от линейных типов, которые можно использовать для моделирования распределения памяти на основе кучи ). [1] : 30–31 Без свойства обмена объект можно использовать только тогда, когда он находится на вершине смоделированного стека, после чего он удаляется, в результате чего каждая переменная используется ровно один раз в том порядке, в котором она была введена.
Системы линейного типа [ править ]
Линейные типы соответствуют линейной логике и гарантируют, что объекты используются ровно один раз. Это позволяет системе безопасно освободить объект после его использования. [1] : 6 или для разработки программных интерфейсов , которые гарантируют, что ресурс не может быть использован после его закрытия или перехода в другое состояние. [2]
Язык программирования Clean использует типы уникальности (вариант линейных типов) для поддержки параллелизма, ввода/вывода на месте и обновления массивов . [1] : 43
Системы линейных типов допускают ссылки , но не псевдонимы . Чтобы обеспечить это, ссылка выходит за пределы области действия после появления в правой части присваивания , тем самым гарантируя, что одновременно существует только одна ссылка на любой объект. Обратите внимание, что передача ссылки в качестве аргумента функции . является формой присваивания, поскольку параметру функции будет присвоено значение внутри функции, и поэтому такое использование ссылки также приводит к ее выходу за пределы области действия
Свойство единственной ссылки делает системы линейного типа пригодными в качестве языков программирования для квантовых вычислений , поскольку оно отражает теорему о запрете клонирования квантовых состояний. С точки зрения теории категорий , отказ от клонирования — это утверждение о том, что не существует диагонального функтора , который мог бы дублировать состояния; аналогично, с точки зрения комбинаторной логики , не существует K-комбинатора, который мог бы разрушать состояния. С точки зрения лямбда-исчисления переменная x может появляться ровно один раз в термине. [3]
Системы линейных типов являются внутренним языком закрытых симметричных моноидальных категорий , во многом так же, как просто типизированное лямбда-исчисление является языком декартовых замкнутых категорий . Точнее, можно построить функторы между категорией систем линейного типа и категорией замкнутых симметричных моноидальных категорий. [4]
Системы аффинных типов [ править ]
Аффинные типы — это версия линейных типов, позволяющая отбрасывать (т.е. не использовать ) ресурс, соответствующий аффинной логике . Аффинный ресурс можно использовать не более одного раза, а линейный — один ровно раз .
Соответствующая система типов [ править ]
Соответствующие типы соответствуют соответствующей логике, которая допускает обмен и сжатие, но не ослабление, что означает, что каждая переменная используется хотя бы один раз.
Интерпретация ресурса [ править ]
Номенклатура, предлагаемая системами субструктурных типов, полезна для характеристики аспектов управления ресурсами языка.Управление ресурсами — это аспект языковой безопасности, обеспечивающий каждого выделенного ресурса освобождение ровно один раз.Таким образом, интерпретация ресурса касается только использования, которое передает право собственности – перемещение , где право собственности – это ответственность за освобождение ресурса.
Использование без передачи права собственности ( заимствование ) не входит в сферу применения этой интерпретации, но семантика срока службы еще больше ограничивает эти виды использования между распределением и освобождением.
| Отказ от движения | Обязательный ход | Переместить количественную оценку | Принудительный конечный автомат вызова функции | |
|---|---|---|---|---|
| Нормальный тип | Нет | Нет | Любое количество раз | Топологическое упорядочение |
| Аффинный тип | Да | Нет | Максимум один раз | Заказ |
| Линейный тип | Да | Да | Ровно один раз | Заказ и завершение |
Ресурсно-аффинные типы [ править ]
Согласно интерпретации ресурса, аффинный тип не может быть потрачен более одного раза.
Как пример, один и тот же вариант торгового автомата Хоара можно выразить на английском, логике и на Rust :
| Английский | Логика | Ржавчина |
|---|---|---|
| Монета может купить тебя конфета, напиток, или выйти за рамки. | Монета ⊸ Конфеты Монета ⊸ Напиток Монета ⊸ ⊤ | fn buy_candy ( _ : Монета ) -> Конфета { Конфета {} } fn buy_drink ( _ : Монета ) -> Напиток { Напиток {} } |
Что это значит для В этом примере монета должна быть аффинным типом (что так и есть, если только она не реализует Признак копирования ) заключается в том, что попытка потратить одну и ту же монету дважды — это недопустимая программа, которую компилятор имеет право отклонить:
пусть монета = Монета {}; пусть конфеты = buy_candy ( монета ); // Здесь заканчивается время жизни переменной coin. пусть напиток = buy_drink ( монета ); // Ошибка компиляции: использование перемещенной переменной, не имеющей свойства Copy. Другими словами, система аффинных типов может выражать шаблон состояния типов :Функции могут использовать и возвращать объект, завернутый в разные типы, действуя как переходы состояний в конечном автомате , который сохраняет свое состояние как тип в контексте вызывающего объекта — typestate . API может использовать это для статического обеспечения того, чтобы его функции вызывались в правильном порядке.
Однако это не означает, что переменную нельзя использовать без ее использования:
// Эта функция просто заимствует монету: амперсанд означает заимствование. fn validate ( _ : & Coin ) -> Result < (), () > { Ok (()) } // Одна и та же переменная монеты может использоваться бесконечно много раз // до тех пор, пока она не будет перемещена. пусть монета = Монета {}; цикл { проверить ( & монету ) ? ; } Что Rust не может выразить, так это тип монеты, который не может выйти за рамки — для этого потребуется линейный тип.
Ресурсно-линейные типы [ править ]
Согласно интерпретации ресурса, линейный тип не только может быть перемещен, как и аффинный тип, но и должен быть перемещен — выход за пределы области действия является недопустимой программой.
{ // Должен передаваться, а не удаляться. пусть токен = HotPotato {}; // Предположим, что не каждая ветка покончила с этим: if ( ! очереди . is_full ()) { очередь . нажать ( токен ); } // Ошибка компиляции: удержание неудаляемого объекта по окончании области видимости. } Привлекательность линейных типов заключается в том, что деструкторы становятся обычными функциями, которые могут принимать аргументы, могут давать сбои и т. д. [5] Это может, например, избежать необходимости сохранять состояние, которое используется только для уничтожения. Общее преимущество явной передачи зависимостей функций заключается в том, что порядок вызовов функций (порядок уничтожения) становится статически проверяемым с точки зрения времени жизни аргументов. По сравнению с внутренними ссылками, это не требует пожизненных аннотаций, как в Rust.
Как и в случае с ручным управлением ресурсами, практическая проблема заключается в том, что любой ранний возврат , что типично для обработки ошибок, должен привести к такой же очистке. Это становится педантично в языках, в которых есть размотка стека , где каждый вызов функции является потенциальным ранним возвратом. Однако, если провести близкую аналогию, семантика неявно вставленных вызовов деструктора может быть восстановлена с помощью отложенных вызовов функций. [6]
Ресурсно-нормальные типы [ править ]
Согласно интерпретации ресурса, нормальный тип не ограничивает количество раз, из которого можно перемещать переменную. C++ (в частности, семантика неразрушающего перемещения) попадает в эту категорию.
auto coin = std :: unique_ptr <Coin> ; ) ( auto candy = buy_candy ( std :: move ( монета )); auto Drink = buy_drink ( std :: move ( монета )); // Это допустимо для 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]