Рекурсивные типы. Часть 2/5. Неподвижные точки конструкторов типов / forpes.ru

Главная
Рекурсивные типы. Часть 2/5. Неподвижные точки конструкторов типов

Рекурсивные типы. Часть 2/5. Неподвижные точки конструкторов типов +6

05.12.2024 07:07

Underskyer1 0 901 Источник

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

Откуда есть пошли типы рекурсивные
Неподвижные точки конструкторов типов
Начальная F-алгебра
Наибольшая неподвижная точка
Классы типов неподвижных точек
Промежуточный итог

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

Откуда есть пошли типы рекурсивные

Конечно же нас больше интересует не исторический аспект, а причины, почему вообще можно захотеть получить рекурсивные типы.

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

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

type OptCell = [A] =>> [X] =>> Option[(A, X)] // 1 + A × X

type List3 = [A] =>> OptCell[A][OptCell[A][OptCell[A][Unit]]]
//   List3 = 1 + A × (1 + A × (1 + A × 1)) ≅ 1 + A + A × A + A × A × A

val lst3: List3[Int] = Some(1, Some(2, Some(3, ()))) // (1, 2, 3)

Тип List3 построен из трёх одинаковых «опциональных ячеек» и представляет собой сумму списков длинны 0, 1, 2 и 3. Переменная lst3 содержит список максимальной длинны 3.

Вот как можно реализовать свёртку таких списков:

def foldList3[A, B](b: B, comb: (A, B) => B) = (lst: List3[A]) =>
  lst match
    case None => b
    case Some(a: A, x) =>
      val acc1 = comb(a, b)
      x match
        case None => acc1
        case Some(a, x) =>
          val acc2 = comb(a, acc1)
          x match
            case None => acc2
            case Some(a, _) => comb(a, acc2)

val foldToString = foldList3("foldList3: ", (i: Int, s: String) => s + i + " ")
foldToString(lst3) // "foldList3: 1 2 3"

Бросается в глаза троекратное (ну, почти) повторение кода в теле foldList3, завязанное на структуре List3, скомпонованной из трёх OptCell. Напрашивается использование рекурсии – она позволила бы сворачивать списки без ограничений на их длину. Но тогда нужно сформулировать тип List_∞, который был бы изоморфен сумме типов списков всевозможных длин. Вот одна из реализаций этого типа:

case class List_∞[A](cell: OptCell[A][List_∞[A]])

Класс List_∞ ссылается сам на себя аналогично тому, как это было с рекурсивными функциями.

Как и ожидалось, свёртка также будет рекурсивной:

def foldList_∞[A, B](lst: List_∞[A], b: B, comb: (A, B) => B): B =
  lst.cell match
    case None             => b
    case Some(head, tail) => foldList_∞(tail, comb(head, b), comb)
    //                         ↑↑↑↑↑↑↑↑↑↑ - вызов себя же
val lst4 = List_∞(Some(1, List_∞(Some(2, List_∞(Some(3, List_∞(Some(4, List_∞(None)))))))))

foldList_∞(lst4, "foldList_∞: ", (i: Int, s: String) => s + i + " ")
// foldList_∞: 1 2 3 4

И, само собой, рекурсию из свёртки можно вынести в комбинатор неподвижной точки:

type FoldIterState[A, B] = (List_∞[A], B, (A, B) => B)
type FoldFunc[A, B] = FoldIterState[A, B] => B

def foldListBase[A, B]: FoldFunc[A, B] => FoldFunc[A, B] =
  self => (lst, b, comb) =>
  lst.cell match
    case None             => b
    case Some(head, tail) => self(tail, comb(head, b), comb)

def foldList[A, B] = fix(foldListBase[A, B])

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

$\begin{split}OptCell[A] &: \star \rightarrow \star,\\List_\infty[A] &: \star,\\\end{split}$

где $\star$ – это вид простого типа. Тип List_∞ определён в виде класса, а для OptCell использован синтаксис $\lambda$ -выражения третьей версии Scala – $\lambda$ -исчисление (система Fω) работает и на уровне типов!

