Обобщённые типы. Часть 1/3. Полиморфные типы высокого рода / forpes.ru

Главная
Обобщённые типы. Часть 1/3. Полиморфные типы высокого рода

Обобщённые типы. Часть 1/3. Полиморфные типы высокого рода

13.04.2024 11:08

Underskyer1 3 4300 Источник

Теория типов способна дать ответы даже на очень сложные вопросы. Осталось только научится правильно формулировать вопросы.

В предыдущей статье раскрывались некоторые базовые понятия теории типов. В этот раз мы рассмотрим обобщённые типы (generics) – необходимость появления такой абстракции, ключевые особенности и различные сценарии использования в программировании.

Предисловие

Однажды я делал доклад для сотрудников о технических решениях на одном из наших Scala-проектов. Там рассказывалось про применение монадических трансформеров, Tagless Final и прочих ФП-шных вкусностей. После доклада по обратной связи я получил в числе прочих и вопрос, который звучал примерно так: "а зачем вообще нужны обобщённые типы?". В тот момент я не был готов к такому вопросу и пообещал, что в следующий раз обязательно раскрою эту тему.

При подготовке ответа выяснилось, что тема обобщённых типов очень обширна. То, что подсказывал интернет, даже если бы и удовлетворило любопытство спросившего, но не убеждало меня. Обычно там говорятся общее слова, мол, обобщённые типы дают "типобезопасность", "оптимизацию" (не требуется явное приведение к типам-значений и т.п.), "переиспользуемость" и прочая "вода". Зачастую, далее приводится пример, в котором раскрываются преимущества типизированных (обобщённых) коллекций над нетипизированными... Однако, во многих языках программирования со строгой типизацией уже есть встроенные типизированные коллекции со своими методами, например, массивы. Выглядит так, что будто бы и нет необходимости давать программистам возможность создавать свои обобщённые типы?

На самом деле, полезными бывают, конечно же, не только типизированные списки и методы для работы с ними. Кроме того, “обобщённые типы” – это лишь одно из нескольких названий, каждое из которых выделяет определённые аспекты этой концепции. В данной статье мы рассмотрим обобщённые типы во всём их многообразии с различных точек зрения.

Так же как и предыдущая статья, эта не является подробным учебником с систематическим изложением материала. Основная задача – поверхностный обзор темы с самых разных точек зрения, с тем, чтобы заинтересовавшийся каким-либо аспектом читатель смог найти подробности самостоятельно. Далее предполагается, что читатель уже знаком с базовыми понятиями теории типов (см. например, предыдущую статью).

Для примеров кода в статье выбран язык Scala 3. Да, мало в каких популярных языках есть поддержка типов высокого рода (HKT), или контекстных абстракций, как в Scala, но многие высказанные тут утверждения относительно обобщённых типов справедливы для большинства языков программирования, поддерживающих эту абстракцию. Выразительные возможности третьей версии Scala дают возможность очень наглядно продемонстрировать некоторые интересные особенности обобщённых типов.

Обобщённые типы

Мотивация

Представим, что у нас есть функция, которая может завершится ошибкой, которую в дальнейшем можно будет обработать. Это может быть поиск элемента в коллекции (искомого значения может не найтись), или запрос на web-сервер (тут может быть много разных ошибок). В привычном императивном программировании для работы с ошибками обычно применяется механизм выброса исключений и их отлов. Такой подход, как правило, недекларативен – по сигнатуре функции нет возможности понять, какие "несчастливые" исходы вычисления возможны. В любом случае, такие механизмы усложняют язык, вводя новые синтаксические конструкции, вроде try/catch.

В то же время, с использованием понятия суммы типов сигнатура таких функций может выглядеть следующим образом:

$findItem: RegEx \Rightarrow ItemType + NotFound$ $\begin{split} getSmthFromWeb:{}& Request \Rightarrow Response + {}\\ Unaccessable + {}& BadRequest + InternalError \end{split}$

При такой записи явно выделяются возможные исходы вычислений. Благодаря очевидному алгебраическому изоморфизму, описанного в предыдущей статье, для каждой такой суммы типов однозначно определяется функция, которая из значений этого типа вычисляет значения произвольного типа – механизм сопоставления с шаблонами проверяет, чтобы программист предоставил функции в тип из всех типов-слагаемых:

def foldToString(itemOrNot: ItemType | NotFound)( // ItemType + NotFound
  itemToString: ItemType => String,  // на вход приходят две функции
  notFoundResult:   Unit => String   // по количеству слагаемых типа
): String = 
  itemOrNot match     // тело функции не зависит от конкретного ItemType!
    case it: ItemType => itemToString(it)
    case _: NotFound  => notFoundResult()

Здесь объединение типов ItemType | NotFound можно считать суммой типа ItemType и единичного типа NotFound.

И поиск элемента в коллекции, и загрузка контента из веб-сервиса являются весьма распространёнными сценариями, которые неоднократно встречаются во многих приложениях. При этом, конкретные типы ItemType, или Response будут различаться в разных местах, но способы использования результирующих значений типов суммы – реализации методов fold – не будут зависеть ни от ItemType, или Response! Более того, различные реализации метода fold будут отличаться только заменой типа ItemType (или, аналогично, Response) на какой-нибудь другой. Многократное дублирование этого кода для каждого такого конкретного "типа-параметра" выглядело бы весьма неудачным решением...

Помимо сценариев с суммами типов, рассмотрим и другие. Например, если какой-либо метод ищет некий контент на разных ресурсах, было бы полезно вместе с результатом вернуть и сведения об первоисточнике, откуда этот контент был получен. Тут уже поможет произведение типов Content × Source, где тип Content может отличаться в разных конкретных случаях, а Source – это фиксированный тип, например, String. В таких случаях способы использования такого кортежа на основе проекторов в типы Content и Source не будут зависеть от того, какой именно тип-параметр Content будет там использоваться.

def foldToInt(contentWithSource: Conent & Source)( // Conent × Source
  handler: Conent => Source => Int  // на вход приходит каррированная функция
): Int = 
  // обработчик handler вполне может игнориовать свой второй параметр source
  handler(contentWithSource: Conent)(contentWithSource: Source)

Ещё один популярный сценарий – "избавление от зависимостей". Если в неком методе требуется использование какого-то сервиса типа Service, то обычно его называют зависимостью и передают в самом начале, например, вместе "бизнесовыми" параметрами метода (или же по-ООП-шному, чуть раньше – в конструктор класса, где реализован метод). Получается, так называемый, "жадный" захват зависимости. Сигнатура вычисления примерно такая: (Service, BusinessParam) => Result. "Жадному" механизму противопоставляется "ленивый", когда метод не требует предоставление зависимости в самом начале, но возвращает функцию, которая на вход требует только значение Service, и сигнатура будет уже другая: BusinessParam => (Service => Result). Получается, что каррирование помогло избавить метод от зависимости! Таким образом, всю бизнес-логику можно описать чисто, вынеся всю работу с зависимостями в самый конец приложения, оставить это библиотечным методами или среде исполнения. В такого рода сценариях наблюдается знакомая закономерность – способ использования значений экспоненциального типа Service => Result не зависит от типа Result, он является параметром метода:

def foldToResult(
  resultByService: Service => Result)( // Resultˢᵉʳᵛⁱᶜᵉ
  service: Service                     // на вход приходит сервис
): Result = 
  resultByService(service)             // что такое Result - не важно!

Можно привести и другие аналогичные сценарии, в которых конкретизация некоторых типов (вроде Result, Content, Response, ItemType) не нужна – в разных вариантах это могут быть самые разные типы, но паттерн остаётся тем же самым! Было бы весьма расточительно многократно копипастить такие функции, отличающиеся лишь своей сигнатурой, но имеющие одинаковую реализацию.

Для решения такой проблемы необходима новая абстракция – обобщённые методы.

Обобщённые методы

Идея простая – достаточно описать единственную обобщённую функцию, которая будет описывать все варианты сценария с различными конкретными типами, передаваемыми ей как параметры. В Scala параметры-типы передаются не в круглых скобках, как обычные аргументы, а в квадратных. Перепишем методы fold, объявленные в предыдущем примере, в обобщённой форме:

