[Перевод] Rust: объясняем Владение и Субструктурные типы на пальцах

Системы типов помогают разработчикам создавать надежные и безопасные программы. Однако такие термины, как «субструктурные типы» или «владение», нередко кажутся сложными и трудными для понимания, особенно для тех, кто не сталкивался с теорией типов в академической среде.
Новый перевод от команды МойОфис расскажет вам, как субструктурные типы и система владения в Rust помогают создавать безопасные и эффективные программы. Автор разбирает ключевые теоретические аспекты, выясняет, какие преимущества они предоставляют, и показывает, почему их использование становится неотъемлемой частью разработки современных языков. Вы узнаете, как субструктурные типы помогают обеспечивать безопасность и жизнеспособность программ, а также познакомитесь с идеями и проблемами их внедрения на практике.
Цель этого материала — объяснить, как можно применить теорию системы субструктурных типов при создании языков программирования. Термины вроде «теория системы субструктурных типов» обычно пугают и сбивают с толку программистов, которые не пишут на Haskell по выходным. Поэтому, чтобы обычные программисты смогли понять принцип работы нового языка, его создатель должен придумать эффектные метафоры, пусть даже несколько вводящие в заблуждение. Один из таких терминов — «владение».
Довольно часто объекты в программе начинают представлять что-то за пределами самих себя; они не являются «чистыми данными», а скорее ресурсом с идентичностью (identity).
Классическим примером может служить дескриптор, предоставляющий эксклюзивный доступ к ресурсу.
Для успешной реализации этой функции нужно понимать, что:
Для получения этого объекта необходимо выполнить определенный код («конструктор»).
Когда объект больше не используется, будет выполнен другой код («деструктор»).
Пока объект находится в области видимости, никакой параллельно выполняющийся код не относится к объекту, представляющему тот же эксклюзивный ресурс (он не имеет псевдонимов).
Это и есть владение (по крайней мере, в том виде, в котором оно представлено в Rust).
Я хочу просто и доступно рассказать о таком явлении как владение и системе субструктурных типов, чтобы как можно больше людей смогли разобраться в том, что это такое. В этой статье нет сверхновых данных — если вы уже «в теме», то не найдете здесь новой информации. Но в ней есть несколько аспектов по работе с Rust, которые я считаю неверными (и один из них довольно легко исправить).
Системы типов и свойство корректности
Для начала я хочу сделать шаг назад и поискать ответ на более фундаментальный вопрос. Для чего нужна система типов?
Мне очень нравится то, как однажды это сформулировал Грейдон Хоар (хотя, думаю, что он сам пересказал чью-то мысль): системы типов — это те элементы формальных методов, которые мы научились упрощать. То есть система типов — это формальный (и, хочется надеяться, надежный) метод статического анализа, который автоматически применяется к вашей программе для проверки аспектов ее поведения. В формальном анализе было проведено важное различие между двумя видами свойств, которыми может обладать ваша программа:
Свойство безопасности, которое гарантирует, что «плохие вещи не происходят» (то есть ваша программа не демонстрирует определенное нежелательное поведение).
Свойство жизнеспособности, которое гарантирует, что «хорошие вещи происходят» (то есть ваша программа демонстрирует определенное желаемое поведение).
Обычно мы говорим о системах типов как о средствах обеспечения определенных свойств безопасности. Например, если у меня есть функция fn(String) -> Integer
, система типов обеспечит то, что моя программа никогда не вызовет эту функцию с аргументом, который не является String (или с двумя аргументами, или без аргументов и т.д.). Но система типов также обеспечивает некоторые свойства жизнеспособности: например, она гарантирует, что функция вернет целое число.
Однако свойство жизнеспособности может страдать из-за выразительности используемых нами языков. В частности, почти каждый широко используемый язык программирования обладает полнотой по Тьюрингу, и поэтому мы не можем гарантировать, что эта функция вернет целое число. Напротив, она может никогда не завершиться. Поэтому свойство жизнеспособности обычно понимается с оговоркой, что программа выполнит необходимое действие в конечном итоге, где «в конечном итоге» может быть где-то в бесконечном будущем.
В большинстве языков программирования также есть возможность прервать выполнение программы или сгенерировать нетипированное исключение, что является еще одной оговоркой, которую необходимо сделать в отношении любых гарантий жизнеспособности. Здесь много несовершенств, но таково текущее положение дел на практике.
Владение — это метод расширения системы типов языка, позволяющий обеспечить дополнительные гарантии безопасности и жизнеспособности программ, написанных на этом языке. В частности, относительно количества раз, которое будет использовано значение заданного типа.
Что такое субструктурные типы?
В математической логике существуют определенные виды универсальных правил, известные как «структурные правила», поскольку они являются частью структуры логики. Сегодня нам будут особенно интересны два из них:
Ослабление (или «монотонность следствия»): Если вы знаете, что A влечет за собой B
(A -> B
), можно утверждать, что A и любой другой факт также влекут за собой B (например,A, C -> B
). Это означает, что вы можете игнорировать ненужные предикаты в правиле.Сокращение (или «идемпотентность следствия»): Если вы знаете, что несколько A влекут за собой B (
A, A -> B
), можно утверждать, что единичная A тоже влечет за собой B (например,A -> B
). Это означает, что вам не нужны несколько одинаковых предикатов в правиле.
Можно построить другие виды логик, в которые эти структурные правила не входят. Например, в линейной логике нет ни одного из этих правил: вы не можете утверждать, что A, A, C -> B
или A -> B
только потому, что вы знаете, что A, A -> B
.
Некоторое время назад стало известно, что теории типов и математические логики тесно связаны. Люди, пишущие на Haskell, могут бесконечно об этом рассказывать — это и есть сущность «соответствия Карри-Говарда». На этой основе возникла идея создания систем типов, в которых также отсутствуют эти структурные правила. Как мне объяснил Аарон Турон (хотя я не изучал историю подробно), сначала это были чисто теоретические исследования без конкретных возможностей применения на практике. Однако эти исследования оказались очень полезными для представления тех видов объектов, которые я описал выше —объектов со значимым понятием идентичности.
«Субструктурный тип» — это тип, у которого удален эквивалент одного или обоих этих структурных правил. Как это понимать: в то время как значения обычных типов могут использоваться любое количество раз, значения субструктурных типов могут быть использованы ограниченное количество раз. Если тип нельзя «ослабить», он должен быть использован хотя бы один раз, прежде чем выйдет из области видимости. Если тип нельзя «сократить», его нельзя использовать более одного раза. Каждая из этих категорий типов имеет свое название, они приведены в этой таблице:
ОСЛАБЛЕНИЕ? | СОКРАЩЕНИЕ? | ИСПОЛЬЗОВАНИЕ | |
Обычные типы | ДА | ДА | Любое количество раз |
Аффинные типы | ДА | Не более одного раза | |
Релевантные типы | ДА | Хотя бы один раз | |
Линейные типы | Только один раз |
В текущей версии Rust все типы подчиняются закону ослабления, но по умолчанию не подчиняются закону сокращения. Поэтому большинство типов в Rust называются аффинными типами, и их можно использовать только один раз или ни разу. Использовать их — значит перемещать; не использовать — значит удалить. Именно это мы называем владением.
Rust также поддерживает обычные типы, которые можно использовать любое количество раз. Сейчас это типы, реализующие Copy
. Это приводит к тому, что у Rust есть одна особенность: все обычные типы должны быть копируемыми путем использования memcpy. Другие типы, которые в других языках были бы обычными типами, реализуют трейт Clone
, который придает им семантику обычного типа, но требует добавлять вызов clone
каждый раз, когда вы хотите переместить их более одного раза. Это сделано для того, чтобы «отговорить» вас выполнять дорогостоящие операции (например, копирование в диапазоне String
требует размещения новой сколь угодно большой кучи и копирования в нее данных). При этом некоторые memcpy являются затратными (большие), а какие-то копии — более простые (в частности, Rc
и Arc
). Недавно Нико Матсакис озвучил мысль о том, что это нужно изменить, чтобы уйти от жесткой связи между семантикой обычных типов и memcpy; я думаю, это отличное предложение, и я с нетерпением жду увидеть эти изменения в Rust.
Возвращаясь к обсуждению свойств безопасности и жизнеспособности, я хочу акцентировать внимание на том, что нам дало владение. Во-первых, оно дало нам гарантию того, что для значения не заданы псевдонимы где-либо еще в программе. Это позволяет нам изменять его, сохраняя при этом свойство безопасности, заключающееся в отсутствии изменяемого состояния с возможностью задать псевдоним. Это критическая функция в Rust, которая гарантирует безопасность доступа к памяти, защиту от гонок данных и возможность локальных рассуждений.
И поскольку нам известно, что у значения нет псевдонимов, когда оно выходит из области видимости, мы знаем, что можем вызвать его деструктор. Мы можем закрыть файл, разблокировать мьютекс и так далее. Языки без владения не могут дать такую гарантию, так как для значения может быть задан псевдоним где-то еще. В некоторых языках реализованы неудачные и незавершенные решения этой проблемы (например, конструкция with
в Python). И хотя они помогают уменьшить количество ошибок, с которыми сталкиваются программисты, они не решают проблему полностью. Например, в Python все еще возможны ситуации, когда файл, открытый с помощью блока with
, выходит за пределы этого блока, поскольку ничто не мешает присвоить его переменной вне блока.
Линейные и сессионные типы
В Rust есть аффинные типы, но в нем все еще отсутствуют «неослабляемые» типы, то есть типы, которые должны быть использованы хотя бы раз. В итоге особое внимание привлекают «линейные типы», поскольку именно они должны быть использованы только один раз. Данный термин неверно используется некоторыми программистами Rust в отношении другого решения, связанного с утечками памяти (к этой теме еще вернемся в разделе, посвященному «совместному владению»).При этом он также применяется к линейным типам, которые также называются «перемещаемыми» (must move) или «неосвобождаемыми» (undroppable).
Сейчас добавление линейных типов в Rust кажется непростой задачей, но стоит обсудить их ценность для любого языка. Проще всего продемонстрировать их пользу на примере «сессионных» типов.
Цель сессионных типов заключается в использовании протокола с параллельно исполняемым процессом в системе типов так, чтобы можно было выполнять только те операции, которые разрешены в зависимости от текущего состояния данного параллельного процесса. Это что-то вроде реализации в языке «машины состояний», где каждое состояние представляет собой отдельный тип, и каждое изменение состояния реализуется через метод, возвращающий тип следующего состояния.
Разберем самый простой пример транзакции с двумя методами — commit (выполнить) и abort (прервать):
impl Transaction {
pub fn commit(self) -> TransactionResult;
pub fn abort(self);
}
Проблема этого сессионного типа в том, что программа может в любой момент просто освободить ресурс данной транзакции (то есть вызвать drop). На такой случай можно написать деструктор, скажете вы, и при освобождении ресурса транзакции вызвать abort (остановимся на этом подробнее в следующем разделе), но, согласитесь, бывают гораздо более сложные случаи, когда не столь очевидно, какие состояния необходимо изменить при освобождении ресурса.
Линейные типы решают проблему с освобождением ресурса сессионного типа, поскольку программа обязана использовать данный сессионный тип. Этот сессионный тип может быть использован через commit или abort либо перемещен (передан) в другую функцию. Что другая функция будет с ним делать? Она также может либо переместить (передать) его другой функции, либо вызвать commit или abort сама. В таком случае появляется гарантия, что тип будет существовать в памяти до тех пор, пока рано или поздно (обратите внимание «рано или поздно» также может означать «никогда») программа не вызовет commit или abort данной транзакции.
Если исследовать вопрос глубже, то обнаруживается изъян в реализации аффинных типов в Rust. Посмотрите на имплементацию commit и abort: они получают аргумент self
, имеющий тип Transaction
, который опять же является линейным типом. Это значит, что вышеуказанные методы также обязаны как-то использовать значение self. Очевидно, что это не может продолжаться до бесконечности.
Вторая задача для эффективной реализации линейных сессионных типов заключается в их деструктуризации (destructuring). Транзакционный тип представляет собой структуру (struct), которая содержит набор полей, причем эти поля могут быть представлены обычными или аффинными типами. В каждом из этих методов в определенный момент транзакционный тип должен быть деструктуризирован (разбит) на типы содержащихся в нем полей, которые используют транзакцию, но вместо транзакционного типа, они должны вернуть такие типы, которые можно спокойно освободить (то есть вызвать drop). Линейные типы следует реализовывать только так. Иначе пришлось бы хранить каждое значение когда-либо созданного линейного типа и возвращать их все через функцию main
!
Тем не менее, если есть возможность деструктуризировать транзакционный тип, то пропадает гарантия его существования в памяти и того, что будет можно вызвать commit или abort. Поэтому третья и последняя задача для обеспечения существования сессионного типа заключается в использовании приватности, которая предотвратит несанкционированную деструктуризацию (destructuring) сессионного типа другим кодом. Если поля транзакции будут приватными, тогда только методы ее же модуля смогут ее деструктуризировать. Таким образом, в библиотеке, которая предоставляет транзакционный тип, он может быть деструктуризирован исключительно через commit и abort, а значит, гарантируется существование типа в памяти, и программа, использующая данную библиотеку, в конечном итоге сможет вызвать commit или abort любой транзакции.
E0509
Типы с владением можно рассматривать как частный случай типа сеанса, который имеет допустимый «переход между состояниями по умолчанию». Этот переход между состояниями по умолчанию должен переходить в ()
(он не может возвращать ошибку или любое другое содержательное значение). И он вызывается каждый раз, когда значение выходит из области видимости без вызова других методов перехода (если таковые вообще есть). Мы называем этот переход между состояниями по умолчанию деструктором.
Мне кажется, именно в этом ключе стоит рассматривать типы с владением: они просто являются частным случаем типов сеансов, которые имеют деструктор по умолчанию. Это подводит нас к тому, что такой тип программы не принимает компилятор Rust. И мне кажется, компилятор Rust ошибается: невозможно деструктурировать тип, у которого есть деструктор. Код этой ошибки — E0509.
Если переход между состояниями типа сеанса — это просто метод, который потребляет тип сеанса и деструктурирует его, а деструктор — это просто метод автоматического перехода между состояниями, то деструктор — это тоже просто автоматический деструктуризатор. Ничто не помешает мне разложить его другим способом. Вполне возможно представить себе такую систему, в которой вы либо деструктурируете тип, либо вызываете деструктор. Но сегодня в Rust нет способа это реализовать, потому что если вы добавите деструктор к типу, вы не сможете его деструктурировать.
E0509 была добавлена на ранних этапах развития Rust, когда, как мне кажется, было меньше понимания о теоретических основах семантики перемещения (move semantics) и владения. Насколько я могу судить, мотивация была в том, что если вы добавляете деструктор к типу, вы хотите, чтобы этот деструктор вызывался, а если вы деструктурируете этот тип, то деструктор вызываться не будет. Но решение в этом случае такое же, как и для линейных типов: объединить деструктор с приватностью, чтобы деконструирование не использовалось для потребления типа.
Этот принцип применяется почти во всех типах с деструктором (у всех есть приватные поля), поэтому эта проблема возникает редко. Но у меня есть отличный пример от Дэвида Толнея — речь идет о ситуации в serde_json, когда от библиотеки потребовали совершить неудачный обходной путь, поскольку в ней есть тип, который в точности соответствует тому паттерну, который исключает E0509: тип, который должен быть потреблен путем его деструктуризации или запуска его индивидуального деструктора.
Этот тип — Value
, который служит для представления любого значения JSON. Это перечисление всех видов значений JSON (число, логическое значение, массив и так далее). Вы можете использовать его для преобразования JSON без предполагаемой схемы в значение, которое можно обойти с помощью match
и подобных методов.
Однако зачастую парсинг JSON осуществляется из ненадежных источников, и в результате, вполне вероятно, будет обнаружен некорректный JSON, что приведет к переполнению стека (stack overflow) простого деструктора. В качестве примера рассмотрим JSON [[[]]].
При парсинге в Value
мы получим массив, содержащий пустой массив. При наличии автоматически сгенерированного кода деструктора будут выполнены 3 вложенных вызова для освобождения памяти каждого варианта массива. Некорректная JSON-строка будет содержать достаточное количество вложенных массивов, чтобы переполнить стек при уничтожении значения такого типа. Поэтому для типа Value в serde_json предусмотрен кастомный деструктор, использующий форму оптимизации хвостовых вызовов, чтобы не допустить увеличения размера стека в глубину JSON.
Проблема в том, что если вы реализуете этот деструктор для типа Value
, то не сможете его деструктурировать. А ведь весь смысл Value
в том, чтобы деструктурировать его с помощью match!
Дэвид Толнай решил эту проблему, добавив кастомный тип Array
вместо использования Vec
, который имеет оптимизирующий деструктор хвостовых вызовов, но при этом усложняет API. Вместо этого следует удалить E0509 и дать возможность определять тип Value
с кастомным деструктором, не препятствуя пользователям в его деструктурировании.
Совместное владение и ссылки
Владение — это хорошо, но иногда возникает необходимость разрешить задавать псевдонимы для значений, на которые распространяется система владения. Один из способов реализовать это — иметь некий конструктор, который берет аффинный тип и производит обычный тип (или в случае с текущей версией Rust аффинный тип с Clone
для имитации семантики обычного типа). Это называется «совместное владение». Эти конструкции совместного владения будут отслеживать количество псевдонимов данного значения и запускать деструктор только после того, как последнее значение выйдет из области видимости.
Есть несколько важных моментов, о которых следует помнить, если вы хотите добавить функцию совместного владения в свой язык.
Во-первых, нельзя позволять изменять значение, на которое распространяется совместное владение, без синхронизации, так как это приведет к изменяемому состоянию с возможностью задавать псевдонимы. Поэтому если вы собираетесь добавить эту функцию, вам обязательно понадобится механизм контроля изменений.
Во-вторых, если в вашей системе общего владения не предусмотрен механизм прерывания циклов (как в случае с указателями с подсчетом ссылок (reference counting)), вы можете столкнуться с циклическими ссылками (cyclic references). Это приведет к тому, что значения будут утекать, а их деструкторы не будут вызываться. Это означает, что любая гарантия жизнеспособности в отношении выполнения деструкторов (или, в сущности, переходов линейных типов сессий) теперь должна упоминаться с оговоркой о возможности утечки значения. И если ваше решение прерывает циклы, но не гарантирует своевременной деаллокации значения (как в случае со сборщиками мусора с отслеживанием ссылок), это, скорее всего, вызовет проблемы с производительностью для некоторых деструкторов, например, для лок-гардов (объекты, которые автоматически освобождают мьютекс при выходе из области видимости) мьютексов. В целом, это довольно рискованная функция, и ее следует добавлять с осторожностью.
В Rust разрешены указатели со счетчиком ссылок без прерывания циклов, поэтому все гарантии, связанные с деструкторами, должны учитывать тот факт, что деструкторы могут не вызываться. Наметился интерес к изменению этой ситуации с тем, чтобы можно было определять типы, которым нельзя дать утечь («типы, которые нельзя утерять»), и которые, соответственно, нельзя безопасно использовать в конструкциях с общим владением. Как и в случае с линейными типами, добавление такого дифференцирования в язык на данном этапе было бы очень сложной задачей, но эта идея выглядит очень заманчивой.
Один из способов разрешить задавать значению псевдоним без противоречий с системой общего владения — это концепция ссылок. Оператор ссылки — это особый оператор, который производит действие со значением, но это не считается перемещением, поэтому значение остается на месте после присвоения ссылки. Общая ссылка может быть обычным типом, поэтому для нее можно задать псевдоним. Вы также можете добавить изменяемые ссылки, которые являются аффинными типами и допускают изменения, поскольку для них не задаются псевдонимы.
Если вы хотите использовать эту функцию, то должны гарантировать, что значение не будет использовано снова, пока существует ссылка, поскольку это сделает ее недействительной. В Rust это реализовано с помощью присвоения ссылкам «времени жизни» и «механизма заимствований», который проверяет правильность программы путем отслеживания этих жизненных циклов. Кроме того, это решение предотвращает появление циклических ссылок (cyclic references) благодаря самому принципу функционирования «времени жизни». Эта информация выходит за рамки данной публикации, но эти особенности очень часто рассматриваются вместе с системой владения как единая концепция «владения и заимствования».
Заключение
Могу сказать точно, что я бы не стал создавать новый язык программирования без субструктурных типов в какой-либо форме. Они гарантируют безопасность при использовании псевдонимов и жизнеспособность при переходах между состояниями. Надеюсь, мы увидим эти функции в новых языках, которые будут появляться в будущем.
Наконец, есть основания полагать, что участники проекта Rust (в особенности Нико Матсакис) видят смысл в изменении системы владения в этом языке. И при всей сложности реализации этих изменений, я уверен, это станет существенным улучшением. Rust только выиграет от внедрения линейных типов и от того, что обычные типы не будут привязаны к memcpy. Более простым изменением, которое также стоит рассмотреть, может стать удаление ошибки E0509, что позволит использовать типы с системой владения, которые можно деструктурировать.