Такая «функциональная» трактовка обобщённых типов позволяет применять к ним те же рассуждения, которые использовались ранее при рассмотрении рекурсивных функций. Например, класс List_∞ в определении ссылается сам на себя так же, как и рекурсивные методы могут вызывать себя же. Кстати, наивная попытка определить такой тип через псевдоним приведёт к ошибке компиляции:

type List_∞ = [A] =>> OptCell[A][List_∞[A]] // ОШИБКА КОМПИЛЯЦИИ
// illegal cyclic type reference: alias ... of type Lst_∞ refers back to the type itself

В появившемся в Scala 3 механизме сопоставления типов с шаблонами они реализовали поддержку прямой рекурсии в псевдонимах типов, хотя и там не обошлось без нелепых ограничений…

Помимо привычных ссылок на ещё не определённые типы, любые рекурсивные типы можно реализовать в Scala через неподвижные точки конструкторов типов. Но в отличие от обычных функций, во вселенной типов дополнительно проявляются интересные особенности. Рассмотрим их далее.

Неподвижные точки конструкторов типов

Прямым аналогом комбинатора неподвижной точки fix: (A => A) => A, но во вселенной типов будет такой класс:

case class Fix[F[_]](val: F[Fix[F]]) // Fix: (⋆ → ⋆) → ⋆

Класс Fix описывает бесконечную цепочку применения переданного ему конструктора типов F[_] к самому себе: F[F[F[…∞…]]]. Например, всё тот же тип списка вот так можно переписать с помощью Fix:

type List[A] = Fix[OptCell[A]]
val list: List[Int] = Fix(Some(1, Fix(Some(2, Fix(Some(3, Fix(None))))))) // (1, 2, 3)

И, аналогично усложнённому комбинатору fixf, на уровне типов можно записать такой вариант:

case class FixF[RecBase[_[_], _], A](v: RecBase[[X] =>> FixF[RecBase, X], A])

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

type TreeBase = [Self[_], A] =>> Option[(A, Self[A], Self[A])]
type Tree     = [A]          =>> FixF[TreeBase, A]

val ∅   : Tree[Nothing] = FixF(None)
val tree: Tree[Int]     = FixF(Some(4, ∅, FixF(Some(2, ∅, ∅)))) //    4
//                                                                   /  \
//                                                                  ∅    2
//                                                                      /  \
//                                                                     ∅    ∅

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

$\begin{split}TreeBase:&\,\,\,\, (\star \rightarrow \star,\; \star) \rightarrow \star \;\;&&\cong\,\,\,\,(\star \rightarrow \star) \rightarrow (\star \rightarrow \star)\\FixF:&\; ((\star \rightarrow \star,\; \star) \rightarrow \star,\; \star) \rightarrow \star \;\;&&\cong\;((\star \rightarrow \star) \rightarrow (\star \rightarrow \star)) \rightarrow (\star \rightarrow \star)\\\end{split}$

Любопытно, что концептуально FixF без изменений транслирует вариантность базы рекурсии:

$\begin{split}FixF&:&((\pm\star \rightarrow \star) \rightarrow (\pm\star \rightarrow \star)) \rightarrow (\pm\star \rightarrow \star)\\\end{split}$

Здесь можно выбрать либо все верхние, либо все нижние знаки. К сожалению, Scala не поддерживает проброс вариантности, но не сложно самостоятельно расставить нужные знаки перед типами-параметрами. Предыдущий пример с TreeBase показывает, что и у Self, и у параметровFixF можно везде проставить знак +, фиксируя ковариантность. А вот с контравариантными конструкторами типов ситуация интереснее:

case class FixContra[RecBase[_[-_], -_], -A](v: RecBase[[X] =>> FixContra[RecBase, X], A])
type WtfBase = [Self[-_], A] =>> Option[Self[Self[A]]] => String
type Wtf[A]  = FixContra[WtfBase, A] // ↑↑↑↑-↑↑↑↑ - хитрость для соблюдения вариантности))