def foldToString[ItemType](itemOrNot: ItemType | NotFound)( // ItemType + NotFound
  itemToString: ItemType => String,  // на вход приходят две функции
  notFoundResult:   Unit => String   // по количеству слагаемых типа
): String = ???                      // реализация такая же, как и раньше

def foldToInt[Conent](contentWithSource: Conent & Source)( // Conent × Source
  handler: Conent => Source => Int  // на вход приходит каррированная функция
): Int = ???                        // реализация такая же, как и раньше

def foldToResult[Result](resultByService: Service => Result)( // Resultˢᵉʳᵛⁱᶜᵉ
  service: Service                  // на вход приходит сервис
): Result = ???                     // реализация такая же, как и раньше

Использовать их можно так:

val doubleOrNot: Double | NotFound = 4.2
val str = foldToString[Double](doubleOrNot)(d => s"double: $d", _ => "no double found")
//                     ↑↑↑↑↑↑ - тип-параметр указан явно (но это не обязательно)

val intOrNot: Int | NotFound = 42
val str = foldToString(intOrNot)(i => s"int: $i", _ => "no int found")
//                   ↑↑ - зачастую, тип-параметр компилятор и сам может вывести

Тут обобщённый метод foldToString, определённый единообразно для любого конкретного типа ItemType, используется со значениями разных типов: Double и Int. Причём во втором случае тип не указан явно – компилятор сам определяет его по типу первого параметра метода.

Телом обобщённых методов являются выражения, в которых используемые там термы могут быть любого, не известного заранее типа. Такие типы участвуют в выражении свободно – они могут меняться в зависимости от контекста использования этого выражения. Метод же образуется путём связывания всех свободных параметров выражения с параметрами, которые нужно передать в метод (замыкания сейчас не рассматриваем). В случае обобщённых методов некоторыми из таких параметров будут типы.

В типах аргументов представленных выше обобщённых методов ItemType | NotFound, Conent & Source, Service => Result упоминаются неопределённые типы-параметры ItemType, Conent и Result. То есть, параметризация методов типами отразилась прежде всего на типах их аргументов и результата.

Часто бывает полезно параметризировать типом не один метод, а целую группу. ООП-шные языки программирования, в том числе и Scala, предлагают собирать группу методов в классы. И в нашем же случае это будут уже обобщённые классы.

Обобщённые классы

Типы-параметры обобщённых классов в Scala указываются в квадратных скобках сразу после имени класса.:

case class ContentAndSource[Content](content: Content, source: String)

trait ContentHandler[Content, Result] {
  def handleContent(contentAndSource: ContentAndSource[Content]): Result
}

Чтобы создать экземпляр обобщённого класса, помимо значений-параметров конструктора, нужно конкретизировать и типы-параметры:

case class MyContent(test: String) // будем подставлять его как тип-параметр

val contentHandler = new ContentHandler[MyContent, String] {
  def handleContent(contentAndSource: ContentAndSource[Content]) =
	  s"Из источника '${contentAndSource.source}' получено содержимое: ${contentAndSource.content.text}"
	  //                                    используем проектор конкретного класса MyContent.text ↑↑↑↑
}

val myContentAndSource = ContentAndSource(MyContent("text"), "hardcoded")
//                                      ↑↑ необязательно указывать тип - он будет выведен автоматически

val str = contentHnadler.handleContent(myContentAndSource) // String
// "Из источника 'hardcoded' получено содержимое: text"

Практически о всех ФП-шных Scala-библиотеках обобщённые типы представлены именно как обобщённые классы (и трейты). Это обусловлено, в частности, полезностью разграничения контекстов – определённые через классы, типы считаются разными, даже если реализованы они одинаково. Это значит, что применимые к ним наборы функций не будут пересекаться. В то же время, с рассматриваемыми в следующей главе псевдонимами λ-выражений типов ситуация обратная – типы сравниваются по формулировке, а не по названию, значит, могут быть (потенциально нежелательные) коллизии между наборами функций, предоставляемыми для этих типов разными библиотеками. Избежать таких нежелательных коллизий возможно и ФП-шными средствами Scala, но, проще и привычнее использовать классы.

Говоря об обобщённых классах Scala стоит упомянуть такую особенность JVM, как “стирание типов”. Дело в том, в JVM экземпляры обобщённых классов не хранят информацию о типе-параметре. При компиляции такого кода

def checkType[A](xs: List[A]) = xs match
  case _: List[String]  => "Список строк"
  case _                => "Что-то ещё"

будет выведено предупреждение

the type test for List[String] cannot be checked at runtime because its type arguments can't be determined from List[A]

Этот код всегда будет сворачивать на первую ветку, независимо от типа-параметра: при передаче в функцию List(4, 2) она всё равно вернёт "Список строк". Дело в том, что механизм сопоставления с шаблонами проверяет типы значений не на этапе компиляции, а во время выполнения. Для этого он пытается вытащить через отражения информацию о классе, конструктором которого было создано это значение, и сравнить её с шаблоном типа. Но так как там нет упоминания конкретного типа-параметра, код хоть и скомпилируется, но будет работать не так, как можно было бы ожидать. Такую “фишку” JVM всегда стоит иметь ввиду при работе с обобщёнными классами, а любые проверки типов стоит стараться выносить на этап компиляции.

Рассмотрим также понятие “обобщённые алгебраические типы данных“ (generalized algebraic data type, GADT). Термин, появившийся изначально в среде хаскелистов относится к типам, представимым в виде сумм других типов. В терминологии ООП сами классы описывают типы произведения своих членов (полей и методов, суть значений функционального типа), а суммы типов определяются через наследование – тип суперкласса является суммой типов подклассов (желательно, но не обязательно, чтобы наследование было ограничено “запечатыванием” и “финализацией”):

sealed trait CalcResult[R] // CalcResult[R] ≅ String + R × Rᶜᵃˡᶜᴼᵖᵗⁱᴼⁿˢ
final case class Error(msg: String)    extends CalcResult[Nothing]
final case class Successful[R](res: R) extends CalcResult[R]:
  def recalcWithOptions(options: CalcOptions): R = ??? // (CalcOptions => R) ≡ Rᶜᵃˡᶜᴼᵖᵗⁱᴼⁿˢ

Здесь запечатанный трейт CalcResult[_] определяет обобщённый алгебраический тип данных, представляющий сумму типов, связанных с финальными классами-наследниками Error и Successful[_]. Далее же мы рассмотрим более ФП-ориентированные способы определения подобных типов.

Конструкторы типов

Термин "конструкторы типов" буквально отражает идею возможности построения новых типов из существующих. Единожды описав такой конструктор (или используя встроенные) можно создавать новые типы, подставляя разные известные типы в этот конструктор. Термин отражает функциональную природу обобщённых типов – это, по сути, отображения из типов в тип (а не из значений в значения, как обычные функции).

Любая функция строится вокруг некоторого выражения, которое становится её телом. Поэтому в первою очередь рассмотрим, какие выражения над типами можно использовать в языке Scala.

Встроенные операции над типами в Scala

В Scala 3 есть такие конструкции для построения новых типов из существующих:

просто тип A – случай настолько тривиальный, что легко упустить его полезность,
кортеж (A, B, C) – суть тип-произведение,
объединение типов A | B – если типы разные, то это аналогично их сумме,
пересечение A & B – если типы разные, то это аналогично их произведению,
"вызов" другого конструктора типов, например,
- A => B – тут используется псевдоним для Function[A, B],
- A Either B – синоним для Either[A, B],
- Option[A], Map[K, V],
- MySupperClass[A, B, C] – конечно, можно вызывать и конструкторы типов, связанных с классами (или трейтами), не определёнными в стандартной библиотеке Scala.
сопоставление с шаблонами для типов.

Ремарка о сопоставлении с шаблонами для типов

Механизм сопоставления с образцом для типов сочетает в себе несколько разных аспектов: специальный полиморфизм, зависимые типы, деконструкция дерева выражений. Только первый пункт имеет прямое отношение к обобщённым типам и он будет рассмотрен далее. Два оставшихся аспекта выходят далеко за рамки темы этой статьи, поэтому и механизм сопоставления с образцом здесь не будет рассматриваться.

Комбинируя эти конструкции можно определять типы произвольной сложности:

