Рекурсивные типы. Часть 5/5. Занимательный матан / Хабр

Мастера Угвэя ничуть не удивляло, что отношения между типами напоминают школьную математику.

Содержание пятой части:

Натуральные числа
Разложение в ряд
Производные от типов
Производные от экспоненциалов
Производные от рекурсивных типов
Список литературы
Зак��ючение по всему обзору

Другие части обзора

Натуральные числа

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

type Nat = μ[Option]

Продемонстрировать это не сложно. Сперва введём более удобные конструкторы:

// основные
val zero:          Nat = inFix[μ, Option](None   )
def succ(n:Nat):   Nat = inFix[μ, Option](Some(n))
// вспомгательные
val one:           Nat = succ(zero)
def toNat(i: Int): Nat = (1 to i).foldRight(zero)((_, acc) => succ(acc)) // не корректно для отрицательных i, но сейчас это не важно

Затем реализуем обычную арифметику по Пеано:

extension (nat: Nat)
  def +     = foldFix[μ]((_: Option[Nat]).fold(nat )(succ   ))
  def *     = foldFix[μ]((_: Option[Nat]).fold(zero)(_ + nat))
  def **    = foldFix[μ]((_: Option[Nat]).fold(one )(_ * nat))  
  def toInt = foldFix[μ]((_: Option[Int]).fold(0   )(_ + 1  ))(nat)

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

А работает наша арифметика следующим образом:

val two   = succ(one)
val three = succ(two)
val six   = toNat(6)

val theAnswer = (two * three) ** two + six
theAnswer.toInt // 42

Важно обратить внимание, что конструкторы Nat реализованы через inFix, а арифметические операции и деконструкция в Int – через foldFix. Пара этих методов как раз определяет основные возможности для наименьшей неподвижной точки μ, введённой в предыдущей части статьи. Вообще, всё полезное, что может дать тип Nat, выражается через свёртку этого рекурсивного типа! Например, факториал – это свёртка Nat в такой же рекурсивный Nat:

def factorial: Nat => Nat =
  foldFix[μ][Option][(Nat, Nat)]{
    _.fold((one, one))((n, fact) => succ(n) -> fact * n)
  } andThen {_._2}

factorial(toNat(5)).toInt // 120

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

«Несчётные» типы

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

Разложение в ряд

Ранее список был выражен через неподвижную точку конструктора типов OptCell:

$\begin{align}OptCell[A][X] &\cong 1 + A \times X,\\List[A] &= \mu[OptCell[A]]\\\end{align}$

При этом μ определялся в стиле передачи продолжений, чтобы скрыть «ссылку на себя». Но давайте теперь посмотрим на чуть более привычное определение списка:

$List[A] = 1 + A \times List[A]\\$

Это не что иное, как функциональное уравнение для «функции» List[A]. Выражение справа можно попробовать раскрыть, шаг за шагом подставляя вместо List[A] всё выражение целиком. У нас будет получаться такая бесконечная сумма:

$List[A] = 1 + A + A \times A + A \times A \times A + \ldots = \sum_{n=0}^\infty A^n\\$

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

$List[A] = \frac1{1 - A}\\$

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

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

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

И такие выражения появляются не только при работе со списками. К примеру, обычное бинарное дерево представляется следующим функциональным уравнением:

$Tree[A] = 1 + A \times Tree[A] \times Tree[A]\\$

Его «решением» является такой ряд:

$Tree[A] = 1 + A + 2 A^2 + 5 A^3 + 14 A^4 + \ldots\\$

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

Производящая функция этого ряда будет содержать радикал:

$Tree[A] = \frac{1-\sqrt{1-4A}}{2A}\\$

Второе решение

Второе решение, со знаком перед корнем из дискриминанта оказывается непродуктивным. Разложение подразумевает «малость» , но при $A \rightarrow 0$ такое решение устремляется в «бесконечность», и сложно понять, как использовать получаемый ряд: $1/A - 1 - A - 2 A^2 - 5 A^3 + \ldots$