val wtf: Wtf[Int] = opt => ???
//                  ↑↑↑ - ошибка! тип невозможно нормализовать!!!

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

Но не только контравариантные (+инвариантные) обобщённые типы имеют неконструктивные неподвижные точки. Вот ещё пример:

type ContStr[+A] = (A => String) => String
type ContRec = Fix[ContStr]
val  contRec: ContRec = Fix((f: Fix[ContStr] => String) => ???)
//                     что можно сделать с этим значением? ↑↑↑

Не смотря на то, что этот тип ContStr ковариантный, тут тоже возникают проблемы со значениями его неподвижной точки. Тип аргумента f вполне нормализуется, но во что можно с ним сделать? Внезапно оказывается, что вызвать функцию f: Fix[ContStr] => String от какого-либо честно типизированного значения невозможно! Попытка приведёт бесконечной цепочке вызовов тех же Fix, что и при определении переменной contRec. Конечно, в арсенале программистов есть разные «читерские» способы, вроде метода toString, применимого к термам любого типа, но все они лишь подчеркнут бесполезность применения рекурсии к такому конструктору типов.

В итоге получаем такое правило:

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

Начальная F-алгебра

Неподвижная точка I = Fix[F] удовлетворяет изоморфизму типов $F[I] \cong I$ . Это означает, что между I и F[I] существуют две функции, действующие «туда и обратно», причём без потерь. В случае класса Fix такой изоморфизм демонстрируют конструктор класса и проектор unfix, но существуют и другие реализации неподвижной точки.

Выпишем тип одной из этих функций:

type Algebra[F[_]] = [X] =>> X => F[X] // Algebra: (⋆ → ⋆) → (⋆ → ⋆)

Название «алгебра» используется здесь из-за математических аналогий. По сути класс типов Algebra[F] описывает преобразования закодированных в F[_] комбинаций значений некоторого типа X в него же. Например, функция типа $Algebra[OptCell[X]][X] \cong 1 + X \times X \Rightarrow X$ представима в виде пары функций различной «арности»:

$\begin{split}&zero:\; 1 (= X^0) \Rightarrow X;\;\; &- \;\;\text{нулярная операция (слева 0 значений типа X),}\\&cobm: X \times X (= X^2) \Rightarrow X\;\; &- \;\;\text{бинарная операция (слева 2 значения типа X).}\end{split}$

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

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

type μ[F[_]] = [X] => Algebra[F][X] => X // μ[F[_]] = Algebra[F] ~> Id

Прилагательное «начальный» позаимствовано из теории категорий. В данном случае оно подразумевает, что из значений начальной алгебры μ[F], всегда можно получить любую другую алгебру X, если, конечно, предоставить экземпляр класса типа Algebra[F][X]. Для различных реализаций наименьшей неподвижной точки принято использовать функцию «свёртки» (fold), подразумевающую сворачивание бесконечной структуры данных F[F[…∞…]] до значения «простого» типа:

def foldμ[F[_]]: [X] => Algebra[F][X] => μ[F] => X =
  [X] => (alg: Algebra[F][X]) => (μF: μ[F]) => μF(alg)

Покажем, что μ[F] является неподвижной точкой для F[_], то есть, что типы μ[F] и F[μ[F]] изоморфны. Сперва придётся явно предоставить доказательство ковариантности F[+_] – сделаем это посредством класса типов Lift (см. предыдущую статью):

type Lift[F[_]] = [A, B] => (A => B) => (F[A] => F[B])
def fmap[F[_] : Lift] = summon[Lift[F]]
extension [F[_]: Lift, A](fa: F[A])
  def map[B] = (f: A => B) => fmap(f)(fa)

Тогда искомый изоморфизм составляют такие реализации Algebra[F][μ[F]] и Coalgebra[F][μ[F]] (обе их композиции дают тождественную функцию):