type Action  = NoAction | ((Service1 & Service2) => MyIO[(SingleResult Either List[AltResult], Log)])
//             ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑
//                       Вот такое кучерявое выражение получилось. Конечно, можно и длиннее ?

Функции над типами

Идентификаторы, которые используются в выражении, могут относится как к известным в текущем контексте конструкциями, так быть неопределёнными, свободными переменными. Чтобы иметь возможность вычислить выражение, можно построить функцию, связать все свободные переменные выражения с параметрами, которые требуется передать при вызове этой функции.

С этой точки зрения удобно рассматривать и обобщённые типы – это функции, отображающие из одного или нескольких типов в тип. Аналогия обобщённых типов Scala с обычными функциями нагляднее прослеживается в объявлениях псевдонимов типов с помощью ключевого слова type:

type Union[A, B]          = A | B                     // объединение типов
type OrErrorAndContext[X] = Union[(X, String), Error] // "вызывается функция" (конструктор типов) Union

Действительно, похоже на определения обычных функций, только "тип" аргументов и результата нигде не указывается. У них у всех одинаковый "тип" – это тип!?

В Scala 3 также есть возможность использовать литералы обобщённых типов – λ-выражения типов:

type    WithContext = [A] =>> (A, String) // псевдоним типа, опеределённый через λ-выражение 
type IntWithContext = WithContext[Int]    // "вызвали функцию" WithContext с аргументом Int и получили (Int, String)

Опять же, синтаксис похож на обычные λ-выражения.

Для обобщённых типов, принимающих ровно два аргумента, возможна инфиксная запись, которая иногда бывает полезна, а иногда – не очень:

// если такой код компилируется, значит использованы эквивалентные типы по обе стороны =:= 
summon[(Either[String, Int]) =:= (String Either Int)]     // близко к естественному языку "строка или целое число"
//      ↑↑↑↑↑↑ обычная запись            ↑↑↑↑↑↑ инфиксная запись 
summon[(Function[String, Int]) =:= (String Function Int)] // а с таким типом инфиксная запись читается хуже

С другой стороны, Scala позволяет объявлять идентификаторы, состоящие из специальных символов, что может повысить читаемость:

type =>[A, B] = Function[A, B] // такой псевдоним уже есть в стандартной библиотеке
type  ×[A, B] =         (A, B) // новый псевдоним для типа произведения

// используем псевдонимы из спец-сиволов в инфиксной форме:
val func: Int => String = _.toString
val pair: Int ×  String = (5, "пять")

Важно отметить, что с помощью ключевого слова type объявляются не сами типы, а псевдонимы выражений типов. Т.е. это некие синтаксические деревья, которые можно нарастить, например, в другом определении псевдонима типа, или же преобразовать с помощью упомянутого ранее механизма сопоставления с шаблонами типов. Эти выражения вычисляются в процессе типизации конкретных термов (например, переменных). С помощью различных построений псевдонимов типов можно получить схожие деревья выражения, дающие в итоге одинаковые типы, что не всегда может быть желанным результатом. Семантически различимые новые типы в Scala можно ввести только описав новые классы (трейты, объекты), либо используя литеральные типы. Работа с синтаксическими деревьями выходит за рамки данной статьи.

Каждый тип характеризуется набором функций-стрелок, связывающих одни типы с другими. Обобщённые типы позволяют связывать между собой любые такие наборы стрелок с помощью функций, определяемых телом обобщённого типа (комбинации сумм, произведений, экспоненциалов и т.п.):

Обобщённый тип F[_] связывает с помощью проекторов произведения типов фиксированный тип B с типом, который может быть подставлен в тело F вместо A. — Обобщённый тип `F[_]` связывает с помощью проекторов произведения типов фиксированный тип `B` с типом, который может быть подставлен в тело `F` вместо `A`.

Обобщённые рекурсивные типы

Особого внимания заслуживает возможность объявлять типы рекурсивно, когда в теле выражения используется идентификатор объявляемого типа.

В Scala рекурсивные типы зачастую описываются в ООП-стиле, например,

sealed trait List[A]
case object Nil                                  extends List[Nothing] // почему Nothing - будет рассказано далее
final case class Cons[A](head: A, tail: List[A]) extends List[A]

val myList: List[Int] = Cons(1, Cons(2, Cons(3, Cons(2, Cons(1, Nil))))) // 1, 2, 3, 2, 1

Рекурсивность List с первого взгляда, возможно, незаметна. Она спрятана за наследованием классов (extends). Соответствующие объявленным классам типы можно записать так:

$\begin{align} List[A] &= Nil + Cons[A],\\Cons[A] &= A \times List[A],\\Nil &\cong 1.\\\end{align}$

Если подставить два последних выражения в первое, то получается равенство, в котором рекурсия видна явно:

$List[A] \cong 1 + A \times List[A].$

(Если вместо подставить тип $Nothing \cong 0$ , то можно убедиться, что $List[Nothing] \cong 1 \cong Nil$ .)
Таким образом, список – это либо пустой список, либо элемент (голова) и другой список (хвост).

Просуммируем такой список:

def sum(list: List[Int]): Int = list match
  case Nil              => 0
  case Cons(head, tail) => head + sum(tail) // тут рекурсия!

Прослеживается очевидная закономерность – для рекурсивных типов нужны рекурсивные методы!

Пользуясь только суммой и произведением типов с помощью рекурсии можно построить любые древовидные структуры, например,

sealed trait NonEmptyTree[A]
final case class Leaf[A](value: A) extends NonEmptyTree[A]
final case class Node[A](left: NonEmptyTree[A], right: NonEmptyTree[A]) extends NonEmptyTree[A]

Трейту NonEmptyTree соответствует такой тип:

$NonEmptyTree[A] \cong A + NonEmptyTree[A] \times NonEmptyTree[A].$

Объявить рекурсивный тип в актуальной версии Scala без привлечения ООП несколько затруднительно. Например, такая конструкция не скомпилируется:

type List[A] = Unit + (A, List[A]) // illegal cyclic type reference...

Компилятор ~~пытается~~ даже не пытается развернуть выражение типа, спрятанного за псевдонимом, а, определив бесконечную рекурсию, сразу сообщает об ошибке. Выглядит как недоработка компилятора, так как есть обходной путь с использованием механизма сопоставления с шаблонами на уровне типов – там типы вычисляются "лениво" и подобная рекурсия считается вполне легальной.

Такие обобщённые древовидные типы иногда называются абстрактными типами данных (неизменяемыми). Они описывают коллекции определённой структуры, которые могут "хранить" элементы любого типа. В частности, обычный список является вырожденной разновидностью дерева.

Нетривиальность концепции рекурсивных типов можно ощутить, если для их построения задействовать экспоненциал типов (типы функций). Например, давайте посмотрим на два таких симметричных типа:

case class SelfModifyingHandler[A](f: A      => SelfModifyingHandler[A])
case class Wtf[A]                 (f: Wtf[A] => A)

Попробуйте самостоятельно создать значения этих типов и придумать сценарии их использования (названия толсто намекают...). Результатами предлагаю поделиться в комментариях.

Тема рекурсивных типов и рекурсии в целом настолько богата, что хотелось бы раскрыть её в отдельной статье. В ней хотелось бы рассказать о таких вкусностях, как

ограничения на рекурсию ("что не так с Wtf");
хвостовая рекурсия, трамплины;
ряд Тейлора и корни многочленов для обобщённых рекурсивных типов ;
производные от обобщённых рекурсивных типов;
комбинаторы неподвижной точки;
схемы рекурсии (ката-, ана- и прочие морфизмы). Очень надеюсь, что найдётся возможность подготовить и такой обзор.

Полиморфные типы

Разновидности полиморфизма

В интернете можно встретить различные определения полиморфизма, но вряд ли какое-либо из них можно считать “общепринятым”. Например, определение полиморфизма в Википедии немного отличается от аналогичного в Wikipedia. Там указаны разные источники, но в качестве первоисточника приводится одна статья 1967 года “Fundamental Concepts in Programming Languages” Кристофера Стрейчи, переизданная в 2000м. Однако, и там нет определения полиморфизма как такового. Пожалуй, в наиболее общем виде это понятие можно сформулировать так:

Полиморфизм в программировании – это свойство фрагмента кода определять разное поведение в зависимости от типов термов, использованных в нём.
Такой код ссылается на набор различных алгоритмов, “форм”, ассоциированных с конкретными типами, то есть, является полиморфным по типу (слово “πολυμορφή“ можно перевести с греческого как “множество форм”).

В той статье Стрейчи говорится о двух основных разновидностях полиморфизма – универсальном (параметрическом) и специальном (ad-hoc). Разные исследовали приводят множество разновидностей полиморфизма и, если собрать их все вместе, то наберётся не меньше дюжины. Но, так или иначе, любой такой подвид можно притянуть за уши либо к универсальному, либо к специальному (или же к их сочетаниям). В этой статье, помимо прочих, будут рассмотрены такие разновидности, как полиморфизм видов и полиморфизм вселенных – они являются обобщениями приведённого определения, в которых расширено понятие “тип”.

Отдельно стоит сказать про полиморфизм в языках с динамической типизацией. Как правило, в таких языках явно типизированными остаются лишь некоторые функции, например, встроенные арифметические операции, но типы любых значений проверяются только в момент попытки их использования в типизированных функциях. Вне контекста выполнения типы термов просто не определены, что не позволяет проводить проверку корректности программы до её выполнения. Но теория типов используются в программировании прежде всего для обеспечения корректности алгоритма в целом, для любых начальных условий. Не смотря на то, что при динамической типизации код является фактически полиморфным (описывает работу со значениями разных типов), далее динамический полиморфизм не будет рассматриваться в этой статье.

Классификация Стрейчи канонична, но при нынешнем засилье объектно-ориентированной парадигмы у многих программистов уже могло сложиться представление о полиморфизме, как лишь об одном из "столпов ООП". Например, перейдя по одной из первых ссылок в результатах интернет-поиска по слову "полиморфизм", можно прочесть:

Полиморфизм (polymorphism) — это понятие из объектно-ориентированного программирования, которое позволяет разным сущностям выполнять одни и те же действия. При этом неважно, как эти сущности устроены внутри и чем они различаются.

Не уверен, что имеет смысл упрекать авторов подобных цитат в том, что они вводят в заблуждение читателя. Популярность какого-либо мнения превалирует в массовом сознании над его качеством, корректностью. ООП-шный полиморфизм рассмотрим подробнее чуть позднее, а сейчас предлагаю сосредоточиться на наиболее востребованном универсальном полиморфизме.

Универсальный полиморфизм и λ-исчисление

Само понятие универсального (параметрического) полиморфизма появилось в процессе развития $\lambda$ -исчисления. Эта формальная система создавалось как фундаментальный язык, алгоритмы на котором можно было бы проверить на логическую корректность.

Изначально $\lambda$ -исчисление было безтипововым. Там было введено понятие $\lambda$ -абстракции с правилом аппликации (применения):

$\begin{align}f&:=\lambda x.\;2\cdot x+1;\\f\;5\equiv f(5)&=2\cdot 5+1=11.\end{align}$

Затем появилось просто-типизированная система $\lambda^{\rightarrow}$ . Здесь у каждой переменной, которая связывается квантором $\lambda$ фиксируется метка-тип (явно – в стиле Чёрча):

$\begin{align}\lambda x:A.M;\\\end{align}$

Тип самого $\lambda$ -выражения однозначно (по возможности) определяется по типу аргумента и телу выражения .

Обозначение $\lambda^{\rightarrow}$ (стрелочка) связано с тем, что простые типы можно выразить как функции высшего порядка в кодировке Чёрча, т.е. :

type Zero     = Any        // ? ≅ Any
type One      = Any => Any // ? ≅ Any => Any
type Bool     = Any => One // ? ≅ Any => Any => Any
type Natural  = One => One // ℕ ≅ (Any => Any) => Any => Any - натуральные числа по Пеано

Например:

val trueWay: Bool = happyWay => unhappyWay => happyWay
val one  : Natural = suc => z =>         suc(z)
val three: Natural = suc => z => suc(suc(suc(z)))

// вычисления
def calc(cond: Bool, trueNum: Natural, falseNum: Natural) =
  cond(trueNum)(falseNum).asInstanceOf[Natural]
val result = calc(trueWay, three, one)

// натуральное число к Int32
def natToInt(num: Natural): Int =
  num(_.asInstanceOf[Int] + 1)(0).asInstanceOf[Int]  
natToInt(result) // 3

Дальнейшее развитие – полиморфная система $\lambda2$ (система F). Теперь в $\lambda$ -выражении стало возможно связывать не только обычные переменные, но и типовые:

$\begin{align}\lambda A:\star.\; \lambda x:A.\; M\end{align}$

Здесь $\star$ – это "тип типа". Система $\lambda2$ позволяет определять обобщённые функции. В изоморфизме Карри-Ховарда типы соответствуют утверждениям, свойствам объектов, следовательно, система $\lambda2$ ассоциируется с логикой второго порядка (отсюда и двойка в названии).

В Scala 3 добавлен специальный синтаксис для типов обобщённых функций:

// обычный метод
def foldWithContext[A, B](aWithContext: WithContext[A])(folder: (A, String) => B)
  = folder(aWithContext._1, aWithContext._2)

// переменная обобщённого функционального типа
val foldWithContextVal
  : [A, B] => WithContext[A] => ((A, String) => B) => B // тип      ∀A,B. WithContext[A] → ((A, String) → B) → B
  = foldWithContext                                     // значение λA,B. λa:WithContext[A]. λf:(A,String) → B. f(a._1, a._2)

Значения такого типа можно передавать в методы, в которых будет решаться, какие типы подставить для этих обобщённых функций.

Наконец ещё более продвинутая система $\lambda\omega$ (или $F\omega$ ) позволяет уже строить типы, используя $\lambda$ -выражения

$List = \lambda A.\; \forall B.\; (A\rightarrow B\rightarrow B)\rightarrow B\rightarrow B;\\$

Именно тут появляются полноценные полиморфные (обобщённые) типы:

type List = [A] =>> [B] => (A => B => B) => B => B

def emptyList[A]: List[A] =
  [B] => (aggr: A => B => B) => (start: B) => start

def append[A](lst: List[A], a: A): List[A] =
  [B] => (aggr: A => B => B) => (start: B) => aggr(a)(lst(aggr)(start))

def fold[A, B](lst: List[A], start: B, aggr: A => B => B): B = lst(aggr)(start)

val myList = append(append(append(emptyList[Int], 1), 2), 3) // [1, 2, 3] 
fold(myList, "список:", i => _ + " " + i)                    // "список: 1 2 3"

Сами выражения, на которых строятся полиморфные типы, определяют способы их использования – связанные с ними полиморфные функции. Компилятор сам может (его можно научить) строить такие функции для полиморфных типов, что может значительно сократить количество кода, которого приходится писать программистам вручную.

Ввиду того, что в таких полиморфных типах параметр связывается через квантор "для любого", параметрический полиморфизм называется универсальным. Полиморфизм, где используется дуальный квантор "существует", называется специальным – он будет рассмотрен позже.

Полиморфизм подтипов

Рассмотрим теперь полиморфизм подтипов на конкретном примере:

trait Person { val name: String def sayHello(): String }
case class Français(name: String) extends Person { def sayHello() = "Bon après-midi!" }
case class Русский (name: String) extends Person { def sayHello() = "Здаров!" }

def dialogWith(person: Person) =
  println("Привет, " + person.name)
  println(person.sayHello())              // 1

val Француа = Français("François")
val Василий = Русский("Вася")
dialogWith(Француа); dialogWith(Василий)  // 2

Возможно, у кого-то возникнет впечатление, что полиморфизм тут проявляется в строке с пометкой 1, ведь именно там конкретное поведение метода sayHello определяется "типом значения", спрятанного за переменной person. Но проблема в том, что, по определению, типы привязываются к термам языка (литералам, переменным, выражениям), а не к значениям, размещённым в памяти компьютера.

Да, у значения, зачастую, есть ссылка на описание класса, конструктором которого это значение создано, и класс связан с конкретным типом, который используется во время выполнения при проверке возможности использования значения в тех или иных операциях. Но, как уже было сказано, основанный на этой идее динамический полиморфизм не помогает в проверке корректности алгоритма, и мы не будем его рассматривать.