Если построить дерево с пятью или более ветвями в узле, то точное решение для соответствующего функционального уравнения не удастся получить. Тем не менее, разложение в ряд интерпретируется также просто, как и в случае бинарного дерева.

И всё же, не все полиномиальные рекурсивные типы приводят к полезным разложениям в ряд. Рассмотрим такой тип:

$\begin{eqnarray}UMagma[A] &=& A + 1 + UMagma[A] \times UMagma[A]\\UMagma[A] &=& \frac12 \left(1 \pm \sqrt{-4 A - 3}\right)\\\end{eqnarray}$

При попытке разложения UMagma[A] в ряд выясняется, что все его коэффициенты бесконечны! Другими словами, для любого заданного наперёд количества элементов существует бесконечное множество различных форм дерева такой структуры. Причём, сам по себе тип корректный и не бесполезный:

final case class UMagma[A](value: A `Either` Option[(UMagma[A], UMagma[A])])

def leaf[A](a: A) = UMagma(Left(a))
def twig[A] = UMagma[A](Right(None))
def node[A](left: UMagma[A], right: UMagma[A]) = UMagma(Right(Some(left, right)))

val someTree = node( //     /\
  leaf(42),          //   42  \
  twig               //        ∅
)

val sameTree = node( //     /\
  leaf(42),          //   42  \
  node(              //       /\    // ∅ добавляются неограниченно.
    twig,            //      ∅  \   // вот откуда возникают
    twig             //          ∅  // все эти бесконечные формы 
  )                                 // для одинакового количества A
)

Неподвижные точки любых полиномиальных конструкторов типов («алгебраические» типы, состоящие из сумм произведений) представляют собой различные деревья. Вырожденными случаями таких деревьев являются и списки (дерево с единственной веткой), и даже натуральные числа:

$Nat \cong List[Unit]$

Функциональное уравнение для натуральных чисел выглядит просто

Тип не параметризирован, и единственное решение уравнения – бесконечность)).

Что же до неподвижных точек конструкторов типов, в которых есть экспоненциалы (типы функций), то тут картина такая. Если тип-параметр хотя бы раз находится в отрицательной позиции, то, как уже говорилось ранее (см. в конце этого раздела), такая неподвижна точка неконструктивна и с её значениями не получится работать. В прочих же случаях, когда тип-параметр является результатом какой-либо функции, например $A^{Int}$ («степенной» тип), то тип в значении экспоненты, как говорилось ранее, считается счётным, изоморфным Nat. Это означает что все степенные типы можно представить как произведения типа-параметра с самим собой. Соответственно, неподвижные точки таких выражений можно трактовать как знакомые деревья, просто с большим количеством ветвей в узлах.

Производные от типов

Контейнерные типы F[+_] используют для обслуживания различных эффектов (см. предыдущую статью цикла). Такие типы определяют некий контекст преобразований, производящихся над «значениями внутри» контейнера. Но после всех преобразований неизбежно следует «распаковка» F[A] => B. В частности, для многих контейнеров важно извлечение именно «хранимого» значения F[A] => A. Этот вариант сейчас и рассмотрим подробнее.

Попробуем выяснить, получится ли выразить контекст «хранения» значения в контейнере F[A] в виде некого типа ∂[F][A]. Тогда результат распаковки можно было бы записать как пару (∂[F][A], A). Мы как бы «выкалываем» какое-то одно значение A из F[A].

В простых случаях это действительно возможно:

type Const[X] = SomeType
type Id   [X] = X

summon[∂[Const][X] =:= Nothing] // 0    (Nothing, A) ≅ Nothing
summon[∂[Id   ][X] =:= Unit   ] // 1    (Unit, A) ≅ A = F[A]

Для контейнера Id имеем тривиальный результат – контекст не несёт ничего, кроме самого факта хранения значения типа A. В то же время тип Const[X] не использует в теле параметр X, значит он не может хранить значение и не содержит никого контекста.

