Система субструктурного типа - Substructural type system

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

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

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


	Обмен	Ослабление	Сокращение	Использовать
Упорядоченный	—	—	—	Ровно один раз по порядку
Линейный	Допустимый	—	—	Ровно один раз
Аффинный	Допустимый	Допустимый	—	Максимум однажды
Соответствующий	Допустимый	—	Допустимый	Хотя бы один раз
Нормальный	Допустимый	Допустимый	Допустимый	Произвольно

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

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

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

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

Системы линейного типа

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

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

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

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

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

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

Системы аффинного типа

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

Соответствующая система типов

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

Языки программирования

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

Смотрите также

Примечания

^ Уокер 2002, п. ИКС.
^ Уокер 2002, п. 4.
^ Уокер 2002 С. 30–31.
^ Уокер 2002, п. 6.
^ Уокер 2002, п. 43.
^ std :: unique_ptr ссылка
^ Джон с. Баэз и Майк Стэйт "Физика, топология, логика и вычисления: розеттский камень ", (2009) ArXiv 0903.0340 в Новые структуры для физики, изд. Боб Кок, Конспект лекций по физике т. 813, Springer, Берлин, 2011 г., стр. 95-174.
^ С. Эмблер "Логика первого порядка в симметричных моноидальных замкнутых категориях ", Докторская диссертация, Эдинбургский университет, 1991.