Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Системы типов
Общие понятия
Основные категории
Второстепенные категории
Смотрите также

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

Различные системы субструктурного типа [ править ]

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

ОбменОслаблениеСокращениеИспользовать
Упорядоченный---Ровно один раз по порядку
ЛинейныйРазрешается--Ровно один раз
АффинныйРазрешаетсяРазрешается-Не более одного раза
УместнымРазрешается-РазрешаетсяХотя бы один раз
ОбычныйРазрешаетсяРазрешаетсяРазрешаетсяПроизвольно
  • Системы упорядоченного типа (отказ от обмена, ослабления и сжатия): каждая переменная используется ровно один раз в том порядке, в котором она была введена.
  • Системы линейного типа (допускают обмен, но не ослабляют и не сужают): каждая переменная используется только один раз.
  • Системы аффинного типа (допускают обмен и ослабление, но не сокращение): каждая переменная используется не более одного раза.
  • Соответствующие системы типов (допускают обмен и сокращение, но не ослабление): каждая переменная используется хотя бы один раз.
  • Системы нормального типа (допускают обмен, ослабление и сжатие): любая переменная может использоваться произвольно.

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

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

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

Системы линейного типа [ править ]

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

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

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

Линейная система типа похож на C ++ «s unique_ptr класс , который ведет себя как указатель , но может быть перемещен только (т.е. не копируется) в назначении. Хотя ограничение линейности проверяется во время компиляции , разыменование недействительного unique_ptr вызывает неопределенное поведение во время выполнения . [6]

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

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

Системы аффинных типов [ править ]

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

Соответствующая система типов [ править ]

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

Языки программирования [ править ]

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

  • АТС
  • Чистый
  • Идрис
  • Меркурий
  • Ржавчина
  • F *
  • LinearML
  • Милостыня
  • Haskell с GHC 9.0 или новее
  • Гранула

См. Также [ править ]

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

Заметки [ править ]

  1. Перейти ↑ Walker 2002 , p. ИКС.
  2. Перейти ↑ Walker 2002 , p. 4.
  3. Перейти ↑ Walker 2002 , pp. 30–31.
  4. Перейти ↑ Walker 2002 , p. 6.
  5. Перейти ↑ Walker 2002 , p. 43.
  6. ^ std :: unique_ptr ссылка
  7. ^ Джон c. Баез и Майк Стей, " Физика, топология, логика и вычисления: Розеттский камень ", (2009) ArXiv 0903.0340 в New Structures for Physics , ed. Боб Кук, Lecture Notes in Physics vol. 813 , Springer, Берлин, 2011 г., стр. 95-174.
  8. ^ С. Амблер, " Логика первого порядка в симметричных моноидальных замкнутых категориях ", доктор философии. Диссертация, Университет Эдинбурга, 1991.

Ссылки [ править ]

  • Уокер, Дэвид (2002). «Системы субструктурного типа». В Пирсе, Бенджамине С. (ред.). Дополнительные темы по типам и языкам программирования (PDF) . MIT Press. С. 3–43. ISBN 0-262-16228-8. CS1 maint: обескураженный параметр ( ссылка )