Так как извлекается единственное значение, то для суммы типов в контексте должен сохранится выбор, из какого именно слагаемого достаём значение:

infix type  +[A,    B   ] = A `Either` B
infix type ++[F[_], G[_]] = [X] =>> F[X] + G[X]

summon[∂[F ++ G][X] =:= ∂[F][X] + ∂[G][X]]

summon[∂[Id ++ (Const ++ Id)][X] =:= Unit + Unit]
//    ∂ₓ[X  + (SomeType + X)]    =:=   1  +  1   ≅ Boolean  - тип с двумя вариантами, местом вхождения X

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

infix type  ×[A,    B   ] = (A, B)
infix type ××[F[_], G[_]] = [X] =>> F[X] × G[X]

summon[∂[F ×× G]][X] =:= ∂[F][X] × G[X] + F[X] × ∂[G][X]]

summon[∂[Id ×× (Const ++ Id) ][X] =:= SomeType + X + X]
summon[∂[Id ×× Id ×× Id ×× Id][X] =:= (X × X × X) + X × (X × X + X × (X + X))]
//     ∂[ X  ×  X  ×  X  ×  X]     ≅  4 × X × X × X

Получается, что контекст «хранения» значения X в четырёхместном кортеже (X, X, X, X) – это не только оставшиеся значения (X, X, X) но также ещё и тип 4, значение которого указывает, в какой из четырёх позиций исходного кортежа лежал наш X.

Deja vu… Но и это ещё не всё. Так же из общих соображений поиска контекста извлекаемого из контейнера значения можно также получить и «цепное правило» для вложенных контейнеров. При извлечении значения из вложенного контейнера у нас остаются контексты от обоих контейнеров:

summon[∂[F ∘ G]][X] =:= ∂[F][G[X]] × ∂[G][X]]

type Prod1[X] = X × X
type Prod2[X] = X × SomeType

summon[∂[Prod1 ∘ Prod2][X]  =:= (X × SomeType + X × SomeType) × SomeType]

Выпишем эти соотношения в виде математических формул:

$\begin{eqnarray}\partial_A Const &=& 0 \hspace{2cm} \text{выражение $Const$ не содрежит типовой переменной $A$}\\\partial_A A &=& 1\\\partial_A \left(F[A] + G[A]\right) &=& \partial_A F[A] + \partial_A G[A]\\\partial_A \left(F[A] \times G[A]\right) &=& G[A] \times \partial_A F[A] + F[A] \times \partial_A G[A]\\\partial_A \left(F[G[A]]\right) &=& \partial_X F[X]_{{}_{X = G[A]}} \times \partial_A G[A]\\\end{eqnarray}$

Числа (0, 1, 2 и другие) обозначают типы с соответствующим количеством «обитателей» (Nothing, Unit, Boolean и т.д.). Ещё в дальнейшем нам пригодится дополнительное правило для многоаргументного контейнера, которое можно вывести из тех же положений:

$\partial_A\; F[G[A],\; H[A]] =\left.\partial_G\; F[G,\; H[A]]\right._{{}_{G=G[A]}} \times \partial_A G[A] +\left.\partial_H\; F[G[A],\; H]\right._{{}_{H=H[A]}} \times \partial_A H[A]$

Все эти правила действительно напоминают обычное дифференцирование функций. По этой причине подобные контексты называют производными от типов.

Но на эту картину можно взглянуть и по-иному. Дело в том, что извлекаемое значение и контекст расположения в контейнере вместе несут всю информацию для восстановления исходного контейнерного значения. Ничего не теряется, но нужно также учесть, что для некоторых F[_] могут существовать такие значения F[A], в которых вообще нет ни одно��о значения A (например, для Option[A] это будет None: Option[Nothing]). С учётом вышесказанного, для любых (полиномиального) F[_] и A может быть построен следующий изоморфизм:

$F[A] \cong \partial_A F[A] \times A + F[0] \tag{DiffIso} \label{DiffIso}$

Извлекая каким-либо способом из F[A] значение A вместе с контекстом, всегда можно восстановить исходное значение! Так что на этот изоморфизм можно смотреть не только как на дифференцирование (получение ∂[F][A]) и интегрирование (восстановление F[A]), но и как простое правило деления с остатком.

Действительно, попробуем разделить на . Делимое раскладывается на следующие простые множители: $18=2\times3\times3$ . В разложении отсутствует число , контекст его расположения в равен . В свою очередь, без – это те же $18_{5=0}=18$ . Таким образом, $18 = 0 \times 5 + 18$ . Для демонстрации аналогии с типами мы не будем пользоваться возможностями натуральных чисел, выделять ту часть делимого, которая будет-таки делиться на . Если мы по тем же правилам поделим на , то получим контекст $(2\times3\times3) / 3 = 2\times3 = 6$ , а остаток $18_{3=0} = 2\times0\times3 = 0$ , то есть $18=6\times3+0$ . Здесь действуют всё те же правила получения контекста, выведенные ранее для типов. Принципиальное же отличие заключается в том, что натуральные числа, внезапно, сложнее! Дело в том, что для них умножение коммутативно, поэтому нет разницы, где в выражении $3\times3$ стоит нужная . Можно считать, что мы вроде бы и получаем контекст $2\times3$ , но двойка сокращается из-за неразличимости $\_ \times 3$ и $3 \times \_$ . В то время как для типов этот коэффициент не сокращается и играет важную роль. Поэтому «деление с остатком» для типов выглядит как вычисление производных.

В Scala 3 вычисление типа контекста можно реализовать с помощью сопоставления типов. Этот механизм позволяет создавать конструкторы типов, описывающие целые семейства типов. И, в отличие от обычных псевдонимов типов, здесь в вариантах можно явно ссылаться на определяемый тип, образуя рекурсию.

Для дифференцирования потребуется несколько типов. Сперва нам нужен тип, который отметит все вхождения типа-параметра в контейнер. Этот фантомный тип Hole по-хорошему должен быть недоступен для пользователей… но сделаем его хотя бы бесполезным для них)). Нужно также семейство типов DiffHolled с четырьмя (как минимум) правилами дифференцирования. По одному из этих правил должен возвращаться нулевой тип, но, к сожалению, Nothing не подойдёт, так как существующий мех��низм сопоставления типов завязан на подтипизацию. Лучше заведём ещё один фантомный тип Zero. Простое применение правил дифференцирование приведёт к кучерявым структурам, со жуткими сложениями и умножениями нулевого и единичного типов. Поэтому нам не обойтись без семейства типов Simplify, упрощающего алгебраическое выражение типов (и в помощь ему ещё пара нерекурсивных семейств типов). И в самом конце нужно будет подставить тип-параметр X вместо дырок Hole – сделаем это с помощью семейства типов SubstHole.

private object zero
opaque type Zero = zero.type // Nothing не сработает ((

private object hole
opaque type Hole = hole.type // тип дырки в идеале должен быть недоступен пользователям

type SimplifiedSum[a, b] = a match
  case Zero   => b
  case _      => b match
    case Zero => a
    case _    => a + b

type SimplifiedProd[a, b] = a match
  case Zero   => Zero
  case Unit   => b
  case _      => b match
    case Zero => Zero
    case Unit => a
    case _    => a × b

type Simplify[T] = T match // упрощение алгебраического выражения
  case a + b  => SimplifiedSum [Simplify[a], Simplify[b]] // рекурсия!
  case a × b  => SimplifiedProd[Simplify[a], Simplify[b]] // рекурсия!
  case _      => T

type DiffHolled[T] = T match // основные правила дифференцирования
  case Hole   => Unit
  case a + b  => Simplify[DiffHolled[a]     +     DiffHolled[b]]  // рекурсия!
  case a × b  => Simplify[DiffHolled[a] × b + a × DiffHolled[b]]  // рекурсия!
  case _      => Zero

