Объекты в качестве параметров типов
Вот бывают в программировании типы с параметром, например тип List - это списки, у которых элементы типа T.
Функция, которая может работать со списком любого типа элементов, тоже имеет параметрический тип:
reverse(list : List) : List
В языках вроде Java параметром типа может быть только тип. Но когда система типов покруче, бывает что в качестве параметра выступает значение. Например бывают в математике такие матрицы n на m, где n и m натуральные числа, и вот для них удобно иметь тип Mat.
Умножать матрицы ведь можно только если количество столбцов в левой совпадает с количеством строк в правой.
multiply(a : Mat, b : Mat) : Mat
В общем полезная штука, когда в качестве параметра типа может фигурировать число или значение какого-нибудь иного типа.
Но осмысленно ли, чтобы в качестве параметра фигурировало не значение, а объект?
В 2016ом, когда я читал первый условно-публичный препринт МакБрайдовского опуса “I Got Plenty o' Nuttin'” на его гитхабе, я никак не мог придумать, зачем бы такое было нужно. И вот читая «Functional Ownership through Fractional Uniqueness» Маршалла и Орхарда я наконец понял, картанка сложилась.
Знаете, в языке Rust можно создать изменяемую переменную. Это как раз пример объекта (а не значения). Например, у нас будет тип MutStr, мутабельная переменная, хранящая строку.
Позже там можно создать на неё readonly-ссылки, и пока все ссылки назад не сдашь, она остаётся заблокированной на запись.
Теперь давайте придумаем как красиво на уровне системы типов принудить к такому поведению.
Для этого у нас будет тип ссылок только для чтения с дробными весами: ReadonlyStrRef,
где вес - положительное дробное число не более единицы.
Блокируя мутабельную переменную (запрещая запись в неё), мы будем получать ссылку на чтение веса 1:
lock(consume v : MutStr) : ReadonlyStrRef<1>
(Блокировка на уровне системы типов заключается в том, что эта операция поглощает нашу переменную v. Её больше нет в контексте и модифицировать нечего.)
Затем такие ссылки мы можем разбивать надвое. . То есть если r : ReadonlyStrRef, то есть поглащающая r операция split, которая возвращает две ссылки весом вполовину меньше:
let (a, b) = split(r),
где
a : ReadonlyStrRef
b : ReadonlyStrRef
(По факту веса ссылок у нас всегда будут диадическими числами, то есть рациональными числами, где в знаменателе степени двойки.)
Теперь давайте думать, как же “сдавать назад” ссылки, чтобы разблокировать переменную. Давайте просто наивно напишем:
join(x : ReadonlyStrRef, y : ReadonlyStrRef)
: ReadonlyStrRef
Так можно соединять ссылки назад, а когда мы назад собрали все получилась ссылка веса 1, и можно разлочить объект:
unlock(r : ReadonlyStrRef<1>) : MutStr
Кто внимательный, заметил проблемку. Мы можем по ошибке сджойнить ссылки на две совершенно разных переменных. Поэтому понадобится нам у ReadonlyStrRef ещё один параметр - собственно переменная, на которую мы ссылку сделали. ReadonlyStrRef.
Только я, если можно, буду вместо двухместрых сигнатур использовать запись origin.ReadonlyRef, представив что позаимствовали в языке Scala path dependent types.
И тогда корректные сигнатуры станут такие:
lock(v : Mut) : v.ReadonlyRef<1>
split(r : v.ReadonlyRef)
: (v.ReadonlyRef, v.ReadonlyRef)
join(x : v.)
join(x : v.ReadonlyRef, y : v.ReadonlyRef)
: v.ReadonlyRef
unlock>(r : v.ReadonlyRef<1>) : Mut
Важно отличать релевантное использование объекта (при котором объект вообще говоря консьюмится и становится недоступным) от использований в типовых аннотациях, при которых объект не консьюмится, а используется как абстрактное имя. Это то что у МакБрайда называлось в разных версиях статьи icon или ghost. Отметим также, что для использования функций join и unlock совершенно не нужно, чтобы объект v был внутри скоупа: он выводится унификацией параметров типов аргументов.
* * *
Мы тут пока рассуждали только о блокировке изменений переменной и получении на время блокировки реплицируемых readonly-ссылок.
Но возможна блокировка в другом смысле и получение accessors с другими capabilities: скажем можем мы сделать целочисленную переменную, и временно заблокировать как запись в неё напрямую, так и чтение из неё напрямую, получить реплицируемый accessor, позволяющий делать её инкремент (с репликацией тем же самым механизмом с дробными весами, split и join). Так мы получим Grow-only Counter, который нельзя ни считывать, ни сеттить пока кто-то может его инкрементить, а потом когда все “ручки, за которые можно инкрементить” сданы можно посмотреть сумму изменений. Разумеется, вместо Grow-only Counter подойдут любые CRDTы (Conflict-free replicated data type).
* * *
Читатель знакомый с concurrent separation logic заметит, что тройки (weight, original object, accessor capabilities) образуют тот самый частичный коммутативный моноид (PCM), описание которого в явном виде требуется для рассуждений о программе, если у нас появляются некие “вместилища объектов”, обеспечивающие возможность объектам выйти за локальный скоуп функции, где они были порождены.
В Rust'e таковы lifetimes для (мутабельных) переменных, в Kotlin'e coroutineScopes для джобов (запущенных корутин) - они позволяют объектам выйти за локальный скоуп, но всё ещё привязаны к лексическому скоупингу. Их кузены, не привязанные к лексическому скоупингу - персистентные вместищила объектов. Это Heap для переменных, Stage для акторов.
Получение вполне удовлетворительных теоретикотиповых описаний систем, где присутствуют такие сущности - важнейшая из не решенных на данный момент задач прикладной теории типов.
Функция, которая может работать со списком любого типа элементов, тоже имеет параметрический тип:
reverse(list : List) : List
В языках вроде Java параметром типа может быть только тип. Но когда система типов покруче, бывает что в качестве параметра выступает значение. Например бывают в математике такие матрицы n на m, где n и m натуральные числа, и вот для них удобно иметь тип Mat.
Умножать матрицы ведь можно только если количество столбцов в левой совпадает с количеством строк в правой.
multiply(a : Mat, b : Mat) : Mat
В общем полезная штука, когда в качестве параметра типа может фигурировать число или значение какого-нибудь иного типа.
Но осмысленно ли, чтобы в качестве параметра фигурировало не значение, а объект?
В 2016ом, когда я читал первый условно-публичный препринт МакБрайдовского опуса “I Got Plenty o' Nuttin'” на его гитхабе, я никак не мог придумать, зачем бы такое было нужно. И вот читая «Functional Ownership through Fractional Uniqueness» Маршалла и Орхарда я наконец понял, картанка сложилась.
Знаете, в языке Rust можно создать изменяемую переменную. Это как раз пример объекта (а не значения). Например, у нас будет тип MutStr, мутабельная переменная, хранящая строку.
Позже там можно создать на неё readonly-ссылки, и пока все ссылки назад не сдашь, она остаётся заблокированной на запись.
Теперь давайте придумаем как красиво на уровне системы типов принудить к такому поведению.
Для этого у нас будет тип ссылок только для чтения с дробными весами: ReadonlyStrRef,
где вес - положительное дробное число не более единицы.
Блокируя мутабельную переменную (запрещая запись в неё), мы будем получать ссылку на чтение веса 1:
lock(consume v : MutStr) : ReadonlyStrRef<1>
(Блокировка на уровне системы типов заключается в том, что эта операция поглощает нашу переменную v. Её больше нет в контексте и модифицировать нечего.)
Затем такие ссылки мы можем разбивать надвое. . То есть если r : ReadonlyStrRef, то есть поглащающая r операция split, которая возвращает две ссылки весом вполовину меньше:
let (a, b) = split(r),
где
a : ReadonlyStrRef
b : ReadonlyStrRef
(По факту веса ссылок у нас всегда будут диадическими числами, то есть рациональными числами, где в знаменателе степени двойки.)
Теперь давайте думать, как же “сдавать назад” ссылки, чтобы разблокировать переменную. Давайте просто наивно напишем:
join(x : ReadonlyStrRef, y : ReadonlyStrRef)
: ReadonlyStrRef
Так можно соединять ссылки назад, а когда мы назад собрали все получилась ссылка веса 1, и можно разлочить объект:
unlock(r : ReadonlyStrRef<1>) : MutStr
Кто внимательный, заметил проблемку. Мы можем по ошибке сджойнить ссылки на две совершенно разных переменных. Поэтому понадобится нам у ReadonlyStrRef ещё один параметр - собственно переменная, на которую мы ссылку сделали. ReadonlyStrRef.
Только я, если можно, буду вместо двухместрых сигнатур использовать запись origin.ReadonlyRef, представив что позаимствовали в языке Scala path dependent types.
И тогда корректные сигнатуры станут такие:
lock(v : Mut) : v.ReadonlyRef<1>
split(r : v.ReadonlyRef)
: (v.ReadonlyRef, v.ReadonlyRef)
join(x : v.)
join(x : v.ReadonlyRef, y : v.ReadonlyRef)
: v.ReadonlyRef
unlock>(r : v.ReadonlyRef<1>) : Mut
Важно отличать релевантное использование объекта (при котором объект вообще говоря консьюмится и становится недоступным) от использований в типовых аннотациях, при которых объект не консьюмится, а используется как абстрактное имя. Это то что у МакБрайда называлось в разных версиях статьи icon или ghost. Отметим также, что для использования функций join и unlock совершенно не нужно, чтобы объект v был внутри скоупа: он выводится унификацией параметров типов аргументов.
* * *
Мы тут пока рассуждали только о блокировке изменений переменной и получении на время блокировки реплицируемых readonly-ссылок.
Но возможна блокировка в другом смысле и получение accessors с другими capabilities: скажем можем мы сделать целочисленную переменную, и временно заблокировать как запись в неё напрямую, так и чтение из неё напрямую, получить реплицируемый accessor, позволяющий делать её инкремент (с репликацией тем же самым механизмом с дробными весами, split и join). Так мы получим Grow-only Counter, который нельзя ни считывать, ни сеттить пока кто-то может его инкрементить, а потом когда все “ручки, за которые можно инкрементить” сданы можно посмотреть сумму изменений. Разумеется, вместо Grow-only Counter подойдут любые CRDTы (Conflict-free replicated data type).
* * *
Читатель знакомый с concurrent separation logic заметит, что тройки (weight, original object, accessor capabilities) образуют тот самый частичный коммутативный моноид (PCM), описание которого в явном виде требуется для рассуждений о программе, если у нас появляются некие “вместилища объектов”, обеспечивающие возможность объектам выйти за локальный скоуп функции, где они были порождены.
В Rust'e таковы lifetimes для (мутабельных) переменных, в Kotlin'e coroutineScopes для джобов (запущенных корутин) - они позволяют объектам выйти за локальный скоуп, но всё ещё привязаны к лексическому скоупингу. Их кузены, не привязанные к лексическому скоупингу - персистентные вместищила объектов. Это Heap для переменных, Stage для акторов.
Получение вполне удовлетворительных теоретикотиповых описаний систем, где присутствуют такие сущности - важнейшая из не решенных на данный момент задач прикладной теории типов.