В данном же примере у переменной (терма) person тип Person фиксирован в сигнатуре метода, в строчке 1 идёт однозначное обращение к методу sayHello трейта Person, следовательно, тут полиморфизма нет. То, что “под капотом” будет переадресация на метод из таблицы виртуальных методов, связанной со значением, нас не должно волновать, так как мы сейчас на более высоком уровне языка программирования рассматриваем статическую типизацию.

Но полиморфизм есть в строке с пометкой 2 – при вызовах метода, принимающих параметр типа Person, используются переменные других типов, Français и Русский. В этой строке срабатывает неявное приведение от подтипов к супертипу – именно это и определяет ООП-шный полиморфизм подтипов! Например, если бы с помощью dialogWith обрабатывалась коллекция значений типа Person, то полиморфным было бы добавление значений классов Français и Русский в эту коллекцию.

Вызов по имени метода, перегруженного в неизвестном подклассе, который определяется по значению person не является какой-то "ООП-шной магией", ведь методы суть значения функционального типа – по ссылке person можно добраться до размещённой в памяти таблицы виртуальных методов, а уже в этой таблице лежат ссылки на методы именно того подкласса, конструктором которого это значение было создано. Ссылки на методы можно вытащить явно, и в предыдущем примере достаточно просто переписать эти три строчки (и выкинуть классы-наследники)

case class Person(val name: String, val sayHello: Unit => String)
val Француа = Person(       "François",           ()   => "Bon après-midi!")
val Василий = Person(       "Вася",               ()   => "Здаров!")

и получить тот же самый результат, но уже без привлечения полиморфизма.

Следуя Википедии, полиморфизм подтипов относится к разновидности универсального полиморфизма с ограничениями подтипизации - об этом будет далее. Но с другой стороны, сами эти ограничения можно реализовать с помощью специального полиморфизма, о котором будет рассказано далее в одноимённом разделе.

Вариантность

Является ли список строк списком произвольных объектов? Конкретнее, можно ли передать терм типа List[String] в функцию, которая принимает аргумент типа List[Any]? Опытным путём можно убедиться, что в Scala (да и во многих других языках) это можно сделать. Но вот, наоборот, передавать терм типа List[Any] в функцию, принимающую List[String], запрещено. Получается, что List[String] является подтипом List[Any] и, очевидно, безо всякого наследования! Попробовав с другими простыми типами, можно заметить, что конструктор типов List транслирует отношения подтипизации для своих аргументов.

Но для других типов наблюдается иная картина:

type Func[X] = X => Int // псевдоним для конструтора типов Function1

// если этот "призыв" компилируется, значит такая подтипизация корректна
summon[     String  <:<      Any]
summon[List[String] <:< List[Any]]
summon[Func[Any]    <:< Func[String]] // поменялись местами String и Any!

Получается, что конструктор типов [X] =>> X => Int обращает подтипизацию в обратную сторону! Причём, у похожего типа[X] =>> Int => X подтипизация вновь окажется “прямой”!

А вот если мы наивно попробуем то же самое со своим классом, у нас ничего не получится:

class Test[A](val a: A)

summon[Test[String] <:< Test[Any]]    // ошибка!
summon[Test[Any]    <:< Test[String]] // ошибка!

Чтобы разобраться в чём причина, достаточно ~~просто прочесть документацию~~ посмотреть на определение типов List и Function (=>) в стандартной библиотеке:

type List    [+A]     = scala.collection.immutable.List[A]
type Function[-A, +B] = Function1[A, B]

Именно значки перед параметрами конструкторов типов определяют вид вариантности:

+ означает прямую ковариантную трансляцию подтипизации,
- – инвертированную, контравариантную,
нет значка – подтипизация блокируется – инвариантность. (Псевдонимы типов по-умолчанию пробрасывают вариантность своих выражений без изменений.)

В представленном выше классе Test параметр A используется двояко – и как тип аргумента конструктора (контравариантно), и как тип проектора поля a (ковариантно). Следовательно, полиморфный тип, связанный с этим классом, является инвариантным. Попытки поставить в квадратных скобках перед A плюс или минус приведут к ошибке компиляции вида contravariant type A occurs in covariant position in type A of value a ("контравариантный тип A появляется в ковариантной позиции типа переменной a"). О какой же позиции тут идёт речь?

На первый взгляд может показаться, что имеется ввиду позиция "относительно стрелки" =>:

отрицательная позиция (знак -), если слева от стрелки и
положительная позиция (знак +), если справа. Но не всё так просто?. Например, вот этот тип внезапно оказывается ковариантным:

type Cont[+X] = (X => Int) => Int
summon[Cont[String] <:< Cont[Any]]

Параметр X стоит левее сразу двух стрелок – дважды отрицательная позиция превращается в положительную!

Обобщённые списки ковариантны, и это объясняет, почему тип пустого списка Nil ≅ List[Nothing]. Универсальным свойством нулевого типа Nothing (см. предыдущую статью) является наличие неявного преобразования от Nothing к любому другому типу, поэтому, вследствие ковариантности, пустой список типа Nil можно использовать везде, где требуется List[A] при любом A.

Как уже не раз упоминалось, отношение подтипизации – это просто функция от одного типа к другому (неявное преобразование). Тогда, вариантность – это то, как подобные функции преобразуются "под действием" конструкторов типов. Чуть подробнее такие возможности обобщённых типов будут раскрыты в этой статье позднее.

Тип вариантности полиморфного типа F[_] проявляется в том, как отношения подтипизации (функции неявных преобразований) между A и B переносятся на типы F[A] и F[B]. Синими стрелками обозначены ключевые черты функтора: ковариантного или контравариантного, в зависимости от направления красной стрелки. — Тип вариантности полиморфного типа `F[_]` проявляется в том, как отношения подтипизации (функции неявных преобразований) между `A` и `B` переносятся на типы `F[A]` и `F[B]`. Синими стрелками обозначены ключевые черты функтора: ковариантного или контравариантного, в зависимости от направления красной стрелки.

В дополнение можно рекомендовать эту статью: Demystifying Variance in Scala.

Ограничения подтипизации

Привычный ООП-шный полиморфизм подтипов подразумевает, что в любую функцию мы можем передавать значения любых типов, являющихся подтипами к типу соответствующего параметра функции.

trait SupperClass { val i: Int }
case class SubClass(i: Int) extends SupperClass

def someFunc(x: SupperClass) =
  x.i + 3

val sub = SubClass(5)
someFunc(sub) // полиморфизм тут

Это эквивалентно ситуации, как если бы функция явно декларировала, что может принимать значения разных типов (т.е. имеет тип-параметр, превращающий её в обобщённую), но для которых задано определённое ограничение подтипизации.

Такая система типов $F_{<:}$ , в которой универсальный полиморфизм сочетается с ограничениями подтипизации, реализуется во многих популярных языках, в том числе и в Scala. Например, во фрагменте кода выше достаточно изменить сигнатуру метода someFunc, чтобы продемонстрировать полиморфизм явно:

def someFunc[A <: SupperClass](x: A) =
  x.i + 3 // тело функции не меняется

Таким образом, система $F_{<:}$ позволяет относить полиморфизм подтипов к разновидности универсального полиморфизма, дополненного ограничениями подтипизации.

Ограничения подтипизации для параметров обобщённых методов мощнее, чем полиморфизм подтипов. Следующий фрагмент кода показывает, что полиморфизм с ограничением подтипизации позволяет без потерь передать тип аргумента на выход функции:

trait SupperClass { val i: Int }
case class SubClass(i: Int, s: String) extends SupperClass // в подклассе новое поле s
val sub: SubClass = SubClass(5, "string")

def extractInt1[A <: SupperClass](x: A): (A,           Int) = (x, x.i)
def extractInt2(x  : SupperClass      ): (SupperClass, Int) = (x, x.i)

// с помощью "_1" обращаемся к первому элементу кортежа 
extractInt1(sub)._1.s // "string"
extractInt2(sub)._1.s // !!! ОШИБКА !!! Компилятор не видит тут никакого s!

В последней строке будет ошибка компиляции, так как функция extractInt2 ничего не знает об исходном типе переданного ей аргумента – неявное преобразование подтипизации сработало до того, как значение было передано в функцию.