type SubstHole[T, X] = T match // подстановка X в «дырку»
  case Hole   => X
  case a + b  => SubstHole[a, X] + SubstHole[b, X]  // рекурсия!
  case a × b  => SubstHole[a, X] × SubstHole[b, X]  // рекурсия!
  case _      => T

type ∂[F[_]] = [X] =>> SubstHole[DiffHolled[F[Hole]], X] // собственно дифференцирование

Любопытная особенность: типы Simplify, DiffHolled, SubstHole являются рекурсивными, и их даже можно описать через неподвижные точки, вроде введённой в предыдущей части FixF (что в данном случае привело бы к переусложнению). Ведь даже «простые» типы данных представляют собой деревья алгебраических выражений, то есть фактически являются рекурсивными структурами!

Эти конструкции неплохо работают для кортежей (пар) и Either. Их вполне можно использовать для соответствующих конструкторов типов. Но универсальный тип ∂[_[_]][_] подразумевает использование его значений в универсальных методах. Ключевым свойством для этого типа является изоморфизм (DiffIso). Для каждого контейнерного значения можно получить список распакованных значений с их контекстами, и пересобрать контейнер, подставляя в эти контексты уже, возможно, другие значения:

def decompose[F[_], X]: F[X]        => Seq[X × ∂[F][X]]
def integrate[F[_], X]: X × ∂[F][X] => F[X]

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

Производные от типов сами по себе являются контейнерами, и их также можно представить как «значение в контексте его расположения». Значит для исходного контейнера возможны и более сложные разложения:

$F \cong \partial_X (\partial_X F) \times X \times X + \partial_X F|_{{}_{X = 0}} \times X + F|_{{}_{X = 0}}$

Дальнейшие же разложения не приведут к привычному ряду Тейлора, с факторами 1/n! ввиду, опять же, того, что произведение типов не коммутирует и значение каждого множителя из $X \times \ldots \times X$ должно попадать именно в свой контекст.

Производные от экспоненциалов

Объявленные выше правила получения контекста расположения действуют только для сумм и произведений типов. Но как быть с экспоненциалами (типами функций)? Для функции F[X] = Boolean => X контекст очевиден: $\partial_X\; X^2 \cong \partial_X\; (X \times X) = 2 \times X^1$ . Аналогичная ситуация с перечислениями: для любого enum NCases с N вариантами всегда можно написать другой enum NMinusOneCases, у которого вариантов будет на один меньше. Для таких перечислений будет работать формула

$\partial_X\; X^n = n \times X^{n-1}$

Секрет заключается в возможности представления степенных типов в виде произведения. В то же время, вычитание единицы из бесконечного типа Nat ( $\mathbb{N}$ ), введённого в начале этой публикации, даст в точности его же, и контекст будет таким:

$\partial_X\; X^{\mathbb{N}} = \mathbb{N} \times X^{\mathbb{N}}$

Вычитать единичный тип из Int, у которого более четырёх миллиардов вариантов, задача весьма неблагодарная, хотя и решаемая (например, с помощью зависимых типов библиотеки iron). Полезность дифференцирования степенных типов определяется трактовкой «вычитания единицы» из типа показателя.

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

type Class[X] = X => Boolean

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

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

opaque type Set[X] <: X => Boolean = X => Boolean
object Set:
  def empty[X]    : Set[X] = _ => false
  def one[X](x: X): Set[X] = _ == x

  extension[X](set: Set[X])
    infix def ||(set2: Set[X]): Set[X] = x => set(x) || set2(x)
    infix def &&(set2: Set[X]): Set[X] = x => set(x) && set2(x)

