Система субструктурного типа - Substructural type system
| Системы типов |
|---|
| Общие понятия |
| Основные категории |
|
| Второстепенные категории |
Системы субструктурных типов - это семейство систем типов, аналогичных субструктурной логике, где одно или несколько структурных правил отсутствуют или разрешены только при контролируемых обстоятельствах. Такие системы полезны для ограничения доступа к системным ресурсам, таким как файлы , блокировки и память, путем отслеживания происходящих изменений состояния и предотвращения недопустимых состояний.
Различные системы субструктурного типа
Несколько систем типов возникли за счет отказа от некоторых структурных правил обмена, ослабления и сжатия:
| Обмен | Ослабление | Сокращение | Использовать | |
|---|---|---|---|---|
| Заказал | - | - | - | Ровно один раз по порядку |
| Линейный | Разрешается | - | - | Ровно один раз |
| Аффинный | Разрешается | Разрешается | - | Не более одного раза |
| Соответствующие | Разрешается | - | Разрешается | Хотя бы один раз |
| Обычный | Разрешается | Разрешается | Разрешается | Произвольно |
- Системы упорядоченного типа (отказ от обмена, ослабления и сжатия): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
- Системы линейного типа (допускают обмен, но не ослабляют и не сужают): каждая переменная используется ровно один раз.
- Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
- Соответствующие системы типов (допускают обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
- Системы нормального типа (допускают обмен, ослабление и сжатие): любая переменная может использоваться произвольно.
Объяснение систем аффинных типов лучше всего понять, если перефразировать его следующим образом: «каждое вхождение переменной используется не более одного раза».
Система упорядоченного типа
Упорядоченные типы соответствуют некоммутативной логике , в которой отбрасываются обмен, сжатие и ослабление. Это можно использовать для моделирования выделения памяти на основе стека (в отличие от линейных типов, которые можно использовать для моделирования выделения памяти на основе кучи). Без свойства обмена объект может использоваться только тогда, когда он находится наверху смоделированного стека, после чего он выталкивается, в результате чего каждая переменная используется ровно один раз в том порядке, в котором она была введена.
Системы линейного типа
Линейные типы соответствуют линейной логике и гарантируют, что объекты используются ровно один раз, позволяя системе безопасно освободить объект после его использования.
Язык программирования Clean использует типы уникальности (вариант линейных типов) для поддержки параллелизма, ввода / вывода и обновления массивов на месте.
Системы линейных типов допускают ссылки, но не псевдонимы . Чтобы обеспечить это, ссылка выходит за пределы области действия после появления в правой части присваивания , таким образом гарантируя, что одновременно существует только одна ссылка на любой объект. Следует отметить , что передачи ссылки в качестве аргумента к функции является формой присвоения, так как параметр функции будет присвоено значение внутри функции, и , следовательно , такое использование в качестве ссылки , также заставляет его выходить из сферы.
Линейная система типа похож на C ++ «s unique_ptr класс , который ведет себя как указатель , но может быть перемещен только (т.е. не копируется) в назначении. Хотя ограничение линейности проверяется во время компиляции , разыменование недействительного unique_ptr вызывает неопределенное поведение во время выполнения .
Свойство единой ссылки делает системы линейного типа подходящими в качестве языков программирования для квантовых вычислений , поскольку оно отражает теорему о запрете клонирования квантовых состояний. С точки зрения теории категорий , запрет на клонирование - это утверждение, что не существует диагонального функтора, который мог бы дублировать состояния; аналогично, с точки зрения комбинатора , не существует K-комбинатора, который может разрушать состояния. С точки зрения лямбда-исчисления , переменная x может появляться в терме ровно один раз.
Линейные системы типа являются внутренний язык из замкнутых симметричных моноидальных категорий , во многом таким же образом , что просто напечатал лямбда - исчисление является языком декартово замкнутых категорий . Точнее, можно построить функторы между категорией систем линейного типа и категорией замкнутых симметрических моноидальных категорий.
Системы аффинного типа
Аффинные типы - это версия линейных типов, позволяющая отбрасывать (т.е. не использовать ) ресурс, соответствующий аффинной логике . Аффинное ресурс может быть использован в самых раз, в то время как линейный один должен быть использован точно один раз.
Соответствующая система типов
Соответствующие типы соответствуют соответствующей логике, которая допускает обмен и сокращение, но не ослабление, что означает, что каждая переменная используется хотя бы один раз.
Языки программирования
Следующие языки программирования поддерживают линейные или аффинные типы:
Смотрите также
Примечания
использованная литература
- Уокер, Дэвид (2002). «Системы субструктурного типа». В Пирсе, Бенджамине С. (ред.). Дополнительные темы по типам и языкам программирования (PDF) . MIT Press. С. 3–43. ISBN 0-262-16228-8.