def inμ [F[_]: Lift]:   Algebra[F][μ[F]] = fμF => [X] => (alg: Algebra[F][X]) => alg(fmap(foldμ(alg))(fμF))
def outμ[F[_]: Lift]: Coalgebra[F][μ[F]] = foldμ(fmap(inμ))

Сформулируем с помощью μ тип списка по аналогии с тем, как мы это делали с Fix, и определим конструкторы nil и cons:

type List[X] = μ[OptCell[X]]

given [X]: Lift[OptCell[X]] = // доказаетльство ковариантности OptCell[X]: ⋆ → ⋆
  [A, B] => (f: A => B) => (optCell: OptCell[X][A]) =>
    optCell map {case (x, a) => (x, f(a))}

def nil [A]                         : μList[A] = inμ(None            )	
def cons[A](head: A, tail: μList[A]): μList[A] = inμ(Some(head, tail))

Работа с таким представлением списка требует указания конкретной алгебры:

def lst: List[Int] = cons(1, cons(2, cons(3, nil)))

def   listAlgebra[A]: Algebra[OptCell[A  ]][List[A]] = _.fold( Nil )((h, t) => h :: t)
val stringAlgebra   : Algebra[OptCell[Int]][String ] = _.fold("nil")((i, s) => s"$i, $s")

foldμ(  listAlgebra)(lst) // List(1, 2, 3)
foldμ(stringAlgebra)(lst) //     "1, 2, 3, nil"

Не удивительно, что неподвижные точки Fix[F] и μ[F] оказываются изоморфными:

def туда[F[_]: Lift]: Fix[F] => μ[F] =
  fixf => [X] => (alg: F[X] => X) =>
    alg(fmap(
      туда(_: Fix[F])(alg))( // приходится подсказывать тип компилятору
      fixf.unfix
    ))
def обратно[F[_]: Lift]: μ[F] => Fix[F] = foldμ(Fix.apply)

assert((туда    andThen обратно)(fixList)            == fixList)            // для любых fixList: Fix[OptCell]
assert((обратно andThen туда   )(μList)(listAlgebra) == μList(listAlgebra)) // для любых   μList:   μ[OptCell]

Пара функций туда/обратно, вместе с утверждением, что их композиция образует отображение идентичности, и образуют искомый изоморфизм.

Кстати, тип функции-комбинатора неподвижной точки также можно выразить через μ[_[_]]:

def unsafeFix: μ[Id] =
  [A] => (f: A => A) => f(fix(f)) // переполнит стек!

Комбинатор μ (и изоморфный ему Fix) называют также наименьшей неподвижной точкой контейнера F[_]. Суть «наименьшести» раскроем далее, сравнив с другими неподвижными точками. Сейчас же важно заметить на примере конструкторов nil и cons типа List[A] = μ[OptCell[A]], что новые значения создаются только путём «расширения» значений поменьше за счёт «прирастания» новых данных. Это означает, что все такие списки будут конечными. Во встроенной библиотеке Scala наименьшей неподвижной точкой для $OptCell[A][X] = 1 + A \times X$ соответствует стандартный список List.

Из дополнительной литературы рекомендую статью PRIMITIVE RECURSION WITH FIX AND MU.

Наибольшая неподвижная точка

По аналогии с начальной F-алгеброй μ[F], в основе которой лежит концепция «распаковки» (свёртки) бесконечно-вложенного контейнера F[F[…∞…]], можно построить и дуальную неподвижную точку – конечную F-коалгебру, основанную на идее бесконечной «запаковки» (развёртки). Дуальность выражается несколько сложнее чем хотелось бы)). Если в обозначениях λ-исчисления наименьшая неподвижна точка записывается как

$\mu\, F = \forall X. (F[X] \rightarrow X) \rightarrow X$

то наибольшая неподвижна точка будет такой:

$\nu\, F = \exists X. (X \rightarrow F[X]) \times X$

