Last update: July 2023
Alexander Kuklev* <a@kuklev.com>
* JetBrains Research, HoTT and Dependent Types Lab
* Radboud University Nijmegen, Department of Software Science
Special thanks are due to Galina Ryazanskaya, who greatly assisted in editing this document.
Когда-то Tony Hoare назвал null pointers “ошибкой на миллиард долларов”. В истории языков программирования есть кое-что обходящееся, вероятно, ещё дороже: игнорирование фундаментальной разницы между данными и объектами.
С рождения мы воспринимаем окружающий мир и процессы в нём через картины и ощущения, и этого достаточно для мышления при помощи эвристик и аналогий. Но чтобы сделать возможными чёткие инструкции и строгие рассуждения, необходимо провести условные границы и разложить мир на идеализированные единицы моделирования — объекты. В зависимости от предметной области это могут быть, например, яблоки и груши, ордера и квитанции, поезда и станции или электроны и фотоны. Мы учимся этому, когда учимся говорить и думать словами, а оттачиваем, занимаясь программированием (по части «чётких инструкций») и математикой (по части «строгих рассуждений»). Канонический пример материального объекта в программировании — ячейка памяти, содержащая изменяемое целочисленное значение.
Объекты не обязаны быть в прямом смысле материальными — как объекты следует рассматривать также ресурсы, такие как файлы, базы данных и очереди (message queues), а также внешние сервисы с заданным API. В том числе как внешний сервис следует рассматривать саму среду (program-level POSIX environment), в которой запускается программа.
Теперь допустим, что мы считали значение из ячейки памяти и взвесили яблоко, установив, что X.value = 2 и Apple1.weight = 93g. Упоминающиеся тут ячейка памяти X и яблоко Apple1 — материальные объекты, а вот «целое число 2» и «93 грамма» — платонические “объекты”, существующие исключительно в мире математических абстракций. В их отношении мы будем применять термины данные (мн.ч) и значение (ед.ч). Данные — информация, отделённая от носителя и контекста. Канонические примеры данных — числа, строки, конечные списки чисел List<Int> и таблицы ключ-значение Map<X, Y>.
Данные не обязаны быть конечными, что в применении к программированию можно понимать в терминах evaluation-on-demand. Так значениями являются вещественные числа x : ℝ, бесконечные списки значений Seq<T>, и потенциально бесконечные таблицы “ключ-значение”, то есть так называемые чистые функции (X)-> Y. Отметим, что таким образом чистая функция может служить аргументом другой чистой функции — например, функции map(l : List<X>, f : (X)-> Y) : List<Y>, применяющей функцию f к списку l поэлементно. Разумеется и сама функция map : (List<X>, f : (X)-> Y)-> List<Y> тоже значение.
К объектам применимо понятие “тот же самый, один и тот же” (same). Так в двух разных ящиках могут лежать равные числа, но это не делает их одним и тем же ящиком — если в одном поменять значение, оно не поменяется в другом. Объекты могут возникать/порождаться и исчезать/поглощаться, к ним применимо понятие жизненного цикла (lifecycle).
К значениям, применимо понятие “равный” (equal), но не “тот же”. Быть равными — это свойство пары значений: равенство может быть доказано или опровергнуто, а вот быть одним и тем же объектом можно только по определению. Более того, невозможно вообще корректно определить пару из объекта с самим собой — пара объектов это автоматически пара двух разных объектов. Понятие жизненного цикла к значениям принципиально неприменимо, про них даже нельзя сказать что они “всегда были и будут” — они просто вне времени и материального мира.
Теперь, ознакомившись с базовыми понятиями и обрисовав фундаментальные различия, разберёмся зачем проектировать языки программирования с учётом этих различий. В примерах я буду пользоваться вымышленным языком программировании с синтаксисом на основе Kotlin‘а.
Первый в современном понимании язык программирования появился в 1957 году, это был FORTRAN. Как и во всех современных императивных языках, программа на Фортране представляет собой последовательность инструкций. Два основных вида инструкций — определения a := 1 и команды print("Hello"). Внутри определений и в качестве аргументов команд могут использоваться выражения, такие как 60 · sqrt(4) и a + 10:
val a := 60 · sqrt(4)
print(a + 10)
Выражения — синтаксическое понятие, пришедшее в программирование из математики. Выражения описывают путь вычисления значения, и должны быть взаимозаменимы с этим значением: если вместо выражения сразу подставить его результат, программа не должна измениться. Выражения не содержат ничего кроме последовательного применения функций к значениям. Так выражение 60 · sqrt(4) предписывает сперва применить функцию sqrt к значению 4, а затем применить функцию умножения (·) к результату и значению 60.
К сожалению, подавляющее большинство императивных языков программирования не различают чистые функции, которые без каких-либо побочных эффектов детерминистски вычисляют значение, соответствующее аргументу/аргументам, и команды, которые возвращают значение вообще говоря не детерминированное своими аргументами, и могут производить при выполнении необратимые действия, такие как например удаление файлов. В таких языках можно использовать команды в качестве функций внутри “выражений”. Мы будем использовать термин псевдовыражения для “выражений”, содержащих хотя бы одну команду.
Чистую функцию можно задать выражением (в этом случае выражение называют телом функции), но не псевдовыражением. Псевдовыражение содержит хотя бы одну команду, а значит функция заданная им будет иметь недетерминированный результат или побочные эффекты, то есть не будет чистой функцией. Отметим, что важно не отождествлять функцию и выражение, которым она задана. Функция — семантическое понятие, имеющее подразумеваемую интерпретацию “потенциально бесконечная таблица ключ-значение”. Таким образом, две функции, имеющие равные результаты на равных аргументах, равны как функции и должны быть неразличимы. Выражение же — понятие синтаксическое, и неэквивалентные выражения могут задавать равные функции. Для программы должно быть невозможно посмотреть “посмотреть внутрь определения” функции, т.к. это нарушило бы неразличимость равных функций.
На первый взгляд функции и команды логично объединить — и те, и другие могут принмать аргументы и возвращать значения. Объединение даёт экономию концепций и таким образом как будто уменьшает сложность языка, что же тут может быть плохого? Проблема в том, что нельзя больше рассчитывать, что “выражения” взаимозаменимы со своими значениями. Теряется удобная ментальная модель, позволяющая думать о программе, просто смотря на неё. Теперь во всяком безобидно выглядящем “выражении” может скрываться плохо предсказуемое поведение.
Давайте рассмотрим две самые безобидные с точки зрения поведения команды:
rand(), которая генерирует аппаратное случайное целое число, иtrace(msg : String), которая никак не влияет на вычисления, а лишь записывает msg в лог, недоступный для чтения изнутри программы во время её выполнения.Обе эти команды
Если бы мы имели дело с выражениями, следующие две программы были бы эквивалентны:
val n := rand()
n + n
и rand() + rand(). Но для псевдовыражений взаимозаменяемость с результатом не выполняется: Первая программа всегда выдаёт чётное число, ведь она складывает одно и то же случайное число с самим собой, а вторая складывает два независимых случайных числа, и результат вполне может быть нечётным.
Теперь рассмотрим команду trace(). Допустим, с целью отладки программисты добавили ее в определение функции сложения, и всякий раз при сложении двух чисел выводит их сумму в лог. Если бы функция (+) оставалась чистой, следующие три программы обязаны быть эквивалентны:
(1 + 2) + 3, 1 + (2 + 3), 6.
С точки зрения результата они действительно эквивалентны, но с точки зрения эффектов неидентичны. Первая при выполнении выведет в лог 3, 6, вторая 5, 6, третья не выведет вообще ничего. Полагаясь на подстановочность выражений можно делать мощные оптимизирующие компиляторы, но стоит нам добавить в язык казалось бы безобидную команду trace(), оптимизирующие компиляторы входят в непредсказуемый конфликт с пригодностью логов для post-mortem анализа.
Обратите внимание на пикантность ситуации. Тот, кто пишет (1 + 2) + 3, едва ли заподозрит возможность какого-то подвоха — «это же просто арифметическое выражение». Тот, кто добавляет trace в сложение, едва ли осознаёт в этом какую-либо проблематичность — «это же просто для отладки». Так в результате несогласованных безобидных действий не знающих друг о друге людей совершенно неожиданно может возникнуть как минимум многократное замедление программы.
Теперь рассмотрим команды с необратимыми эффектами. Пусть команда delete(wildcard) удаляет файлы, соответствующие паттерну wildcard, и возвращает количество удалённых файлов. Рассмотрим вот такую программу:
print( delete("*.tmp") · delete("*.*~") )
Что хотел сказать этим автор? Можно ли запустить обе команды удаления одновременно, или нужно сперва произвести удаление слева от оператора (·), а только потом то, которое справа? Если вы уже выбрали предпочтительный ответ, то теперь предположите, что в каталоге вообще не было файлов с расширением .tmp, и первая команда возвращает 0. Нужно ли в таком случае вообще запускать вторую команду удаления? Если допустимо было запустить обе команды одновременно, то можно ли напечатать 0 до завершения второго (ведь уже известно, что результат будет 0), или нужно дождаться завершения? Или может быть прервать второй процесс удаления на пол-дороги? Эти решения предстоит принять и описать в спецификации проектировщикам языка, а пользователям языка (в теории) — их выучить, а на практике (потому что никто не читает спецификаций) неожиданно наткнуться на них в процессе болезненной отладки. Вместо простой и прозрачной ментальной модели выражений, для понимания псевдовыражений требуется знание замысловатых правил, зачастую являющихся результатом исторической случайности.
Вот так смешение функций и команд, на первый взгляд дающая экономию концепций, порождает лавину избыточной сложности (accidental complexity).
Радикальное решение этой проблемы — вообще убрать команды из языка. По этому пути идут так называемые чисто-функциональные (purely functional) языки программирования: в них оставлены одни только чистые функции и данные, а команды и объекты вообще отсутствуют.
Для большинства из нас концепция объекта куда более привычна, чем концепция значения — потому легко предположить, что значения сложная в понимании и обращении математическая абстракция, в то время как объекты просты и наглядны. На деле ситуация обстоит противоположным образом.
Для описания свойств и взаимоотношений значений, и строгих рассуждений о них математики ещё полтора века назад [Frege1879] разработали формализованный язык, называемый исчислением предикатов. Десятилетия теоретических исследований и практического использования исчисления предикатов позволили убедиться в его корректности и достаточной выразительности, понять все его возможности и ограничения, выработать удобный синтаксис.
Когда говорят о чисто-функциональных языках программирования, часто упоминают, что у них есть “математическая основа“. Что имеется в виду и какие преимущества это даёт?
Чисто-функциональные языки программирования оперируют напрямую только и исключительно данными, что позволяет применять исчисление предикатов. Его выразительность гарантирует, что все свойства программ, не завиящие от устройства компилятора / модели вычисления, можно сформулировать. Так можно сформулировать требование, что функция sort всегда правильно сортирует, а функция groupBy правильно группирует. Имеются техники для анализа, в полной ли мере те или иные требования характеризуют функцию. Они позволяют найти неучтённые пограничные случаи, либо убедиться в их отсутствии.
На первый взгляд, эти преимущества имеют значения только в очень нишевых областях, где используется формальная верификация кода. Однако даже если не заниматься формальной верификацией, само принципиальное понимание как формулировать и доказывать утверждения о программах, позволяет выработать достоверную ментальную модель — неформальный способ думать о программах, принципиально необходимый для написания корректных-по-построению программ. Именно в этом состоит главное практическое преимущество “математической фундированности” чисто-функциональных языков. Условия корректности редко выписывают явно вовсе не из-за лени, а потому, что их всё равно едва ли кто-нибудь читать до первого катастрофического сбоя. Совсем другое дело — хорошо структурированный, литературно написанный и очевидно корректный-по-построению код. Будучи укомплектован тестами, демонстрирующими типовое использование и покрывающими пограничные случаи, такой код — лучшая спецификация и лучшая документация самому себе. Только так можно гарантировать отсутствие расхождение между документацией, спецификацией и реализацией.
Несмотря на все эти преимущества, чисто-функциональные языки имеют и ограничения. Некоторые прикладные задачи, например создание интерактивных приложений и распределённых систем, не сводятся напрямую к преобразованию данных. Чтобы заниматься такими задачами на чисто-функциональных языках, приходится прибегать к использованию замысловатой машинерии, позволяющей окольными путями описывать манипуляции объектами на этих языках, лишенных синтаксического аппарата для описания и использования объектов.
Для решения именно таких задач спроектированы современные мультипарадигменные языки, такие как Kotlin, Rust и Scala, позволяющие оперировать напрямую не только данными, но и объектами.
За исключением некоторых узких областей, программирование не сводится к преобразованию данных. Даже если вынести за скобки вопросы моделирования предметной области в терминах объектов и состояний [Shlaer-Mellor91], понятия объектов и команд нужны для описания взаимодействия с базами данных, файлами и сокетами, любых механизмов коммуникации, будь то коммуникация с пользователем, со сторонними приложениями или между компонентами внутри одной системы. Давайте перечислим разновидности объектов, постоянно встречающихся в программировании, начиная с самых простых с точки зрения жизненного цикла.
Одноразовые объекты
Самые простые с точки зрения жизненного цикла объекты — объекты одноразового использования. Примером такого объекта может служить часто присылаемый вместе с сообщением от какого-либо сервиса/сервера одноразовый канал для ответа c : OneShotChannel<T>. Это объект с единственной командой c.reply(t : T), которую можно запустить лишь один раз, после чего объект “потрачен” и не может быть использован во второй раз. Одноразовыей объект с единственной командой вполне можно отождествить с этой командой, в традиции https://kotlinlang.org/docs/fun-interfaces.html.
Если вам доводилось программировать пользовательский интерфейс на JavaScript’е или иным образом сталкиваться с реактивным программированием, вы знаете что такое callbacks. Вы можете запустить таймер (setTimeout()) или какую-то команду f, длящуюся неограниченно долго (например, ожидающую ответ от remote-сервера или пользовательский ввод), и передать ей в качестве аргумента callback — процедуру, которую таймер/команда будет запустят позже. Вообще говоря, в качестве callback’а можно передать не только процедуру, но и приостановленный suspended процесс, ожидающий какого-то значения (или просто “отмашки”) чтобы продолжить выполнение. Сигнатура такой команды f выглядит вот так:
suspend fun f(..., callback : Suspension<X>) {
...
}
Аргумент callback типа Suspension<X> — строго одноразовый. То есть вызов callback(x) может быть последним действием f, а может быть callback будет в какой-то момент запущен отдельным потоком при помощи launch {callback(x)}, или передан в какое-нибудь хранилище приостановленных процессов для дальнейшей реактивации. Важно, что по какому бы сценарию не пошло выполнение f, объект callback должен быть использован, причём ровно один раз.
Встречаются и подвешенные процессы, возвращающие результат типа Y, их тип мы будем записывать как Suspension<X, Y> или при помощи более краткой записи (X)⊸ Y, где символ ⊸ называется линейной импликацией. Почеркнём, что Suspension<X> = Suspension<X, Nothing>, где Nothing пустой тип, тип не содержащий ни одного значения.
Генераторы и Потребители — Сопроцедуры
Генераторами называются потенциально бесконечные процессы, время от времени генерирующие значения типа X при помощи вызова yield(x : X):
suspend fun Consumer<Int>.fibonacciGen() {
var prev = 1
var head = 1
repeat {
yield(head)
(prev, head) := (head, head + prev)
}
}
Потребителями называются потенциально бесконечные процессы, время от времени запрашивающие у генератора следующее значение при помощи вызова next() : X
suspend fun foo(args, gen : Generator<X>) {
val x := gen.next()
...
val y := gen.next()
...
}
Аргумент gen подменяемый одноразовый — он уже недоступен в своей исходной форме, после вызова применительно к нему команды next(). При каждом вызове запроса gen.next() команда next() поглощает имеющийся объект gen и подменяет его новым gen, находящемся в следующем состоянии.
Несложно заметить, что с точки зрения генератора ситуация выглядит ровно противоположным образом: это он принимает подменяемый одноразовый аргумент (в нашем случае это неявный аргумент this), который подменяется командой yield. Вообще говоря, мы могли бы передавать мы могли бы передавать в next() аргумент y : Y, и тогда генератор получал бы его как значение, возвращаемое командой yield. Тогда с точки зрения потребителя генератор это сервис, предоставляющий запрос next(y) : X, а с точки зрения генератора потребитель это сервис, предоставляющий запрос yield(x) : Y. В связи с этой двойственностью и кооперативным взаимодействием, такие объекты как fibonacciGen и foo называются сопроцедурами (coroutines).
Отметим, что сервисы могут вообще говоря предоставлять несколько разных запросов — скажем, ask(prompt) и say(message):
suspend fun Tty.bar() {
var total := 0;
repeat {
total += ask<Int>("Please enter a number")
say("Sum of entered numbers is $total")
}
}
В терминах сервисов с тем или иным фиксированным интерфейсом можно рассматривать огромное количество внешних по отношению к компьютеру материальных объектов, таких как живой пользователь или аппаратный генератор случайных чисел.
Ресурсы
Описанные выше сервисы (генераторы, потребители и их обобщения) предполагают только исключительный доступ — имея такой объект, невозможно раздать доступ к нему сразу в несколько мест. Самая распространённая в прикладном программировании разновидность объектов — так называемые ресурсы: файлы, очереди (message queues), базы данных и т.д. Ресурс это как раз объект, доступ к которому можно раздать сразу в несколько мест. Такое положение дел можно рассматривать как возможность создавать и передавать ссылки на ресурс, предоставляющие те или иные фиксированные возможности доступа (capabilities).
Например в нижеследюущем коде мы пробуем открыть файл ./storage.dat. В момент открытия создаётся объект-ссылка на файл, обеспечивающий возможности чтения и записи. Когда этот объект закончит свой жизненный цикл, файл снова станет доступен для открытия.
try(open("./storage.dat")) {
// here `this` will refer to the file handle
// we may use `read` and `write` commands
} catch (e : AccessDeniedException) {...}
В этом примере мы пытаемся как раз-таки получить объект-аксессор, обеспечивающий эксклюзивный доступ к файлу. Такой объект аксессор исключает репликацию, то есть у нас нет возможности внутри указанного блока передать this куда-либо дальше в качестве аргумента. Однако есть и другие виды объектов-аксессоров к файлу. В частности:
Такие аксессоры могут допускать репликацию. Очереди сообщений и базы данных изначально сделаны для того, аксессоры к ним (возможность подписки на поток сообщений/отфильтрованных изменений и возможность класть сообщения/накатывать изменения в базе) были реплицируемыми неограничено.
Некоторые ресурсы таковы, что мы можем разбить их время на изолированные части. Например, изменяемый массив можно разбить на любое количество подмассивов с непересекающимися индексами:
suspend fun quicksort(arr : MutableArray) {
if (arr.size <= 1) {return}
val pivot := partition(arr)
arr.split(0 until pivot, (pivot + 1) until arr.size) { (lt, rt) ->
launch {quicksort(lt)}
launch {quicksort(rt)}
}
}
Особенная разновидность ресурсов — фабрики объектов, которые позволяют не просто открывать, но создавать в своих рамках какие-то объекты. Например, запускать в своих рамках независимые процессы (такие ресурсы называются execution scopes, в Kotlin’e — coroutine scopes) или создавать в их рамках изменяемые объекты в памяти (такие ресурсы называются heap scopes, в Rust’е — lifetimes). К фабрикам относятся и файловые системы, позволяющие создавать в их рамках каталоги и файлы.
В предыдущем разделе мы поговорили о том, какие практические преимущества для языков программирования предоставляет наличие стройной и исчерпывающей семантики, прозрачно соответствующей синтаксису. Целью нижеследующего текста будет достижение того же для языка программирования, способного наравне со значениями оперировать объектами и поддерживающего concurrency. Кстати, именно такие языки называют мультипарадигменными. В данный момент наиболее развитыми среди распространённых мультипарадигменных языков программировани являются Kotlin, Rust и Scala.
У каждого из этих языков есть преимущества, которых лишены два других.
Внутри каждого мультипарадигменного языка имеется чисто-функциональный язык — функциональное ядро. В ходе нижеследующего текста мы сперва урежем Kotlin до его идеализированного функционального ядра, а потом реконструируем поверх этого стабильного фундамента все необходимые механизмы типизации объектов и работы с объектами, по ходу дела проясняя, расширяя и уточняя их. Мы подробно разберём и такие объекты как приостановленные сопроцедуры и замыкания (closures) в которые заключён (captured) объект, разберёмся как думать об объектах, эффектах и взаимодействующих процессах понятным и непротиворечивым образом. Получившийся язык будет пригоден как для формальной верификации сложно взаимодействующих систем, так и для написания корректных-по-построению фрагментов этих систем.
Наш подход далёк от идеалов экономии концептов — нам придётся ввести и понять много разных концепций и сущностей, однако в данном случае мы будем иметь дело не с избыточной, а с принципиальной сложностью. Со сложностью, присущей самой природе описываемых явлений. Со сложностью, в которой полезно разобраться, если хочется до конца что-либо понимать. Даже если вы не намереваетесь заниматься формальной верификацией и вообще когда-либо пользоваться подобным языком программирования, само понимание его устройства поможет лучше понять многие моменты, касающиеся параллелизации, out-of-order execution, а также многие тонкости, постоянно возникающие в многопоточном программировании.
Disclamer: Для понимания нижеследующих разделов очень желательно основательное знакомство с языком программирования Kotlin, а также понимание общих концепция и практик как объектно-ориентированного, так и функционального программирования. Совершенно необходимо также понимание принципов работы coroutines/suspensions + structured concurrency.
Среди необщеизвестных элементов языка, которыми я буду активно пользоваться — data classes и sealed abstract classes, при помощи которых можно описывать произвольные обобщённые алгебраические данных, extension methods и extension properties, сontext receivers и type-safe builders. Желательно также иметь общие представления о companion objects и typeclasses.
Сперва определим Pure Kotlin — строго-функциональное ядро Kotlin’а, где все функции представляют из себя чистые функции, а все аргументы, параметры, и локальные переменные представляют из себя данные. В частности:
return, throw, break и continue;Мы можем разрешить использование локальных переменных var и циклов while и repeat/while, т.к. они могут быть сведены к рекурсии. Отметим, что и локальные определения val x = expr тоже могут быть сведены к применению и абстракций функций.
Для лучшего соответствия принятым в математике обозначениям и стандартам, мы также будем
Int для обозначения потенциально неограниченно больших по модулю целых чисел, как в Python3;2 + 3 = (+)(2, 3) = 2 ‹Nat.plus› 3;¬ в качестве оператора отрицания, в том числе в ¬in, а также a ≠ b в качестве оператора различия;a = b вместо двойного в качестве оператора равенства;val a := expr вместо одинарного равенства в качестве оператора присвоения;{x ↦ x + 1} вместо диграфа -> в замыканиях и when-блоках;·;x ▸ f вместо x.let f в качестве оператора применения функции налево x ▸ f := f(x);files ▸filter
it.size > 0 &&
it.type = "image/png"
▸map { it.name }
Мы введём два новых синтаксических элемента языка — codata classes и type-classes, на принципах работы которых я не буду заострять внимание, т.к. предполагается что читатель хорошо знаком с этими понятиями. Синтаксис же я продемонстрирую на двух следующих примерах:
Определение последовательности чисел Фибоначчи
codata class Seq<T>(val head : T)
fun next() : Seq<T>
foo fib(head : Int := 1,
prev : Int := 1) := Seq<T>(head)
fun next() := fib(head + prev, head)
Определение Моноида
data class <T>.Monoid(operator val ‹compose› : (vararg xs : T)-> T)
val unit := compose() // unit is the nullary composition
contracts {
unit ‹compose› x = x
x ‹compose› unit = x
x ‹compose› y ‹compose› z = x ‹compose› (y ‹compose› z)
compose(x, *xs) = x ‹compose› compose(*xs)
}
// А теперь мы можем вот так:
fun<T : Monoid> square(x : T)
x ‹T.compose› x
// И так:
fun<T : Monoid(`∘`)> square(x : T)
x ∘ x
Отметим также, что Pure Kotlin может быть расширен индуктивными типами, чекером тотальности и зависимыми типами.
Stratified Kotlin — расширение Pure Kotlin, в котором мы допускаем использование команд и существование псевдовыражений. Для того, чтобы команду всегда можно было отличить от функции, её название должно начинаться с восклицательного знака: !rand, !trace(msg), !return, !throw, !break.
Среди команд мы отметим следующие сорта:
!return, !throw, !break) — весь код, следующий за ними в их ветке выполнения был бы unreachable, поэтому они обязаны быть последними в своей ветке выполнения. Такие команды имеют тип возвращаемого значения Nothing, не содержащего ни одного значения. Такой тип возвращаемого значения означает, что эти команды с точки зрения вызывающей их функции никогда не завершаются, никогда не возвращают управление туда, где их вызвали.!print) — eсли они завершаются, то всегда возвращают одно и то же значение Done. Это команды с типом возвращаемого значения Unit, населённого одним единственным элементом.!rand) — многоразовые команды, от изменения порядка вызова которых не меняются их результаты и эффекты.!delete(wildcard) : Nat, ask<Int>("Please enter a number") : Int).Всякая инструкция (“строка программы”) может содержать произвольное количество вызовов команд-псевдозначений, но не более одного вызова команды, не являющейся псевдозначением. Простые и финальные команды обязаны быть в головной (“внешней”) позиции инструкции, причём финальные могут быть только в последней инструкции соответствующей ветки выполнения.
!print(!rand · !rand) // — так можно
!print( !delete("*.tmp") · !delete("*.*~") ) // — а так нельзя, нужно так:
val a := !delete("*.tmp")
val b := !delete("*.*~")
!print(a·b)
В частности нельзя опустить фигруные скобки вокруг !return или !break в
if (a = null) {!return null}
a.first ?: {!throw SomeException()}
В чистых функциях возможно применение команд структурированных локальных переходов (!return, !continue, !break), т.к. эти команды тривиально сводятся к использованию if-ов.
Все остальные команды можно использовать только в сопроцедурах, а также функциях- и замыканиях-получателях объектных интерфейсов:
fun Env▸main(args : List<String>)
// This function is defined relative to program-level POSIX-environment `Env`,
// so we can use `!print`, `!open` and many other commands here
!print("Starting...")
with(!open("config.ini"))
// This block is a closure receiving an opened file as a context
// here we may additionally use `!read` and `!write`
...
!print("Finished reading configuration...")
— где Env — объектный интерфейс, т.е. интерфейс, описывающий набор доступных команд, их сигнатуры и поведение.
Интерфейсы, доступные в Pure Kotlin переименуем в data interface, а ключевое слово interface будем использовать для типизации объектов. Многократно упоминавшиеся команды !trace и !rand принадлежат следующим интерфейсам:
interface Log
fun trace(msg : String)
interface RandGen
val rand: Int
Ключевое слово fun используется для задания команд, для которых порядок вызова важен, в то время как val используется для псевдозначений. Выше уже упоминался хрестоматийный пример объекта — изменяемая (мутабельная) переменная. На Котлине её интерфейс можно было бы описать так:
interface Variable<T>
val get : T
fun set(v : T)
Другой канонический пример — телетайповый интерфейс взаимодействия с пользователем:
interface Tty
fun say(msg : String)
fun ask<T : Promptable>(prompt : String) : T
Каждое использование команды как бы “поглощает” объект целиком, и подменяет его новым, причём новый может вообще говоря иметь другой интерфейс. Если команда подменяет интерфейс своего объекта, будем обозначать это в её сигнатуре специальной аннотацией ⏴NewInterface после типа, вот так:
sealed interface Order
interface Unfinished : Order
fun process(x : PaymentProof) : OrderId ⏴Order.Pending
interface Pending : Order
fun markAsSent() ⏴Order.Shipped
interface Delivered : Order {
fun markAsDelivered() ⏴Order.Delivered
...
Некоторые команды могут приводить объект в состояние, в котором у него уже нет команд. Такие состояния называются терминальными и означают, что жизненный цикл объекта закончился.
interface OutputStream
fun append(s : String)
fun close() ⏴Nothing
Смена состояния на Nothing гарантирует, что после вызова !close в той же ветви исполнения будут уже недоступны команды !close и !append. Этот механизм позволяет описать один из важнейших типов объектов — подвешенные процессы (single-shot suspensions):
fun interface Suspension<X, Y>
fun resume(x : X) : Y ⏴Nothing
// Suspension<X, Y> мы будем идентифицировать с `(X)⊸ Y`
interface Continuation<T>
fun resume(t : T) : Nothing
// возвращаемый тип Nothing автоматически означает Nothing⏴Nothing
(Объяснение конструкции fun interface: https://kotlinlang.org/docs/fun-interfaces.html)
С использованием механизма подмены состояния у объекта больше нет постоянного набора методов — вместо этого у него имеется жизненный цикл, представляющий из себя конечный автомат состояний, и набор и сигнатуры доступных команд зависят от текущего состояния объекта. Котлин уже обладает механизмом smart casts, в результате которого тип переменной может сужаться по ходу выполнения программы — подмена состояний — расширение этого механизма.
В Котлине для описания типов функций используется обозначение (Xs)-> Y, а для описания методов существует специальное обозначение Context▸(Xs)-> Y. Выше мы уже вводили обозначение (Xs)⊸ Y, называемое линейной импликацией. По аналогии введём для команд обозначение Interface▸(Xs)⊸ Y, а если команда подменяет интерфейс своего объекта, то Interface▸(Xs)⊸ Y⏴NewInterface. Для псевдозначений будем использовать обёртку (_)! известную как “replicable service modality”.
Variable<T>::set : Variable<T>▸(T)⊸ Unit
Variable<T>::get : (Variable<T>▸()⊸ T)!
OutputStream::append : OutputStream▸(String)⊸ Unit
OutputStream::close : OutputStream▸()⊸ Unit⏴Nothing
Строгое описание системы типов, в рамках которой мы можно описать введённые тут интерфейсы, можно найти в статье Ankush Das и Frank Pfenning “Rast: A Language for Resource-Aware Session Types”.
Ещё более точное описание сигнатур интерфейсов возможно при помощи зависимых типов. В зависимо-типизированных языках параметрами типов могут являться значения, например List<T, size : Nat>:
interface RandGen
fun generateRandomPermutation(size : Nat) : List<Nat, size>
Для знатоков теории категорий отмечу что зависимо-типизированные сигнатуры интерфейсов в точности соответствуют свободно-порождённым зависимым комонадам (расширениям Кана).
Как уже было сказано в самом начале, понятие равенства в мире объектов расщипляется на две модальности — равенство эффектов и равенство результатов, которые мы будем обозначать через =e= и =r= соответственно.
Используя равенство эффектов мы можем указать важнейшее свойство команды !rand — отсутствие побочных эффектов:
interface RandGen
val rand: Int
contracts {
{!rand} =e= {}
}
Равенство результатов вообще говоря нерефлексивное, например !rand =r= !rand не
выполняется. Оператор !foo : X ⊸ Y называется детерминированным в точности, если
для него выполняется рефлексивность равенства результатов, т. е.
будучи вызван с одинаковым аргументом он всякий раз выдаёт одинаковые результат:
a = b влечёт !foo(a) =r= !foo(b).
Также обратим внимание, что равенство результатов не влечёт равенства эффектов:
с точки зрения результатов любые два запроса, не возвращающие результатов, равны, но с точки зрения
эффектов !trace("Hello") и !trace("Goodbye") очевидно различаются.
Равенство эффектов напротив рефлексивное, но не влечёт равенства результатов. Равенство эффектов
может быть использована для выражения независимости (параллелизуемости) запросов. Мы можем, например,
постулировать, что запись в независимые потоки вывода (например, !print и !trace) коммутирует:
{!print(x); !trace(y)} =e= {!trace(y); !print(x)}
Информация о коммутировании тех или иных вызовов открывает богатые возможности для оптимизирующей компиляции: компилятор, если это способно повысить производительность, может переставлять вызовы местами или даже вовсе параллелизовать их.
Приведём описание интерфейса мутабельная переменная с контрактами, в полной мере определяющими её поведение:
interface Variable<T>
val get : T?
fun set(v : T)
contracts {
!get =r= !get
{!get} =e= {}
{!set(x1); !set(x2)} =e= {!set(x2)}
{!set(x); !get} =r= x
}
Обратите внимание, что из контрактов и сигнатуры прямо следует, что !get может возвращать null только до первого вызова !set, но не очевидно, что он обязан выдавать именно null до первого вызова !set. Однако легко показать, что это единственное возможное поведение, если в качестве параметра T подставить Nothing, а из параметричности следует что при использовании любого другого типа поведение должно оставаться таким же.
Для знатоков теории категорий отмечу что контракты такого рода называются string diagrams, а интерфейсы, снабженные такими контрактами соответствуют конечно-представленным (вообще говоря, индуктивно-представленным) зависимым комонадам.
Для интерфейса, исчерпывающе заданого контрактами, можно автоматически сгенерировать монаду Дейкстры (https://arxiv.org/abs/1903.01237), предоставляющую удобный инструмент для формальной верификации программ.
* * *
Система типов из упомянутой выше статьи [Das-Pfennig20] допускает сигнатуры более общего вида, чем описанные нами интерфейсы. Можно допустить наличие команд, возвращающих наряду с изменённым this один или несколько дополнительных объектов, или потребляющих объекты. Такие команды мы будем называть операторами порождения и поглощения.
Для описания объектов с такими командами мы будем использовать вместо ключевого слова interface включевое слово resource. В известных автору сценариях практического применения, побочно возвращаемые ресурсами объекты — объекты аксессоры, позволяющие получить эксклюзивный или параллельный доступ к объекту или его подобъектам с теми или иными модальностями доступа (capabilities).
Чтобы формализовать детерминированность результата при параллельном доступе к непересекающимся подобъектам, и согласованности-в-конечном-итоге (eventual consistency) если есть возможность сопернического доступа (concurrent access) ко всему объекту или его пересекающимся подобъектам, требуется описать отделённости/спутанности подобъектов в терминах ресурсной алгебры (resource algebra).
Контракты таких объектов порождают не монаду Дейкстры, а более богатый математический объект, внутренним языком оторого является сепарационная логика. Существует глубокая математическая аналогия между заданием на фактор-индуктивном типе данных синтетического равенства в гомотопической теории типов HoTT, и определением фабрик, как свободно-порождённых алгебр, удовлетворяющих заданной сигнатуре и отношениям отделённости/спутанности, заданным в терминах ресурсной алгебры.
Для интересующихся квантовыми вычислениями математиков отметим, что ресурсную алгебру можно рассматривать как неунитальную алгебру над “полем с одним элеменом” [Durov08]. Судя по всему, если же такую алгебру (неунитальными) гомоморфизмами действует поле с нетривиальной группой единиц, то такая ресурсная алгебра может описывать одновременное существование нереализуемых классически полностью изолированных друг от друга объектов, обладающих тем не менее согласованным-в-конечном-итоге состоянием — такое положение дел соответствует феномену, известному как квантовая спутанность, а ресурсы с такими ресурсными алгебрами, по-видимому, следует рассматривать как квантовые сопроцессоры.
Позволю себе отвлечённое примечание для тех редких читателей, кто хорошо знаком с HoTT и квантовыми теориями поля одновременно. Вернёмся к аналогии с HoTT: ведь там помимо фактор-индуктивных типов можно определять высшие индуктивные типы, равенство на которых является не отношением, но типом значений само по себе — оно населено (не обязательно равными между собой) автоморфизмами подлежащего типа. Глубоко спекулятивно мы можем предположить, что можно разработать такую теорию типов, где автоморфизмы ресурсной алгебры в свою очередь тоже могу быть не значениями, но объектами, что неуловимо напоминает положение дел в калибровочных теориях поля. Там калибровочные бозоны (такие как, например, фотоны) являют собой объектификацию внутренних симметрий поля Дирака (электронно-позитронного поля), как раз описываемого в терминах операторов порождения и уничтожения электронов.
* * *
Для всяких двух объектов, не являющихся подобъектом одного, тем не менее тоже можно дать определение независимости и изолированности. Объекты obj1 и obj2 называют независимыми вызовы методов obj1 и методов obj2 коммутируют между собой. Независимость объектов имплицирует отсутствие коммуникации между ними, но не означает детерминированности.
Изолированным называется объект, независимый от любых других объектов. Для RandGen и Log это свойство постулируется, для детерминистски работающих мутабельных объектов, не замыкающих в себе других объектов, оно выполняется по построению.
Выше мы говорили, что аргументами функций в Pure и Stratified Kotlin могут быть только значения, но не объекты. В Stratified Kotlin мы добавим ещё и coroutines также известные как “suspendable functions”. Сопроцедуры могут принимать в качестве аргументов приведённые выше продолжения и подвешенные сопроцедуры (suspensions).
Всякую функцию performSomeCalculation(x : X) : Y мы можем превратить в сопроцедуру
suspend fun performSomeCalculationCPS(x : X, cont : Continuation<Y>)
val result = performSomeCalculation(x)
!cont(result)
Важно, что cont в каждой ветви выполнения можно запустить не более одного раза, и необходимо запустить не менее одного раза. В общем, в каждой ветви выполнения cont необходимо запустить ровно один раз. Причём её тип Nothing указывает на то, что все инструкции, следующие ниже её никогда не будет запущены (unreachable). Отметим, что команды !break, !continue, !return и !throw тоже имеют тип Nothing и таким образом всегда являются финальными командами своей ветви выполнения.
Второй отличительной особенностью сопроцедур является то, что внутри сопроцедуры можно приостановить её выполнение и передать продолжение в качестве аргумента в другую сопроцедуру:
context(Log)
suspend fun useThatCalculation(x : X) : Y
!trace("Executing foo.....")
suspendCoroutine { cont ↦
!performSomeCalculationCPS(x, cont)
}
!trace("After suspending.....")
Прежде мы только описывали объекты, но никогда не создавали их. Операция suspendCoroutine {obj -> code} “создаёт” объект obj. Мы можем обобщить эту операцию для создания объектов произвольного интерфейса. Правда, для этого нам понадобится аналог when с паттерн-матчингом.
interface S1
foo(x : X) : Y nextState<S2>
bar(a : A) : B nextstate<S2>
...
suspend fun zee(f : S1▸(T) ⊸ R, t : T) : S
suspend.f(t) {
foo(x : X) ↦ {cont : (S2▸(Y)⊸ R) ↦
// something consuming cont and returning S
}
bar(a : A) ↦ {cont : (S2▸(B)⊸ R) ↦
// something consuming cont and returning S
}
return(r : R) ↦ {
// something returning S
}
}
В частности мы можем реализовать поддержку переменных, исключений и генераторов:
suspend fun<T, R, vararg Xs> withVar(f : Variable<T>▸(*Xs) ⊸ R, v : T? := null) : R
suspend.f {
val get := v
set(v : Int) ↦ {
withVar(it, v)
}
return(r : R) ↦ r
}
interface Throws<E>
throw(e : E) : Nothing
suspend fun<E, R> try(f : Throws<E>▸() ⊸ R, handler : E -> R) : R
suspend.f {
throw(e : R) ↦ handler(e)
return(r : R) ↦ r
}
interface Generator<T>
yield(g : T)
suspend fun<R> sum(generator : Generator<Int>▸() ⊸ Unit, accumulator : Int := 0)
suspendInto(generator) {
yield(v) ↦ {it : (State▸(RetType)⊸ R) ↦
sum(it, v + accumulator)
}
return ↦ accumulator
}
Когда мы определяем сопроцедуру, не замыкая внутрь объектов (значения и псевдозначения замыкать можно), сама сопроцедура представляет из себя псевдозначение:
::performSomeCalculationCPS : ( (x : X, cont : (Y) ⊸ Nothing) ⊸ Nothing )!
::useThatCalculation : (Log▸(X) ⊸ Y)!
Можно создать анонимную сопроцедуру, и целиком передать внутрь сопроцедуры объекты (ownership transfer), которые в этом случае должны быть там истрачены или тем или иным способом переданы дальше — в этом случае сопроцедура будет иметь тип вида (*Xs) ⊸ Y.
При помощи нехитрой трансляции в экспериментальный язык Rast из вышеупоминавшейся статьи [Das-Pfennig20] можно показать, что в терминах сопроцедур и structured concurrency мы можем создавать имплементации всех типируемых в описанном нам исчислении объектов.
В 1987 году J.-Y. Girard разработал обобщение одновременно классической и интуиционистской логики высказываний удивительной элегантности, называемое линейной логикой. Обычная логики высказвываний позволяет соединять высказывания X и Y в составные высказывания, такие как X ⇒ Y, X ‹and› Y, X ‹or› Y. Интуиционистски-параллельный фрагмент линейной логики позволяет аналогичным образом комбинировать интерфейсы X и Y объектов при помощи следующих комбинаторов:
X ⊸ Y — линейная импликация,X ⊗ Y — наличие двух объектов,X & Y — наличие одного из двух объектов на выбор потребителя,X ⊕ Y — наличие одного объекта, интерфейс которого X или Y, причём потребитель может выяснить какой именно из двух,X ⅋ Y — наличие одного объекта, интерфейс которого X или Y, причём потребитель не может выяснить какой именно из двух,
и обязан обрабатывать параллельно оба варианта (имея возможность сделать join результатов в конце)X! — replicatable service интерфейса X.Все комбинаторы, исключая последний могут быть реализованы в терминах сопроцедур. Для определения X ⅋ Y нам потребуется structured concurrency: требуется уметь запускать сопроцедуры параллельно (launch) и совершать джойны, что в Котлине обеспечивается сочетанием команды !throw и блока coroutineScope, заверщающегося сразу как только любой из запущенных процессов использует команду !throw, и возвращающего значение переданное в эту команду. Связку ⅋ можно рассматривать как separating conjunction * присущий фабрике coroutineScope.
Для описания свойств данных и чистых функций используется исчисление предикатов, основывающееся на классической логике высказываний. Для описания свойств объектов нам нужен аналог исчисления предикатов, но основывающийся на интуиционистско-параллельном фрагменте линейной логики ILL⅋. Это искомый нами математический фундамент для мультипарадигменных языков программирования.
Stratified Kotlin оперирует как значениями, так и объектами. Выше мы рассказали, что для рассуждения о значениях используется исчисление предикатов, и убедились, что для рассуждения об объектах можно использовать линейную логику. Чтобы рассуждать о программах на Stratified Kotlin в целом, нам понадобится исчисление, сочетающее в себе линейную логику и исчисление предикатов. Такое исчисление недавно ввели Frank Pfenning et al. под названием adjoint logic/adjoint type theory. Мы приведём ссылки на основопологающие статьи по этой тематике, но отметим что adjoint type theory далека от своей окончательной формы и является предметом активных научных исследований, которыми в частности занимается и автор этого текста. Данный текст — вклад в разработку adjoint type theory со стороны практики программирования.
TODO: Описать практическую сторону сопряженных модальных операторов, позволяющих выражать линейную импликацию через монады или комонады (C<X>)-> Y ≡ (X)⊸ Y ≡ (X)-> M<Y>. Описать практическое применение — обратную CPS-translation, при помощи которой императивный quicksort может быть повышен до “чистой функции“, благодаря тому что вся используемая внутри мутабельность и эффекты инкапсюлированы (“никак не проявляются наружу”, и показать что результат эквивалентен чисто функциональной имплементации mergesort.