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