Такие множества можно представить как контейнеры значений X – предикат будет возвращать true только для тех x: X, которые есть в это контейнере. Множество размера – это любой из всевозможных n-кортежей. Так как для множества не важно, в каком порядке оно собиралось, все кортежи с переставленными одинаковыми элементами будут эквивалентны. «Мощность» такого множества будет равна «мощности» кортежа, делённого на количество перестановок (в множестве все элементы различны!). Совокупностю множеств всех размеров будет:

$Set[X] = \sum_{n=0}^{\infty} \frac{X^n}{n!} \tag{Set} \label{Set}$

Несложно проверить, что такой контейнер при дифференцировании ведёт себя как экспонента!

$\partial_X Set[X] = Set[X]$

Секрет превращения контравариантного типа X => Boolean в ковариантный контейнер заключается в том, что, фиксировав конструкторы, мы по сути изменили его тип на примерно такой:

type Set[X] = μ[SetBase[X]]
type SetBase[X] = [Self] =>> Unit + X + Self × Self + Self × Self
//                          empty  one       ||            &&

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

Также рассмотрим такой классификатор:

type Bag[X] = X => Nat

Его можно интерпретировать как контейнер, но который «хранит произвольное количество» одинаковых значений (собственно, количество этот классификатор и возвращает). Кстати, для Bag актуален такой же набор конструкторов, что и для Set, и представление через неподвижную точку будет в точности таким же. Однако не совсем понятно, как честно выразить Bag в виде ряда. Не видно, как правильно подсчитать эквивалентные кортежи заданного размера, ведь значения в них могут повторяться. А без этого невозможно получить контексты расположения значений в этом контейнере. Можно заключить, что существуют такие экспоненциальные типы, которые, даже если и получится использовать их как контейнеры, но не понятно как их честно определить контексты хранящихся там значений.

Производные от рекурсивных типов

Концепция «контекста расположения значения» лучше всего раскрывается в приложении к рекурсивным типам. Правил из предыдущего раздела достаточно, чтобы научиться дифференцировать неподвижные точки $T[A] = \mu X. Base[A, X]$ .

Сперва с помощью outFix развернём $T[A] \rightarrow Base[A, T[A]]$ , и раскроем производную. Полученное линейное рекурсивное соотношение для $\partial_A\; T[A]$ выразим через неподвижную точку $\mu$ . Получившаяся неподвижная точка очень похожа на список, только «пустой» вариант отличен от . Его смело можно вынести наружу как множитель (при разложении в ряд у каждого члена будет такой коэффициент), и тогда останется обычный список. В итоге получается частная производная от Base по первому аргументу и список производных по второму:

$\begin{eqnarray} \tag{DiffRec}\label{DiffRec} \partial_AT[A] &=& \partial_A Base[A, T[A]] \\ &=& \left.\partial_X Base[X, T[A]]\right._{{}_{X=A}} + \left.\partial_X Base[A,X]\right._{{}_{X=T[A]}} \times \underline{\partial_A T[A]}\\ &=& \mu Y. \left( \left. \partial_X Base[X, T[A]]\right._{{}_{X=A}} + \left.\partial_X Base[A,X]\right._{{}_{X=T[A]}} \times Y \right)\\ &=& \left. \partial_X Base[X, T[A]]\right._{{}_{X=A}} \times \mu Y. \left( 1 + \left.\partial_X Base[A,X]\right._{{}_{X=T[A]}} \times Y \right)\\ &=& \left. \partial_X Base[X, T[A]]\right._{{}_{X=A}} \times\, List \left[\left.\partial_X Base[A,X]\right._{{}_{X=T[A]}}\right]\\ \end{eqnarray}$

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

type diffμ[Base[_, _]] = [A] =>>
  List[∂[[X] =>> Base[A, X]][μ[[T] =>> Base[A, T]]]] ×  
       ∂[[X] =>> Base[X, μ[[T] =>> Base[A, T]]]][A]

Разберём как это работает на примере такого тернарного дерева:

type Base3[A, T] = Unit + A × (T × T × T) // 1 + A × T × T × T  
type Tree3[A] = μ[[T] =>> Base3[A, T]]