Выше были представлены такие ограничения, когда тип-параметр должен быть чьим-то подтипом – так называемые, верхние границы типа. Но существует также понятие нижней границы типа: запись X >: SubType означает, что тип-параметр X должен быть супертипом для некого фиксированного типа SubType. Наглядный пример использования такого ограничения можно подсмотреть в официальной документации Scala.

В ранних версиях Scala была возможность использовать, так называемые, ограничения представления. Запись A <% SomeType означала, что известно некое неявное преобразование от типа A к типу SomeType, то есть, возможности типа SomeType применимы к значениям типа A. Такое преобразование вовсе не обязательно завязывалось на наследовании классов, вариантности обобщённых типов (List[String] <: List[Any]) или встроенной подтипизации (Short <: Int) – могут быть использованы в том числе и пользовательские неявные преобразования:

given def intToSubClass(i: Int) // объявляем неявное преобразование Int => SubClass
  = SubClass(i, "нечто") 
def getString[A <% SubClass](a: A) = a.s

getString(5) // "нечто"

В Scala 3 такой синтаксис убрали, но эффектов, аналогичных использованию ограничений <% можно достичь с помощью классов типов – о них будет рассказано далее.

Отношения подтипизации можно ввести не только для простых типов, но и для полиморфных. Сделать это можно разными способами, но, пожалуй, самый очевидный из них - это поточечная подтипизация: считаем F подтипом G, если F[X] является подтипом G[X] для любого типа X. При подготовке статьи очень удивился, обнаружив, что такая подтипизация уже присутствует в Scala:

def headOption[F <: [X] =>> Iterable[X], A](fa: F[A]): Option[A] = fa.headOption
  
headOption(List(5))          // Some(5)
headOption(Option("строка")) // Some("строка")
headOption(Map(1.2 -> true)) // Some((1.2, true))

К сожалению, в актуальной на данный момент версии Scala в ограничении приходится явно указывать $\lambda$ -выражение для типов, что выглядит коряво. К слову, аналогично эффекта можно добиться, написав F[_] <: List[_].

Очевидно, поточечную подтипизацию по индукции можно распространить и на полиморфные типы более высокого рода которые будут рассмотрены далее.

Существует одна разновидность полиморфизма подтипов под названием “F-ограниченный полиморфизм“, когда подтипизация завязывается рекурсивно на определяемый тип. Рассмотрим такой пример:

trait F[U <: F[U]]
class C extends F[C]

Здесь трейт F принимает параметр U, ограниченный сверху F[U] – это и есть то самое рекурсивное “F-ограничение”. Конкретный класс C расширяется обобщёнными возможностями, представленными в трейте F[C], то есть, задействующими всё тот же тип C. Собственно для этих целей и используется F-ограничения. Подробнее о них можно прочесть в статье Брюка Кайсена F-bounded polymorphism in Scala. Сценарии, в которых обычно применяются F-ограничения, также могут быть реализованы посредством специального полиморфизма.

Типы высокого рода

Higher Kinded Types

В математике существуют такие понятия, как

функционал, превращающий функции в "простые" нефункциональные значения (например, интегральная свёртка),
оператор, превращающий одни функции в другие (например, дифференцирование). В отличие от обычных функций, такие отображения связывают не только простые множества, вроде действительных чисел, но и множества функций!

Отображения, из функций и/или в функции в информатике называются функциями высших порядков (higher-order functions). Такие функции могут оперировать не только "простыми" функциями (первого порядка), но и такими же функциями высших порядков. При этом, "порядок" новой функции будет выше чем, у тех, которые она принимает/возвращает.

Ремарка о функциях-значениях

Функция, как набор инструкций, размещённых в памяти, представляет собой обычное значение, и даже в Ассемблере можно передавать указатель на функцию в другую функцию, вызывать её по указателю, или возвращать его. Но сам термин "функции высших порядков" вошёл в оборот, кода в популярных высокоуровневых языках появилась возможность использовать функции как значения – "функции первого класса".

В свою очередь, конструкторы типов, как уже было замечено, представляют собой функции на уровне типов – отображают одни типы в другие. Имеющиеся в системе "простые" конструкторы типов (переводящие один простой тип в другой) в системе $F_\omega$ расширяются функциями высших порядков на типах – higher kinded types (HKT).

Слово "kind" вызывает известные трудности перевода. Встречаются такие варианты:

кайнд – незамысловатая транслитерация, заимствование из английского, которое не всегда считается оправданным;
сорт в русском языке привычно индексируется натуральными числами, что порождает эклектику вроде "типов третьего сорта";
вид типа кажется хорошим вариантом перевода, если избегать словосочетания "типы высокого вида";
род привносит в предметную область не очень уместную, но ставшую уже привычной, "высокородность". Далее будут рассмотрены виды типов высокого рода ?.

Рассмотрим примеры:

type Option = [A] =>> Unit | A
type Reader = [Dep] =>> [A] =>> Dep => A
type Functor = [F[_]] =>> [A, B] => (A => B) => (F[A] => F[B])
type TaglessFinalProgram = [Algebra[_[_]]] =>> [A] =>> [F[_]] => Algebra[F] => F[A]

Конструктор Reader принимает на вход тип зависимости и возвращает другой конструктор, принимающей тип результата и возвращающий тип функции. По сути, Reader является каррированной версией конструктора типов, принимающего два параметра. В свою очередь Functor принимает на вход уже конструктор типов, и возвращает простой тип полиморфной функции.

Не каждый тип может быть подставлен в эти конструкторы типов:

type FOpt = Functor[Option]
//type FReader1 = Functor[Reader]       // нельзя!
type FReader2 = Functor[Reader[Int]]
//type FInt = Functor[Int]              // нельзя!
type OptInt = Option[Int]
//type OptReader1 = Option[Reader]      // нельзя!
//type OptReader2 = Option[Reader[Int]] // нельзя!
type OptReader3 = Option[Reader[Int][String]]
type OptF = Option[Functor[Option]]
//type Reader1 = Reader[Int]            // нельзя!
type Reader2 = Reader[Int][String]

Полиморфные типы добавляют красок в однообразие простых типов – теперь типы не все одинаковые)). Но это приносит не только радость. Ведь даже для простых конструкторов типов вроде Option возникает вопрос: можно ли считать типы высокого рода, собственно, типами, если их нельзя приписать к значениям, как метки? Какой смысл может иметь запись val opt: Option?

Можно, конечно, пофантазировать, сказав, что подставив в значение opt конкретный тип, мы сможем получить новый тип, например val intOpt: getType[Int](opt) = Some(42). Конечно, всё зависит от языка, и, хотя конкретно так Scala не умеет, но с помощью определённых костылей (основанных на полиморфных функциях и зависимых типах) можно добиться схожего результата, но…

Действительно, для типов высокого рода не предусмотрено использование в качестве меток термов, так что на самом деле полиморфные типы не являются типами! (См. также тут.) Конструкторы типов называют типами скорее по аналогии с функциями высших порядков, которые все являются значениями (функции первого класса). В Scala есть синтаксис, использование которого позволяет трактовать конструкторы типов как метки, но уже не для значений, а для других типов - это будет рассмотрено при обсуждении классов типов.

Другие примеры использования типов высокого рода можно подсмотреть, например, тут:

Higher-kinded data in Scala,
GitHub-проект DataPrizm (и статья об использовании типов высокого рода, в этом проекте).

Логика высших порядков

С точки зрения изоморфизма Карри-Ховарда полиморфные типы высокого рода связаны с логикой высших порядков. Например, тип

type Product = [A, B] =>> (A, B)

можно прочесть как
"Для любых типов A и B из их обитаемости следует обитаемость типа-произведения A × B."

Изоморфное этому типу утверждение в логике второго порядка будет выглядеть так:
"Для любых высказываний A и B из их истинности следует истинность высказывания A ∧ B."

Именно наличие квантора ("для любого", или "существует") над типами/высказываниями определяет с одной стороны изоморфизма "высокородность" типа, а с другой - высший порядок логики. Связь более сложных полиморфных типов с логиками высших порядков выводится по индукции.