«Существует такой тип X, для которого задано значение X и функция из X в F[X]». Тип этой функции обычно оформляют в класс типов Coalgebra[F] – дуально Algebra[F]. Значения типа X и его класса типов Coalgebra[F][X] образуют пару, необходимую для «ленивого» (отложенного) вычисления F[X].

type Coalgebra[F[_]] = [X] =>> X => F[X]            // Coalgebra: (⋆ → ⋆) → (⋆ → ⋆)
type LazyFx   [F[_]] = [X] =>> (X, Coalgebra[F][X]) // LazyFx   : (⋆ → ⋆) → (⋆ → ⋆)

def eval[F[_], X]: LazyFx[F][X] => F[X] =           // отложенная «оценка» коалгебры
  case (x, coalgebra) => coalgebra(x)

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

trait Existential[F[_]] { type T; val value: F[T] }
type ?[F[_]] = Existential[LazyFx[F]] // ?: (⋆ → ⋆) → ⋆

Конечной F-коалгеброй этот тип называется потому, что её можно получить из любой другой коалгебры – значения типа X и экземпляра класса типов Coalgebra[F][X] (то бишь, из значения LazyFx[F][X]). Такая операция называется «развёрткой»:

def unfold?[F[_]]: [X] => LazyFx[F][X] => ?[F] =
  [X] => (coalg: Coalgebra[F][X]) => (x: X) =>
    new Existential[LazyFx[F]]:
      type T = X
      val value = LazyFx(x, coalg)

Ленивость носителя коалгебры LazyFx[F] определяет назначение ? – этот тип описывает рекурсивное «развёртывание» некой структуры данных согласно заданному алгоритму. Такой процесс иногда называют «корекурсией», а структуру, описываемую наибольшей неподвижной точкой – «коданными»

Неподвижность F относительно ?[F] доказывается следующим изоморфизмом:

def out?[F[_]: Lift]: Coalgebra[F][?[F]] =  ?F => fmap((x: ?F.T) => unfold?(?F.value.coalgebra)(x))(?F.value.eval)
def  in?[F[_]: Lift]:   Algebra[F][?[F]] = f?F => unfold?(fmap(out?))(f?F)

assert((out? andThen  in?)( ?F) ==  ?F) // для любых  ?F:   ?[F]
assert(( in? andThen out?)(f?F) == f?F) // для любых f?F: F[?[F]]

Рассмотрим пример использования ?[F] на всё том же F[_] = OptCell[A][_]. Развернём список факториалов:

type ?List[A] = ?[OptCell[A]]

val factCoalg10: Coalgebra[OptCell[Int]][(Int, Int)] =
  case (n: Int, fact: Int) => // функция преобразования состояния
    Option.when(n <= 10)(     // ограничение на размер (может отсутствовать!)
      fact,                   // промежуточное состояние
      (n + 1, fact * (n + 1)) // состояние для следующей итерации
    )

val factorial10: ?List[Int] =
  unfold?[OptCell[Int]](factCoalg10)(0, 1)
//↑↑↑↑↑↑                ↑↑↑↑↑↑↑↑↑↑↑  ↑↑↑↑↑↑
//развёртка              коалгебра   начальное состояние (0! = 1)

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

def fold?[F[_]: Lift, X](alg: Algebra[F][X]): ?[F] => X =
  ?F => alg(fmap(fold?(alg))(out?(?F)))

fold?(  listAlgebra)(factorial10) // List(1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800)
fold?(stringAlgebra)(factorial10) //     "1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800, nil"

В Scala есть встроенный тип LazyList, который представляет собой наибольшую неподвижную точку для $OptCell[A][X] = 1 + A \times X$ .

Осталось выяснить, почему комбинаторы μ и ? называются, соответственно «наименьшей» и «наибольшей» неподвижной точкой? Чем они отличаются и есть ли какие-то ещё «промежуточные» неподвижные точки?

Если в предыдущем примере кода убрать условие остановки, то можно получить коалгебру, порождающую «бесконечное» значение типа $F[F[\ldots\infty\ldots]]$ :

