Когда-то Tony Hoare назвал null pointers “ошибкой на миллиард долларов”. В истории языков программирования есть кое-что обходящееся, вероятно, ещё дороже: игнорирование фундаментальной разницы между данными и объектами.
С рождения мы воспринимаем окружающий мир и процессы в нём через картины и ощущения, и этого достаточно для мышления при помощи эвристик аналогий. Но чтобы сделать возможными чёткие инструкции и строгие рассуждения, необходимо провести условные границы и разложить мир на идеализированные единицы моделирования — объекты. В зависимости от предметной области это могут быть, например, яблоки и груши, ордера и квитанции, поезда и станции или электроны и фотоны. Мы учимся этому, когда учимся говорить и думать словами, а оттачиваем, занимаясь программированием (по части «чётких инструкций») и математикой (по части «строгих рассуждений»). Канонические примеры материальных объектов в программировании — ячейка памяти, содержащая изменяемое целочисленное значение, и program-level POSIX среда, в которой запускается программа.
Теперь допустим, что мы считали значение из ячейки памяти и взвесили яблоко, установив, что X.value = 2 и Apple1.weight = 93g. Упоминающиеся тут ячейка памяти X и яблоко Apple1 — материальные объекты, а вот «целое число 2» и «93 грамма» — платонические “объекты”, существующие исключительно в мире математических абстракций. В их отношении мы будем применять термины данные (мн.ч) и значение (ед.ч). Данные — информация, отделённая от носителя и контекста.
К объектам применимо понятие “тот же самый, один и тот же” (same). Так в двух разных ящиках могут лежать равные числа, но это не делает их одним и тем же ящиком — если в одном поменять значение, оно не поменяется в другом. Объекты могут возникать/порождаться и исчезать/поглощаться, к ним применимо понятие жизненного цикла (lifecycle).
К значениям, применимо понятие “равный” (equal), но не “тот же”. Быть равными — это свойство пары значений: равенство может быть доказано или опровергнуто, а вот быть одним и тем же объектом можно только по определению. Более того, невозможно вообще корректно определить пару из объекта с самим собой — пара объектов это автоматически пара двух разных объектов. Также неприменимо к значениям понятие жизненного цикла, про них даже нельзя сказать что они “всегда были и будут” — они просто вне времени и материального мира.
Теперь, ознакомившись с базовыми понятиями и обрисовав фундаментальные различия, разберёмся зачем проектировать языки программирования с учётом этих различий. Но прежде, чтобы твёрдо почувствовать разницу между объектами и данными, разберём её на примерах. В примерах я буду пользоваться вымышленным языком с синтаксисом на основе Kotlin'а.
Каждый программист встречается на практике с массой примеров объектов. Давайте обсудим некоторые разновидности объектов с конкретными примерами, чтобы иметь перед глазами материал для дальнейших рассуждений.
Ресурсы и Аксессоры
Самый распространённый объект в программировании — так называемые ресурсы и аксессоры к ним. Например в следюущем коде открывается файл ./storage.dat, пока в момент открытия создаётся объект-аксессор к файлу, и в тот момент когда этот объект закончит свой жизненный цикл, файл снова станет доступен для открытия. Обратите внимание, что файл можно открыть как на чтение-и-запись, так и только для чтения и в зависимости от этого у объектов-аксессоров будут разные интерфейсы (будет доступна или наоборот недоступна команда write()):
with(open("./storage.dat")) {
// here `this` will refer to the file accessor object
// we may use `read` and `write` commands
}Притом один и тот же файл может быть одновременно открыт на чтение много раз. Базы данных и очереди (message queues) допускают также и многократное открытие “на запись”.
Некоторые ресурсы таковы, что мы можем разбить их время на изолированные части. Например, изменяемый массив можно разбить на любое количество подмассивов с непересекающимися индексами:
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). К фабрикам относятся и файловые системы, позволяющие создавать в их рамках каталоги и файлы.
Одноразовые объекты
Самые простые с точки зрения lifeсycle объекты — объекты одноразового использования. Ниже пример корутины, принимающей в качестве аргумента cont строго одноразовый объект — подвешенный процесс, ожиданиющий значения типа X:
suspend fun f(..., cont : Continuation<X>) {
...
}Вызов cont(x) может быть последним действием f, а может быть cont будет в какой-то момент запущен отдельным потоком при помощи launch {cont(x)}, или передан в какое-нибудь хранилище подвешенных процессов для дальнейшей реактивации. Важно, что по какому бы сценарию не пошло выполнение f, объект cont должен быть использован, причём ровно один раз.
Встречаются и подвешенные процессы, возвращающие результат типа Y, их тип обозначают (X)⊸ Y, причём Continuation<X> = (X)⊸ Nothing, где Nothing пустой тип, тип не содержащий ни одного значения. Значок ⊸ называется линейной импликацией.
Генераторы и Сервисы
Генераторами называются потенциально бесконечные процессы, время от времени генерирующие значения типа T при помощи команды yield(x : T). Корутина, принимающая на вход генератор, может по надобности запрашивать следующий такой объект:
suspend fun f(args, gen : Generator<T>) {
val x := gen.next()
...
val y := gen.next()
...
}При каждом вызове запроса gen.next() команда next() на как бы поглощает поглощает имеющийся объект gen и подменяет его новым gen, находящемся в следующем состоянии.
Сервисы — обобщение генераторов: они могут поддерживать несколько разных запросов (скажем, ask и say), запросы к ним могут принимать аргументы (скажем, ask(prompt) и say(message)):
with<Tty> suspend fun foo() {
var total := 0;
repeat {
total += ask<Int>("Please enter a number")
say("Sum of entered numbers is $total")
}
}Сервисы представляют собой наиболее общий вид объектов в программировании, включающий все предыдущие, характерным примером сервиса сочетающего в себе одновременно всё является program-level POSIX-среда Env. Внешние по отношению к компьютеру физические объекты, такие как живой пользователь, аппаратный генератор случайных чисел, а в недалёком будущем ещё и квантовый регистр на n кубитов, с точки зрения интерфейса ничем не отчаются от сервисов, кроме того что ведут себя (по крайней мере с точки зрения компьютера) недетерминированно.
С практической точки зрения можно думать о данных, как о том что можно передать через сеть. Это не совсем точный, но очень удобный практический критерый — компьютерные сети позволяют передавать информацию, но не физические объекты. А данные, как мы определили выше — отделённая от носителя и контектса информация. Так мы не можем передать через сеть изменяемую ячейку памяти или переферийное устройство (скажем, принтер, печатающий передаваемый ему текст на бумаге). Мы можем предоставить к ним через сеть доступ, но сама ячейка или само устройство останутся там, где были. А вот число, строку или набор строк мы можем передать по сети.
Все цифровые компьютеры поддерживают как минимум один базовый тип значений: ограниченные по длинне целые числа. На подавляющем большинстве компьютеров это числа, которые в двоичном представлении состоят не более из 63 цифр, так называемых битов. Ещё один бит, 64ый, используется для хранения информации о знаке числа (то есть о том, положительное оно или отрицательное).
Нечисленные значения не поддерживаются компьютером напрямую, но их можно хранить в оперативной памяти и кодировать при помощи последовательностей чисел — так они в конечном счёте передаются через компьютерные сети или хранятся на диске.
В высокоуровневых языках программирования появилась возможность передавать между частями программы нечисловые, составные значения. В особенно высокуровневых языках (например, Python) даже наиболее распространённый тип — тип целых чисел Int по умолчанию является типом неограниченных по длинне целых чисел, а типы ограниченных имеют специальные названия, указывающие на максимальную длину (Int64).
К несчастью по историческим причинам в очень многих языках не проводится чёткой границы между передачей составного значения (скажем, фиксированной строки) и передачей указателя на изменяемую структуру данных. Тут нужно помнить — сам указатель (номер ячейки памяти) будучи переданным по сети на другой компьютер теряет смысл, а изменяемая структура данных — физический объект, и её нельзя куда-либо передать — можно передать только её моментальное состояние, вот оно-то и является значением, данными.
Наряду со списками List<T> значений типа T очень важными типами данных являются конечные множества FinSet<T> и таблицы “ключ-значение” Map<X, Y>, представляющие из себя конечное множество пар (x : X, y : Y) с неповторяющимися xами.
Ключевое свойство высокоуровневых языков, которое, к сожалению, редко выполняется — непроницаемость абстракции. Если язык позволяет написать, что наша программа получает список чисел или множество строк на вход, нашей программе должно быть совершенно безразлично, как именно закодированы при передаче по сети и как представлены в памяти эти списки чисел и множества строк, программа должна быть инвариантна относительно представления.
В самом начале этого раздела я сказал, что критерий “можно передать по сети” не совсем точен. Дело в том, что значения не обязаны быть конечными. Бесконечная последовательностей битов Seq<Bit> тоже является информацией — в математическом смысле это значение, данные. Но передать по сети за конечное время мы её не можем. Тут есть, однако, хитрость: в программировании мы обычно встречаем вычислимые последовательности целых чисел (скажем, последовательность Фибоначчи), и вот алгоритм её вычисления мы можем передать по сети. Очень важно подчеркнуть разницу между последовательностью Seq<Bit> и генератором Generator<Bit>: в качестве генератора может выступать аппаратный генератор случайных чисел или даже живой человек, нажимающий по запросу на кнопки yes/no, тогда как последовательность Seq<Bit> это единое значение, она сразу определена на всю свою длину.
Наряду с бесконечным обобщением списков (последовательностями) в программировании очень часто встречаются так называемые чистые функции — это бесконечные обобщения таблиц ключ-значение, с дополнительным требованием что каждому “ключу” x : X соответствует какое-то значение y : Y. Тип чистых функций обозначают X -> Y. К слову, Seq<T> это то же самое, что Nat -> T, то есть функция, сопоставляющие значения типа T натуральным числам.
На практике всякая чистая функция обычно будет задана алгоритмом вычисления, но думать о ней нужно как о бесконечной таблице. Тот факт, что она задана алгоритмом, и то как именно этот алгоритм кодируется, и как исполняется — технические детали реализации, а программы должны быть инвариантны относительно способа физического представления данных. То есть, программа, принимающая на вход бесконечную последовательность чисел или функцию, заданную на бесконечном типе, должна обращаться с ними так, как если бы они были именно бесконечными последовательностями/бесконечными таблицами, и игнорируя тот факт что на самом деле они заданы алгоритмами.
(Примечание: алгоритмы вообще говоря могут не всегда завершаться за конечно время. То есть при некоторых наборах входных данных они могут входить в бесконечный цикл. Если алгоритм, задающий последовательность Seq<T> или функцию (X)-> Y зависает — это ошибка программиста, и она на совести программиста. Компилятор имеет право исходить из того, что все алгоритмы завершаются. На случай если возможность незавершения алгоритма — это не ошибка, а так и задумано, особо продвинутые языки программирования имеют специальный тип T¿, называемый “алгоритм, вычисляющий T, либо зависающий”.)
Пользуясь тем, что чистые функции это значения, мы можем задавать и функции, принмающие другие чистые функции как значения. Например функцию map : (List<X>, (X)->Y)->List<Y>, которая применяет чистую функцию f : (X)-> Y поэлементно к списку list : List<X>, получая таким образом новый список типа List<Y>. Такие функции называются функциями высшего порядка, и их понимание очень важно для нашего текста. Понимание, что одна чистую функция может примать другую чистую в качестве аргумента, очень помогает осознать нетривиальный для многих факт, что чистые функции являются не объектами, но данными.
Первый в современном понимании язык программирования появился в 1957 году, это был FORTRAN. Как и во всех современных императивных языках, программа на Фортране представляет собой последовательность инструкций. Два основных вида инструкций — определения a := 1 и команды print("Hello"). Внутри определений и в качестве аргументов команд могут использоваться выражения:
val a := 60 · 60 · 24
print("1 day / 1 sec = " ++ a)Выражения — синтаксическое понятие, пришедшее в программирование из математики. Выражения описывают путь вычисления значения, и должны быть взаимозаменимы с этим значением. То есть, если вместо выражения сразу подставить его результат, программа не должна измениться. Выражения представляют из себя деревья применения функций к значениям:
60 · 60 · 24
============
60 60
^^ ^^
(·) 24
^^^ ^^
(·)
К сожалению, подавляющее большинство императивных языков программирования не различают чистые функции — функции, детерминистски вычисляющие значение из аргументов, без всяких побочных эффектов — и команды, которые возвращают значение вообще говоря не детерминированное своими аргументами, и при выполнении которых могут производиться необратимые действия, такие как например удаление файлов. В таких языках можно использовать команды в качестве функций внутри “выражений”. Мы будем использовать термин псевдовыражения для “выражений”, содержащих хотя бы одну команду.
Чистую функцию можно задать выражением (в этом случае выражение называют телом функции), но не псевдовыражением: псевдовыражение содержит хотя бы одну команду, а значит функция заданная им будет иметь недетерминированный результат или побочные эффекты, а значит не будет чистой функцией. Отметим, что важно не отождествлять функцию и выражение, которым она задана. После того как функция определена, у нас нет способа “посмотреть внутрь”, не нарушая законы абстракции. Функция семантический элемент (с семантикой “бесконечная таблица ключ-значение”), а выражение элемент семантический, и тот факт что та или иная функция задана каким-то выражением — деталь реализации, которая должна быть скрыта абстракцией.
На первый взгляд функции и команды логично объединить — и те, и другие могут принмать аргументы и возвращать значения. Объединение даёт экономию концепций и таким образом как будто уменьшает сложность языка, что же тут может быть плохого? Проблема в том, что нельзя больше рассчитывать, что “выражения” взаимозаменимы со своими значениями. Теряется удобная ментальная модель, позволяющая думать о программе, просто смотря на неё. Теперь во всяком безобидно выглядящем “выражении” может скрываться плохо предсказуемое поведение.
Давайте рассмотрим две самые безобидные с точки зрения поведения команды:
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, позволяющие оперировать напрямую не только данными, но и объектами. Но как распространить на них вышеописанные преимущества функциональных языков?
В предыдущем разделе мы поговорили о том, какие практические преимущества для языков программирования предоставляет наличие стройной и исчерпывающей семантики, прозрачно соответствующей синтаксису. Целью нижеследующего текста будет достижение того же для языка программирования, способного наравне со значениями оперировать объектами и поддерживающего concurrency. Кстати, именно такие языки называют мультипарадигменными. В данный момент наиболее развитыми среди распространённых мультипарадигменных языков программировани являются Kotlin, Rust и Scala.
У каждого из этих языков есть преимущества, которых лишены два других.
- Scala (Scala 3) обладает доброкачественной системой типов, поддерживающей обобщённые типы высшего порядка, а также поддерживает тайп-классы высшего порядка.
- Rust содержет механизмы structured lifetime and ownership management объектов.
- Kotlin поддерживает корутины и structured concurrency на их основе, а также имеет ряд механизмов, ключевых для обращения с объектами, имеющими нетривиальный жизненный цикл — smart casts и typesafe builders.
Внутри каждого мультипарадигменного языка имеется чисто-функциональный язык — функциональное ядро. В ходе нижеследующего текста мы сперва урежем 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; - внутри классов и объектов-компаньонов запрещаются изменяемые поля, в результате чего все типы данных становятся рекурсивно иммутабельными (hereditarliy immutable);
- равенство значений не может быть переопределено программистом, а выводится автоматически — покомпонентно, как для data classes;
- не существует никакого технического способа проверки равенства “адресов объектов в памяти“, и никаких механизмов runtime-интроспекции.
Мы можем разрешить использование локальных переменных var и циклов while и repeat/while, т.к. они могут быть сведены к рекурсии. Отметим, что и локальные определения val x = expr тоже могут быть сведены к применению и абстракций функций.
Для лучшего соответствия принятым в математике обозначениям и стандартам, мы также будем
- использовать тип
Intдля обозначения потенциально неограниченно больших по модулю целых чисел, как в Python3; - интерпретировать бинарные операторы на числоподобных типах не как методы первого операнда, а как поля соответствующего объекта-компаньона/тайпкласса, и
- использовать скобки для превращения бинарных операторов в функции и одинарные одинарные угловые кавычки для превращения функций (бинарных или vararg) в бинарные операторы:
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.
Первая часть - достаточный ХДЫЩ в голову, чтобы быть отдельной статьёй :)