Содержание второй части:
Другие части обзора
Откуда есть пошли типы рекурсивные
Конечно же нас больше интересует не исторический аспект, а причины, почему вообще можно захотеть получить рекурсивные типы.
В предыдущем разделе была алгоритмическая необходимость в повторении каких-либо действий. Мы вновь и вновь передавали результат предыдущих вычислений в ту же функцию. Но потребность в «повторении» может быть также обусловлена замоделированными типами.
Рассмотрим такой пример:
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])
В контексте исследования рекурсии, обобщённые типы удобно трактовать как конструкторы типов. Этот термин, пришедший из среды хаскелистов, отражает функциональную природу обобщённых типов (см., предыдущую статью), принимающих на вход одни типы и возвращающие новые. Вот, например, виды типов, представленных ранее:
где – это вид простого типа. Тип List_∞
определён в виде класса, а для OptCell
использован синтаксис -выражения третьей версии Scala – -исчисление (система 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, но у них просматриваются те же черты, что и у соответствующих типов во вселенной значений:
Любопытно, что концептуально FixF
без изменений транслирует вариантность базы рекурсии:
Здесь можно выбрать либо все верхние, либо все нижние знаки. К сожалению, 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]
удовлетворяет изоморфизму типов . Это означает, что между I
и F[I]
существуют две функции, действующие «туда и обратно», причём без потерь. В случае класса Fix
такой изоморфизм демонстрируют конструктор класса и проектор unfix
, но существуют и другие реализации неподвижной точки.
Выпишем тип одной из этих функций:
type Algebra[F[_]] = [X] =>> X => F[X] // Algebra: (⋆ → ⋆) → (⋆ → ⋆)
Название «алгебра» используется здесь из-за математических аналогий. По сути класс типов Algebra[F]
описывает преобразования закодированных в F[_]
комбинаций значений некоторого типа X
в него же. Например, функция типа представима в виде пары функций различной «арности»:
«Коалгеброй» же традиционно называется дуальное понятие, когда все стрелки обращены в обратную сторону.
Но в математике традиционно алгеброй называют не сам абстрактный набор операций 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 наименьшей неподвижной точкой для соответствует стандартный список List.
Из дополнительной литературы рекомендую статью PRIMITIVE RECURSION WITH FIX AND MU.
Наибольшая неподвижная точка
По аналогии с начальной F-алгеброй μ[F]
, в основе которой лежит концепция «распаковки» (свёртки) бесконечно-вложенного контейнера F[F[…∞…]]
, можно построить и дуальную неподвижную точку – конечную F-коалгебру, основанную на идее бесконечной «запаковки» (развёртки). Дуальность выражается несколько сложнее чем хотелось бы)). Если в обозначениях λ-исчисления наименьшая неподвижна точка записывается как
то наибольшая неподвижна точка будет такой:
«Существует такой тип 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, который представляет собой наибольшую неподвижную точку для .
Осталось выяснить, почему комбинаторы μ
и 𝛎
называются, соответственно «наименьшей» и «наибольшей» неподвижной точкой? Чем они отличаются и есть ли какие-то ещё «промежуточные» неподвижные точки?
Если в предыдущем примере кода убрать условие остановки, то можно получить коалгебру, порождающую «бесконечное» значение типа :
val factorial_∞ : 𝛎List[Int] = unfold𝛎[OptCell[Int]][(Int, Int)]( (n: Int, fact: Int) => Some(fact -> (n + 1, fact * (n + 1))) // никаких None! )(0 -> 1)
Благодаря ленивости такого значения, бесконечные вычисления всегда можно оборвать, указав условие остановки в алгебре, необходимой для свёртки этой структуры. Аналогичное значение для наименьшей неподвижной точки создать не получится – соответствующий этому значению тип неконструктивен! Более того, неподвижная точка для конструктора типов [X] =>> (Int, X)
представляет собой только бесконечный список. Его наименьшая неподвижная точка изоморфна нулевому типу: , так как такое значение просто невозможно создать. В этом смысле можно утверждать, что наименьшая неподвижная точка любого конструктора типов является подтипом для наибольшей: .
Бесконечные значения некоторых неподвижных точек могут иметь разную структуру (тип), делающую их неэквивалентными. Их типы даже могут быть вообще не сравнимыми – не для всех типов существует алгоритм, который за конечное число действий дал бы ответ об их возможной эквивалентности. Любой комбинатор неподвижной точки , включающий в себя бесконечный тип и будет носить статус «промежуточного»: . Причём, ввиду того, что бесконечные типы и в общем случае неэквивалентны, неподвижные точки и будут различными, но каждая из них окажется «больше» наименьшей, но «меньше» наибольшей.
Парочка интересных ситуаций
Конструктор типов Id[X] = X
обладает неподвижной точкой, содержащей вполне конструктивный бесконечный тип – да вообще любой тип является неподвижной точкой 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:
-
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]]
Зачастую, этого оказывается достаточно на практике. Но неподвижная точка конструктора типов, прежде всего, определяется изоморфизмом , который задаётся двумя функциями:
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). Но в этом обзоре мы обойдём их вниманием потому, что самые интересные случаи опираются на фундамент теории зависимых типов, а эту тему стоит раскрыть отдельно, как-нибудь в другой раз.
ссылка на оригинал статьи https://habr.com/ru/articles/863324/
Добавить комментарий