type Tree3Context[A] = diffμ[Base3][A]  
  
type T = Tree3[Int]  
summon[Tree3Context[Int] =:= List[Int × ((T + T) × T + T × T)] × (T × T × T)]
//                           List[Int × 3 × T × T]             ×  T × T × T

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

Пример конкретного ��ерева типа Tree3. Крестиками отмечены пустые поддеревья, кружками - значения типа A. Нас интересует значение в узле красного цвета. — Пример конкретного дерева типа Tree3. Крестиками отмечены пустые поддеревья, кружками - значения типа A. Нас интересует значение в узле красного цвета.

Здесь представлен пример конкретного тернаного дерева типа Tree3[A]. Сфокусируемся на значении A в <font color="red">красном</font> узле. Путь к нему отмечен чёрными стрелками. Пройденные мимо поддеревья окрашены в разные цвета. Оставшиеся за нашим фокусом поддеревья отмечены <font color="red">фиолетовым</font>. Представим, что мы как бы «подняли» это дерево, взявшись за корневой и фокусный узлы, «ориентировали» его вдоль той единственной ветки, что ведёт к нужному значению.

То же дерево, просто перерисовали по-другому – вытянули его вдоль ветви, на которой находится фокусный узел.

Чтобы не потерять информацию, нужно не забыть, какая из трёх развилок выбрана в каждом узле на пути к фокусному: левая, средняя, или правая.

Осталось только стереть все стрелки, связывающие фокусное значение с исходным деревом:

Значение Tree3 может быть декомпозировано на значение A вместе с контекстом его расположения в исходном дереве – списком игнорированных поддеревьев на пути к значению, а также поддеревьями, расположенными после A. — Значение Tree3 может быть декомпозировано на значение A вместе с контекстом его расположения в исходном дереве – списком игнорированных поддеревьев на пути к значению, а также поддеревьями, расположенными *после* A.

На последней картинке проявляется смысл составляющих производной рекурсивной структуры. Список определяет путь к фокусному значению с оставленными позади поддеревьями и указанием, куда продолжать путь на развилках (тип с тремя значениями в случае Tree3). И ещё тут есть все поддеревья, до которых мы не добрались.

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

«однодырочный контекст» расположения в дереве какого-либо его поддерева (а не одного значения);
«застёжка» (zipper) – это поддерево в своём однодырочном контексте.

type OneHoleContext[Base[_, _]] = [A] =>> List[∂[[X] =>> Base[A, X]][μ[[T] =>> Base[A, T]]]]
type Zipper        [Base[_, _]] = [A] =>> OneHoleContext[Base][A] ×  μ[[T] =>> Base[A, T]]
//   Zipper[Base] = OneHoleContext[Base] × μ[Base] ≅ μ[Base]         ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ - поддерево μ[Base]

Застёжка изоморфна исходному контейнеру (непустому и с фокусом на конкретном поддереве в нём) ввиду того, что для любого дерева $T \equiv \mu X. Base[A, X]$ можно построить изоморфизм

$A \times \partial_A Base[A, T] \cong T$

Здесь множитель обозначает головной (коренной?) элемент, а $\partial_A Base[A, T]$ – его поддеревья. Этот изоморфизм получается из (DiffIso) и (DiffRec) для случая, когда путь тривиален, то есть список однодырочного контекста пустой.

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

$\begin{align}\partial_X List[X] &= \partial_X \left(\frac1{1-X}\right)=\\&=\frac1{(1-X)^2}=\\&=\frac1{1-X}\times\frac1{1-X}=\\\\&=List[X] \times List[X]\end{align}$

Действительно, контекстом значения в списке является пара списков – предшествующие значения и последующие. Для дерева можно провести аналогичные вычисления, только выразить производную через тип исходного дерева будет несколько сложнее (и нужно будет учесть, что $1/(1-2 \times X \times Tree[X]) = List[2 \times X \times Tree[X]]$ ).

Список литературы

