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

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

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

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

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

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

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

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

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

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

• Часть 1. Рекурсия.

• Часть 2. Неподвижные точки конструкторов типов.

• Часть 3. Свободные контейнеры.

• Часть 4. Схемы рекурсии.

• Часть 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:

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

Это не что иное, как функциональное уравнение для «функции» List[A]. Выражение справа можно попробовать раскрыть, шаг за шагом подставляя вместо List[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. Это означает что все степенные типы можно представить как произведения типа-параметра с самим собой. Соответственно, неподвижные точки таких выражений можно трактовать как знакомые деревья, просто с большим количеством ветвей в узлах.

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

Контейнерные типы 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]

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

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

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

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

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

Действительно, попробуем разделить на . Делимое раскладывается на следующие простые множители: . В разложении отсутствует число , контекст его расположения в равен . В свою очередь, без – это те же . Таким образом, . Для демонстрации аналогии с типами мы не будем пользоваться возможностями натуральных чисел, выделять ту часть делимого, которая будет-таки делиться на . Если мы по тем же правилам поделим на , то получим контекст , а остаток , то есть . Здесь действуют всё те же правила получения контекста, выведенные ранее для типов. Принципиальное же отличие заключается в том, что натуральные числа, внезапно, сложнее! Дело в том, что для них умножение коммутативно, поэтому нет разницы, где в выражении стоит нужная . Можно считать, что мы вроде бы и получаем контекст , но двойка сокращается из-за неразличимости и . В то время как для типов этот коэффициент не сокращается и играет важную роль. Поэтому «деление с остатком» для типов выглядит как вычисление производных.

В 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[X] = Boolean => X контекст очевиден: . Аналогичная ситуация с перечислениями: для любого enum NCases с N вариантами всегда можно написать другой enum NMinusOneCases, у которого вариантов будет на один меньше. Для таких перечислений будет работать формула

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

Вычитать единичный тип из 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-кортежей. Так как для множества не важно, в каком порядке оно собиралось, все кортежи с переставленными одинаковыми элементами будут эквивалентны. «Мощность» такого множества будет равна «мощности» кортежа, делённого на количество перестановок (в множестве все элементы различны!). Совокупностю множеств всех размеров будет:

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

Секрет превращения контравариантного типа 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 в виде ряда. Не видно, как правильно подсчитать эквивалентные кортежи заданного размера, ведь значения в них могут повторяться. А без этого невозможно получить контексты расположения значений в этом контейнере. Можно заключить, что существуют такие экспоненциальные типы, которые, даже если и получится использовать их как контейнеры, но не понятно как их честно определить контексты хранящихся там значений.

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

Концепция «контекста расположения значения» лучше всего раскрывается в приложении к рекурсивным типам. Правил из предыдущего раздела достаточно, чтобы научиться дифференцировать неподвижные точки .

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

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

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

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

На последней картинке проявляется смысл составляющих производной рекурсивной структуры. Список определяет путь к фокусному значению с оставленными позади поддеревьями и указанием, куда продолжать путь на развилках (тип с тремя значениями в случае 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]

Застёжка изоморфна исходному контейнеру (непустому и с фокусом на конкретном поддереве в нём) ввиду того, что для любого дерева можно построить изоморфизм

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

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

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

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

• 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], что очень полезно при обработке эффектов;

  • свободные контейнеры позволяют обходить ограничение на стек в рекурсивных вычислениях;

  • популярные примеры реализаций свободных контейнеров;

• схемы рекурсии – это частные случаи обобщения свёртки/развёртки для типовых задач;

  • все схемы рекурсии выражаются через две исходные функции свёртки и развёртки;

  • свободные контейнеры позволяют «заглядывать в прошлое» и решать задачи динамического программирования;

  • ко-свободные контейнеры позволяют «заглядывать в будущее» и преобразовывать списки в деревья;

• типизированное программирование тесно связано с математикой (выводы по данной пятой части обзора);

  • натуральные числа – это рекурсивный тип, совмещающий в себе родственные идеи конструктивной математики и последовательных вычислений;

  • программисты по большей части имеют дело с неподвижными точками «полиномиальных» конструкторов типов (также известных, как «алгебраических», составленных из сумм произведений типов);

  • полиномиальные рекурсивные типы можно представить в виде степенных рядов, что открывает иную точку зрения на их структуру;

  • рекурсивные определения неподвижных точек иногда удаётся решить явно – полученные выражения (с вычитаниями, делениями и радикалами) можно рассматривать как производящие функции для степенных рядов;

  • многие контейнерные типы обладают семантикой хранения значения типа-параметра в контексте его расположения в контейнере, и этот контекст тоже можно выразить в виде него типа;

  • даже контравариантные конструкторы типов иногда можно трактовать, как рекурсивные ковариантные контейнеры;

  • вычисление типа контекста напоминает «деление с остатком», но следует привычным правилам вычисления производной;

  • лучше всего производные раскрываются именно для рекурсивных полиномиальных типов (деревьев).

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

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