Эта статья в значительной степени или полностью основана на одном источнике . ( февраль 2018 г. ) |
Системы типов |
---|
Общие понятия |
Основные категории |
Второстепенные категории |
Смотрите также |
Системы субструктурных типов - это семейство систем типов, аналогичных субструктурной логике, где одно или несколько структурных правил отсутствуют или разрешены только при контролируемых обстоятельствах. Такие системы полезны для ограничения доступа к системным ресурсам, таким как файлы , блокировки и память, путем отслеживания происходящих изменений состояния и предотвращения недопустимых состояний. [1] [2]
Различные системы субструктурного типа [ править ]
Несколько систем типов возникли за счет отказа от некоторых структурных правил обмена, ослабления и сжатия:
Обмен | Ослабление | Сокращение | Использовать | |
---|---|---|---|---|
Упорядоченный | - | - | - | Ровно один раз по порядку |
Линейный | Разрешается | - | - | Ровно один раз |
Аффинный | Разрешается | Разрешается | - | Не более одного раза |
Уместным | Разрешается | - | Разрешается | Хотя бы один раз |
Обычный | Разрешается | Разрешается | Разрешается | Произвольно |
- Системы упорядоченного типа (отказ от обмена, ослабления и сжатия): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
- Системы линейного типа (допускают обмен, но не ослабляют и не сужают): каждая переменная используется ровно один раз.
- Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
- Соответствующие системы типов (допускают обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
- Системы нормального типа (допускают обмен, ослабление и сжатие): любая переменная может использоваться произвольно.
Объяснение систем аффинных типов лучше всего понять, если перефразировать его следующим образом: «каждое вхождение переменной используется не более одного раза».
Система упорядоченного типа [ править ]
Упорядоченные типы соответствуют некоммутативной логике , в которой отбрасываются обмен, сжатие и ослабление. Это можно использовать для моделирования распределения памяти на основе стека (в отличие от линейных типов, которые можно использовать для моделирования распределения памяти на основе кучи). [3] Без свойства обмена объект может использоваться только тогда, когда он находится наверху смоделированного стека, после чего он выталкивается, в результате чего каждая переменная используется ровно один раз в том порядке, в котором она была введена.
Системы линейного типа [ править ]
Линейные типы соответствуют линейной логике и гарантируют, что объекты используются ровно один раз, что позволяет системе безопасно освободить объект после его использования. [4]
Язык программирования Clean использует типы уникальности (вариант линейных типов) для поддержки параллелизма, ввода / вывода и обновления массивов на месте. [5]
Системы линейных типов допускают ссылки, но не псевдонимы . Чтобы обеспечить это, ссылка выходит за пределы области действия после появления в правой части присваивания , таким образом гарантируя, что одновременно существует только одна ссылка на любой объект. Следует отметить , что передачи ссылки в качестве аргумента к функции является формой присвоения, так как параметр функции будет присвоено значение внутри функции, и , следовательно , такое использование в качестве ссылки , также заставляет его выходить из сферы.
Линейная система типа похож на C ++ «s unique_ptr класс , который ведет себя как указатель , но может быть перемещен только (т.е. не копируется) в назначении. Хотя ограничение линейности проверяется во время компиляции , разыменование недействительного unique_ptr вызывает неопределенное поведение во время выполнения . [6]
Свойство единой ссылки делает системы линейного типа подходящими в качестве языков программирования для квантовых вычислений , поскольку оно отражает теорему о запрете клонирования квантовых состояний. С точки зрения теории категорий , запрет на клонирование - это утверждение, что не существует диагонального функтора, который мог бы дублировать состояния; аналогично, с точки зрения комбинатора , не существует K-комбинатора, который может разрушать состояния. С точки зрения лямбда-исчисления , переменная x может появляться в терме ровно один раз. [7]
Линейные системы типа являются внутренний язык из замкнутых симметричных моноидальных категорий , во многом таким же образом , что просто напечатал лямбда - исчисление является языком декартово замкнутых категорий . Точнее, можно построить функторы между категорией систем линейного типа и категорией замкнутых симметрических моноидальных категорий. [8]
Системы аффинных типов [ править ]
Аффинные типы - это версия линейных типов, позволяющая отбрасывать (т.е. не использовать ) ресурс, соответствующий аффинной логике . Аффинное ресурс может быть использован в самых раз, в то время как линейный один должен быть использован точно один раз.
Соответствующая система типов [ править ]
Соответствующие типы соответствуют соответствующей логике, которая допускает обмен и сокращение, но не ослабление, что означает, что каждая переменная используется хотя бы один раз.
Языки программирования [ править ]
Следующие языки программирования поддерживают линейные или аффинные типы:
- АТС
- Чистый
- Идрис
- Меркурий
- Ржавчина
- F *
- LinearML
- Милостыня
- Haskell с GHC 9.0 или новее
- Гранула
См. Также [ править ]
- Система эффектов
- Линейная логика
- Аффинная логика
Заметки [ править ]
- Перейти ↑ Walker 2002 , p. ИКС.
- Перейти ↑ Walker 2002 , p. 4.
- Перейти ↑ Walker 2002 , pp. 30–31.
- Перейти ↑ Walker 2002 , p. 6.
- Перейти ↑ Walker 2002 , p. 43.
- ^ std :: unique_ptr ссылка
- ^ Джон c. Баез и Майк Стей, " Физика, топология, логика и вычисления: Розеттский камень ", (2009) ArXiv 0903.0340 в New Structures for Physics , ed. Боб Кук, Lecture Notes in Physics vol. 813 , Springer, Берлин, 2011 г., стр. 95-174.
- ^ С. Амблер, " Логика первого порядка в симметричных моноидальных замкнутых категориях ", доктор философии. Диссертация, Университет Эдинбурга, 1991.
Ссылки [ править ]
- Уокер, Дэвид (2002). «Системы субструктурного типа». В Пирсе, Бенджамине С. (ред.). Дополнительные темы по типам и языкам программирования (PDF) . MIT Press. С. 3–43. ISBN 0-262-16228-8. CS1 maint: обескураженный параметр ( ссылка )