Предоставление реализации некоторого метода является доказательством обитаемости соответствующего функционального типа. Если компилятор не ругается на такую реализацию, то тип результата метода удалось логически корректно связать с типом его аргумента. С полиморфными типами (функциональными отображениями из типов в тип) ситуация совершенно аналогичная. Полиморфные типы представляют собой инструмент мощной выразительной силы, но при этом сохраняют ключевую особенность простых типов - благодаря изоморфизму Карри-Ховарда, компилятор по-прежнему может проверить логичность алгоритма до его исполнения. (Да, рекурсивные типы, упомянутые ранее, могут усложнить проверку корректности, а то и вовсе сделать её невозможной, но это отдельная история.)

Вид типа

Приведённые выше примеры демонстрируют, что типы высокого рода могут относится к разным видам типа (type kinds). В определениях этих типов однозначно указывается, параметры какого вида типов они принимают: A, F[_], Algebra[_[_]]. Такие параметры должны быть либо простыми типами, либо другими конструкторами типов - отображениями из типов в простые типы.

Для видов типов разработана своя система обозначений. Вид простых типов обозначается звёздочкой $\star$ . Вид конструкторов типов, принимающих на вход простые типы, записывается как $\star\rightarrow\star$ . Все остальные виды типов строятся по индукции. В языках семейства ML (том же Haskell) функции сразу записываются в каррированном виде, это же правило относится и к конструкторам типов. В Scala использован более традиционный синтаксис, когда функция может принимать несколько параметров, разделённых запятыми – также реализуются и конструкторы типов. В итоге получаем следующую формализацию:

Вид типа - это либо вид простых типов ( $\star$ ), либо отображение ( $\rightarrow$ ) из одного вида типа (или нескольких через запятую) в другой вид типа.

Стрелка, как оператор, обычно подразумевает правую ассоциативность, поэтому вид $\star\rightarrow(\star\rightarrow\star)$ эквивалентен виду $\star\rightarrow\star\rightarrow\star$ . Таким образом, в конце каждого вида типа после стрелочки будет вид простого типа $\star$ . Можно говорить, что любой вид типа описывает конструкторы простых, “истинных” типов.

В этой таблице демонстрируется соответствие видов типа и параметров конструкторов типа:

Вид типа	Параметр конструкторов типа этого вида	Пример типа этого вида
$\star$	`A`	`Int`
$\star\rightarrow\star$	`F[_]`	`Option`
$\star\rightarrow\star\rightarrow\star$	`F[_][_]`, но Scala плохо понимает типы каррированного вида((	`Reader` из примера выше
$(\star\rightarrow\star)\rightarrow\star$	`Alg[_[_]]`	`Functor`
$((\star\rightarrow\star)\rightarrow\star)\rightarrow\star$	`Prog[_[_[_]]]`	`TaglessFinalProgram` из примера выше
$(\star,\star)\rightarrow\star$	`M[_, _]`	`Map`

Ещё раз стоит обратить внимание на вид типа Functor из примера выше. В Scala конструкции вроде [A, B] => ... обозначают простой тип полиморфной функции, поэтому в итоге для Functor и получается вид $(\star\rightarrow\star)\rightarrow\star$ .

В Scala REPL (интерпретатор командной строки) есть возможность подсмотреть вид типа, воспользовавшись командой :kind (с опциональным параметром -v). Например, для типа Functor из библиотеки Cats вывод команды будет такой:

scala> :kind -v cats.Functor
cats.Functor's kind is X[F[A]]
(* -> *) -> *
This is a type constructor that takes type constructor(s): a higher-kinded type.

К сожалению, команда :kind работает только с определёнными ранее обобщёнными классами (трейтами). Псевдонимы типов или λ-выражения эта команда не воспринимает.

При подготовке статьи была идея реализовать что-то вроде типа вида типа ?:

type Kind
type GetKind[A <: AnyKind] // <: Kind   // (про AnyKind будет дальше)
def instantinate[K <: Kind]: Kind = ??? // конструтор значения типа вида типа
def toString(kind: Kind): String = ???  // строка вида "(⋆ → ⋆) → ⋆"

Сам тип Kind можно было бы определить как-то так:

opaque type ⋆ = Unit                    // вид простых типов
type -->[K1, K2] = (K1, K2)             // просто некая стрелка
type Kind = ⋆ | (Kind --> Kind)         // тип вида типа (без множественных параметров)

Но, такой код, к сожалению, не компилируется из-за упомянутого ранее ограничения на рекурсию типов. Есть различные обходные манёвры для этого препятствия, но, так или иначе, все они завели в тупик. Чего-то похожего можно добиться, предоставив неявные экземпляры некоторого класса типов, но такой метод работает только для конечного числа видов типа. Если у кого-то из читателей получилось победить компилятор Scala и реализовать эту задумку для всех видов типов, пожалуйста, поделитесь рецептом в комментариях.

Вычисления на уровне типов

Итак, у нас есть возможность строить алгебраические выражения из типов, а также строить функции из типов в тип. И этих возможностей достаточно, чтобы заняться программированием на уровне типов!

Рассмотрим такие определения типов:

type ⊥        = Unit      // тип "нулевого вида"
type ⊤        = [A] =>> A // тип "единичного вида"

type IfFalse  = [False] =>> [True] =>> False
type IfTrue   = [False] =>> [True] =>> True

type Zero     = [Z] =>> [Succ[_]] =>> Z
type One      = [Z] =>> [Succ[_]] =>> Succ[Z]
type Two      = [Z] =>> [Succ[_]] =>> Succ[Succ[Z]]
type Three    = [Z] =>> [Succ[_]] =>> Succ[Succ[Succ[Z]]]

Использование представленных типов сопряжено с трудностями, связанными с отсутствием в Scala должной поддержки каррированных типов-параметров, но всё же возможно. Принадлежность представленных выше типов одному "типу" определяется видом этих типов:

$\begin{split}Zero &:&&\;\; \star\\One &:&&\;\; \star\rightarrow\star\\Bool &:&&\;\; \star\rightarrow\star\rightarrow\star\hspace{2cm} (\text{тут и ниже подразумевается каррирование})\\Natural &:&&\;\; (\star\rightarrow\star)\rightarrow\star\rightarrow\star\\Pair &:&&\;\; (\star\rightarrow\star\rightarrow\star)\rightarrow\star\\\end{split}$

Не сложно заметить, что представленные тут виды типов коррелируют с типами в кодировке Чёрча, представленными ранее, при выведении типов в изначально бестиповой системе. И это логично, так как вид типа является, по сути, типом типа (а $\star$ – это изначально “безтиповый” вид)!

Трактовка таких конструкторов типов достаточно очевидна. Например, типы натуральных чисел соответствуют итерациям применения некого конструктора типов Succ к типу Z. Но также эти типы можно интерпретировать, как фантомные, не предусматривающие использование в качестве меток термов, но которые можно передавать в другие конструкторы типов. С помощью таких фантомных типов можно, например, построить тип списка фиксированной на этапе компиляции длины – при конкатенации длина нового списка будет также рассчитываться на этапе компиляции. И, в принципе, алгоритмы на уровне типов используются именно для каких-либо вычислений на этапе компиляции. Эта идея хорошо раскрывается в habr-статье Решение задачи о 8 ферзях на трёх уровнях Scala — программа, типы, метапрограмма.

Плюсом программирования на типах является его чистота с точки зрения функционального программирования. Нет никаких эффектов – вообще никакого “нечистого” взаимодействия с окружением. Но это же является и минусом, ведь каждый такой алгоритм может решить лишь единственную задачу, условия которой известны до компиляции. Во многих программах есть как минимум одна такая сверхзадача – построение корректной композиции функций, благодаря которой в процессе работы приложения обычные значения будут передаваться между объектами окружения (клавиатура, монитор, память, БД, web-службы и т.п.) согласно техническому заданию. Так вот с такой сверхзадачей программирование на типах справляется вполне успешно.

Другие примеры программирования на типах можно найти тут:

Typelevel Church Numerals in Scala 3 – там также определены типы сложения и умножения для таких "натуральных чисел".
habr-статья Scala: структура данных в пространстве типов — множество;
Type-Level Programming in Scala из журнала Apocalisp;
цикл статей Type-Level Programming in Scala с ресурса Rock the JVM Blog (Part I, Part II, Part III)
цикл статей Meta-Programming with Scala: (Part I, Part II, Part III);
презентация Type-Level Computations in Scala;
pdf-статья Луки Карделли Typeful Programming;
реализации SKI на уровне типов:
- статья Scala type level encoding of the SKI calculus из весьма познавательного блога Мичида;
- GitHub-проект Type level lambda calculus in Scala.

Полиморфизм видов

Есть ли какие-нибудь операции, которые можно было бы сформулировать единообразно для полиморфных типов разного вида? Конечно, есть – это и отношения конструкторов типов (в частности, эквивалентность), и банальный проброс типа произвольного вида (аналог функции identity на значениях), какие-либо модификации вида типа (например, усложнение). Вариантов множество.

Такого рода операции над конструкторами типов должны быть полиморфными по виду Полиморфизм видов (kind polimorphism) также называют полиморфизм высокого рода (higher kinded polymorpism), подразумевая, что в этом случае универсальная квантификация идёт по типам типов. Язык Haskell позволяет работать с видами типов также как и с обычными типами, соответственно, для них также реализован и полиморфизм видов. В Scala 3 же для этих целей предусмотрен специальный синтаксис, похожий на ограничение подтипизации для параметров обобщённых типов: <: AnyKind:

type SomeTypeConstructor[A <: AnyKind]

Из за такой записи может показаться, что AnyKind является ещё одним типом, но это не так. На самом деле это просто метка для компилятора, допускающая вольную трактовку вида типа-параметра.

Практическое применение полиморфизма видов в Scala ограничено реализацией поддержки AnyKind. На упомянутой ранее странице официальной документации Scala до сих пор есть строка:

(todo: insert good concise example)

В интернете же можно найти такие примеры использования AnyKind:

внутри Scala, например, при работе с макросами;
проверка концепции полиморфизма видов, по уже упоминавшейся ранее ссылке;
две любопытных реализации моноида, полиморфного по видам типа: gist s5bug, gist mandubian;
ещё один пример определения монады, через моноид, полиморфный по видам;
Implement SKI combinator calculus с использованием AnyKind;
Вопрос на StackOverflow Scala 3. Kind polymorphism and AnyKind type - any code example?
Слайды презентации Adding kind-polymorphism to the Scala programming language
Обсуждение предложения по доработке Proposal to add kind polymorphism to the language

Если у читателей есть хорошие примеры, пожалуйста, приведите их в комментариях.

Вселенные типов

Итак, виды типов – это типы типов высокого рода. Но “типы типов” не могут сами быть типами – это привело бы к так называемому парадоксу Жирара.

Парадокс Жирара

Парадокс Жирара в теории типов – это аналог парадокса Рассела, демонстрирующего, что совокупность всех множеств сама не может быть множеством. В интернете сложно найти более-менее популярную литературу по парадоксу Жирара, разве что pdf-статья Хёркенса A Simplification of Girard’s Paradox.

Наличие логических парадоксов может скомпрометировать всю теорию типов, делая её ненадёжной. Во избежание этого вводится концепция вселенных типов: простые типы и типы высокого рода относятся к “обычной” вселенной типов , в то время как все виды типов принадлежат уже к другой вселенной . В Haskell реализована работа с типами из обеих вселенных и считается, что этого достаточно для задач языка.

Тем не менее, аналогию между видами типов и самими типами можно продолжить, введя конструкторы видов типа – виды высокого рода! Соответственно, для классификации таких полиморфных видов типов потребуется ввести некие виды видов типов, которые, во избежание всё того же парадокса Жирара, будут относится уже к следующей вселенной типов . Таким образом по индукции можем получить бесконечную последовательность вселенных типов: $U_0,\;U_1,\;U_2,\;\ldots$

Любопытно, что все вселенные устроены одинаково (без учёта концепции вложенности, рассмотренной далее). Например, ранее был представлен вид типов, аналогичный типу натуральных чисел, и таким же способом можно описать обитателей и более далёких вселенных. Интересной является возможность написания кода, который бы одинаково работал для типов из любой вселенной. Такая возможность уже реализована в некоторых языках (Agda, Coq) и называется она “полиморфизм вселенных“.

Можно также заметить, что вселенная видов типов похожа на вселенную типов примерно также, как типы похожи на значения – выше было продемонстрированно, как вычисления можно производить на уровне типов почти также, как это можно делать и со значениями. Это даёт основания для включения в последовательность вселенных типов ещё одну – вселенную значений с не очень удачным индексом $U_{-1}$ . Она является выделенной, начальной, в том смысле, что “типы” этой вселенной уже больше ничего не индексируют, вселенных с меньшими индексами просто не существует (но так ли это??).

Пожалуй, самое интересное в концепции вселенных типов то, что между ними можно путешествовать! Для этого достаточно построить функцию от типа из одной вселенной к типу другой. И хотя в Sacla для взаимодействия с далёкими вселенными есть только упомянутый ранее Anykind, но всё же доступны червоточины между $U_{-1}$ и , то бишь между значениями и типами.

Отображение из в $U_{-1}$ уже встречались в этой статье – это обобщённые функции. Действительно, достаточно передать туда типы-параметры, и обобщённая функция становится обычным значением функционального типа:

val doubleA                  // червоточина  
  : [A] => A      => (A, A)  // из вселенной типов в значение-функцию  
  = [A] => (a: A) => (a, a)  // техника сейчас не важна  
  
val doubleInt                // сюда положим значение  
  : Int => (Int, Int)        // простого типа  
  = doubleA[Int]             // вжух!

В Scala существуют также возможности и обратного путешествия – от значений в типы! О, это очень сильное колдунство под названием зависимые типы. Посмотрим на такой код:

trait IHaveAType { type Type; val v: Type }     // трейт содержит членом абстрактный тип!
val valWithInt:    IHaveAType =                 // червоточина 1
  new IHaveAType { type Type = Int;    val v = 42 }
val valWithString: IHaveAType =                 // червоточина 2
  new IHaveAType { type Type = String; val v = "вселенная" }
  
val doubleDep // функция, ТИП результата которой зависит от ЗНАЧЕНИЯ первого аргумента  
  : (carier: IHaveAType) => (carier.Type, carier.Type)       // вжух туда!
  = (carier: IHaveAType) => doubleA[carier.Type](carier.v)   // вжух обратно!

val stringsPair: (String, String) = doubleDep(valWithString) // ("вселенная", "вселенная")
val intsPair:    (Int, Int)       = doubleDep(valWithInt)    // (42, 42)
//               ↑↑↑↑↑↑↑↑↑↑ указание иных типов приведёт к ошибке компиляции!
//               а всё потому, что тип valWithInt хитрее чем кажется: IHaveAType { type Type = Int }

Тут в строке вжух туда! выражение carier.Type телепортирует из $U_{-1}$ в , а в следующей строке возвращаемся обратно уже знакомым способом. Зависимые типы не редко используется в Scala – по большей части в популярных библиотеках, но можно встретить и в продуктовом коде. Это очень интересная, но очень объёмная тема, рассмотрение которой стоит отложить на другой раз.

Сама функция, переводящая из одной вселенной в другую, относится ко вселенной с максимальным индексом, и в случае описанных выше путешествий, это была вселенная типов . Но чаще считают, что такие функции работают с типами одной и той же вселенной, однако действует простое, но важное правило: вселенные со старшими индексами включают все вселенные с меньшими: $U_{-1}:U_{0}:U_{1}:U_{2}:\ldots$ Таким образуется кумулятивная иерархия вселенных. А вот мультивселенной $U_{\infty}$ , включающей в себя все остальные вселенные попросту не существует (это всё выдумки киношников!) из-за всё того же парадокса Жирара.

Ещё почитать про вселенные типов можно тут:

пара ответов на вопросы о кумулятивных вселенных;
статья на nLab;
pdf-статьи:

Путешествие к далёким вселенным таит множество опасностей для неподготовленного приключенца. По этому в следующей части вернёмся в нашу вселенную, к привычным классам и типам.

Комментарии (3)

Anarchist
14.04.2024 03:48
#26721749
Спасибо! А как лайк поставить несколько раз? :)
1. Underskyer1 Автор
  14.04.2024 03:48
  #26721929
  +1
  Вам спасибо за отзыв! В этой публикации только первая часть обзора. Если сочтёте, что другие части также достойны внимания читателей, то можете проголосовать и там))
1. dididididi
  14.04.2024 03:48
  #26723753
  Просто лайк под этой статьёй делает умнее!д