Abusing the algebra of algebraic data types - why does this work? – несколько ответов на StackOverflow о тесной связи теории типов с алгеброй и матанализом.
Unordered tuples and type algebra – статья про подсчёт перестановок в кортежах (в тему о представлении в качестве контейнера).
Про дифференцирование типов:
- Haskell/Zippers. В начале идёт забавная история, как программист Ариадна помогает Тесею найти путеводную нить для древовидного лабиринта Минотавра)).
- The Derivative of a Regular Type is its Type of One-Hole Contexts (pdf). Тут строгий вывод правил дифференцирования типов. Есть и более глубокие исследования, вроде Derivatives of Containers, но при желании можно их найти самостоятельно.

Заключение по всему обзору

Здесь были раскрыты следующие темы:

рекурсия и неподвижные точки функций;
рекурсивные типы – это способ формализации рекурсивных алгоритмов;
- неподвижные точки конструкторов типов, как средства описания любых рекурсивных типов;
- все неподвижные точки изоморфны, но среди них выделяются самые главные – наименьшая и наибольшая;
- наименьшая неподвижная точка характеризуется парой функций (свёртка, конструктор), где свёртка – рекурсивная;
- наибольшая неподвижная точка характеризуется парой функций (развёртка, деконструктор), где развёртка – рекурсивная;
свободные контейнеры трансформируют любые другие контейнеры, обогащая их возможностями комбинирования контейнерных вычислений вида A => F[B], что очень полезно при обработке эффектов;
- свободные контейнеры позволяют обходить ограничение на стек в рекурсивных вычислениях;
- популярные примеры реализаций свободных контейнеров;
схемы рекурсии – это частные случаи обобщения свёртки/развёртки для типовых задач;
- все схемы рекурсии выражаются через две исходные функции свёртки и развёртки;
- свободные контейнеры позволяют «заглядывать в прошлое» и решать задачи динамического программирования;
- ко-свободные контейнеры позволяют «заглядывать в будущее» и преобразовывать списки в деревья;
типизированное программирование тесно связано с математикой (выводы по данной пятой части обзора);
- натуральные числа – это рекурсивный тип, совмещающий в себе родственные идеи конструктивной математики и последовательных вычислений;
- программисты по большей части имеют дело с неподвижными точками «полиномиальных» конструкторов типов (также известных, как «алгебраических», составленных из сумм произведений типов);
- полиномиальные рекурсивные типы можно представить в виде степенных рядов, что открывает иную точку зрения на их структуру;
- рекурсивные определения неподвижных точек иногда удаётся решить явно – полученные выражения (с вычитаниями, делениями и радикалами) можно рассматривать как производящие функции для степенных рядов;
- многие контейнерные типы обладают семантикой хранения значения типа-параметра в контексте его расположения в контейнере, и этот контекст тоже можно выразить в виде него типа;
- даже контравариантные конструкторы типов иногда можно трактовать, как рекурсивные ковариантные контейнеры;
- вычисление типа контекста напоминает «деление с остатком», но следует привычным правилам вычисления производной;
- лучше всего производные раскрываются именно для рекурсивных полиномиальных типов (деревьев).

Концепция повторения действий может быть реализована единообразно для самых разных сценариев. Это устраняет необходимость «велосипедить» собственные циклы, ил�� рекурсию. Обработка наборов данных может быть выражена через неподвижные точки конструкторов типов – для них, как правило, уже реализованы все рекурсивные алгоритмы, и остаётся только корректно замоделировать в типах условие конкретной задачи.

В обзоре не раз обнаруживались отсылки к другим важным и объёмным темам. Например, свойства рекурсивных типов обусловлены соотношениями, которые формулируются и доказываются на языке теории категорий. А разнообразие используемых на практике типов опирается на не менее интересное понятие «зависимые типы». Эти темы стоит обсудить более обстоятельно, но как-нибудь в другой раз)).

Рекурсивные типы. Часть 5/5. Занимательный матан