val factorial_∞ : ?List[Int] =
  unfold?[OptCell[Int]][(Int, Int)](
    (n: Int, fact: Int) => Some(fact -> (n + 1, fact * (n + 1))) // никаких None!
  )(0 -> 1)

Благодаря ленивости такого значения, бесконечные вычисления всегда можно оборвать, указав условие остановки в алгебре, необходимой для свёртки этой структуры. Аналогичное значение для наименьшей неподвижной точки создать не получится – соответствующий этому значению тип $F[F[\ldots\infty\ldots]]$ неконструктивен! Более того, неподвижная точка для конструктора типов [X] =>> (Int, X) представляет собой только бесконечный список. Его наименьшая неподвижная точка изоморфна нулевому типу: $\mu[(Int,\, \_)] \cong Nothing$ , так как такое значение просто невозможно создать. В этом смысле можно утверждать, что наименьшая неподвижная точка любого конструктора типов является подтипом для наибольшей: $\mu[F] <: \nu[F]$ .

Бесконечные значения некоторых неподвижных точек могут иметь разную структуру (тип), делающую их неэквивалентными. Их типы даже могут быть вообще не сравнимыми – не для всех типов существует алгоритм, который за конечное число действий дал бы ответ об их возможной эквивалентности. Любой комбинатор неподвижной точки fix_i[F] , включающий в себя бесконечный тип fixF_i и будет носить статус «промежуточного»: $\mu[F] <: fix_i[F] <: \nu[F]$ . Причём, ввиду того, что бесконечные типы fixF_i и fixF_j в общем случае неэквивалентны, неподвижные точки и fix_j[F] будут различными, но каждая из них окажется «больше» наименьшей, но «меньше» наибольшей.

Парочка интересных ситуаций

Конструктор типов Id[X] = X обладает неподвижной точкой, содержащей вполне конструктивный бесконечный тип $Id[Id[\ldots\infty\ldots]]$ – да вообще любой тип является неподвижной точкой Id. Но возможны и менее тривиальные случаи. Например, сопоставление типов с шаблонами в Scala 3 позволяет построить и такие конструкторы типов, которые имеют единственную тривиальную неподвижную точку Nothing:

type Semaphore[X] = X match
  case Unit    => Boolean
  case Boolean => Unit

Тем не менее, принято считать, что все неподвижные точки некого конструктора типов изоморфны друг другу. Смысл в том, что работая с конструкторами и изоморфизмами неподвижных точек мы имеем дело с частично-определёнными рекурсивными функциями. Напомню, две такие функции считаются эквивалентными, если они для одних и тех же аргументов либо возвращают одинаковые значения, либо обе расходятся. В нашем же случае для «бесконечных» значений типа ?[F] расходится будут как fold?, так и конструктор соответствующего значения типа μ[F]. Другими словами, в изоморфизмах неподвижных точек бесконечные значения вообще исключаются из рассмотрения, как неконструктивные.

Изоморфизм между ?[F] и μ[F] строится так:

def туда   : ?[F] => μ[F] =   fold?( inμ)
def обратно: μ[F] => ?[F] = unfold?(outμ)

И всё же, несмотря на изоморфность, типы ?[F] и μ[F] обладают разными возможностями. Они представляют два диаметрально противоположных подхода для работы с рекурсивными типами – развертывание структуры данных и её сворачивание. Рассмотрим их в следующем разделе.

Дополнительная литература:

пара вопросов на StackOverflow:
- Least fix point, greatest fix point;
- What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package;
Recursive types for free! – статья лямбда-мена Филиппа Водлера;
RECURSIVE DATA TYPES – 5 часть из книги INTRODUCTION TO TYPES;

Классы типов неподвижных точек

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

type   Fold[Fix[_[_]]] = [F[_]] => Lift[F] ?=> [X] =>  Algebra[F][X]  => Fix[F] =>     X
type Unfold[Fix[_[_]]] = [F[_]] => Lift[F] ?=> [X] => Coalgebra[F][X] =>     X  => Fix[F]

def    fold[Fix[_[_]]:   Fold] = summon[  Fold[Fix]]
def  unfold[Fix[_[_]]: Unfold] = summon[Unfold[Fix]]

Зачастую, этого оказывается достаточно на практике. Но неподвижная точка конструктора типов, прежде всего, определяется изоморфизмом $F[Fix[F]] \cong Fix[F]$ , который задаётся двумя функциями:

type  InFix[Fix[_[_]]] =   Fold[Fix] ?=> [F[_]] => Lift[F] ?=>   Algebra[F][Fix[F]]
type OutFix[Fix[_[_]]] = Unfold[Fix] ?=> [F[_]] => Lift[F] ?=> Coalgebra[F][Fix[F]]

def   inFix[Fix[_[_]]:  InFix:   Fold, F[_]: Lift]:   Algebra[F][Fix[F]] = summon[ InFix[Fix]][F]
def  outFix[Fix[_[_]]: OutFix: Unfold, F[_]: Lift]: Coalgebra[F][Fix[F]] = summon[OutFix[Fix]][F]

И можно даже собрать четыре эти функции в единый класс типов вида

trait FixedPoint[Fix[_[_]]]:
  def   fold[F[_]]: [X] =>   Algebra[F][X] => Fix[F] =>     X
  def unfold[F[_]]: [X] => Coalgebra[F][X] =>     X  => Fix[F]
  def     in[F[_]: Lift]:    Algebra[F][Fix[F]]
  def    out[F[_]: Lift]:  Coalgebra[F][Fix[F]]

однако, две из них всегда можно выразить через две другие. Из пары (fold, in) можно получить пару (unfold, out) и наоборот! выразим это в виде следующих неявных значений:

given unfoldFromFold[Fix[_[_]]: InFix: Fold]: Unfold[Fix] =
  [F[_]] => (_: Lift[F]) ?=> [X] => (coalg: Coalgebra[F][X]) => (x: X) =>
    inFix(fmap(unfoldFromFold(coalg))(coalg(x)))

given foldFromUnfold[Fix[_[_]]: OutFix: Unfold]: Fold[Fix] =
  [F[_]] => (_: Lift[F]) ?=> [X] => (alg: Algebra[F][X]) => (fixF: Fix[F]) =>
    alg(fmap(foldFromUnfold(alg))(outFix(fixF)))

given outFromIn[Fix[_[_]]:  InFix:   Fold, F[_]: Lift]: Coalgebra[F][Fix[F]] =   foldFix(fmap( inFix))
given inFromOut[Fix[_[_]]: OutFix: Unfold, F[_]: Lift]:   Algebra[F][Fix[F]] = unfoldFix(fmap(outFix))

Вот как эти классы типов можно использовать, например, с введённой ранее неподвижной точкой μ:

given Fold[μ] =
  [F[_]] => (_: Lift[F]) ?=> [X] => (alg: Algebra[F][X]) => (fixf: μ[F]) =>
    fixf(alg)

given InFix[μ] =
  [F[_]] => (_: Lift[F]) ?=> (fμF: F[μ[F]]) => [X] => (alg: Algebra[F][X]) =>
    alg(fmap(foldFix(alg))(fμF))

val μfactorial10: μList[Int] = unfoldFix[μ](factCoalg10)(0, 1)
foldFix(stringAlgebra)(μfactorial10) // 1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800, nil

Здесь возможность «развёртки» была выведена автоматически, благодаря неявному значению unfoldFromFold.

В популярных библиотеках вроде Matryoshka возможности Fold и InFix объединяют в один класс типов Recursive[Fix[_[_]]], тогда как Unfold и OutFix – в Corecursive[Fix[_[_]]]. В эти классах типов сгруппированы также дополнительные возможности свёртки/развёртки, о которых расскажем в следующем разделе. Но помимо прочего, в них используются зависимые типы, что позволяет обогащать даже произвольные необобщённые рекурсивные типы.

Промежуточный итог

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

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