В статье « Функциональное программирование с перегрузкой и полиморфизмом высшего порядка » Марка П. Джонса обсуждаются рекурсия и фиксированные точки в разделе « Схемы рекурсии: функциональное программирование с бананами и линзами» со всеми примерами на Haskell. Этот документ отлично подходит для тех, кто интересуется общей концепцией функционального программирования. Если вы еще не прочитали это, прекратите читать этот пост и посмотрите на него.
В разделе о рекурсии в оригинальной статье обсуждаются фиксированные точки на уровне типа и способы ее использования для определения общих абстракций, таких как катаморфизм и анаморфизм., Они широко используются в универсальном программировании типов данных, где вы можете определить универсальные комбинаторы, параметризованные формой данных. Очень распространенный пример комбинатора, параметризованного конструктором формы или типа, — это fold , который работает со многими рекурсивными структурами, такими как List, Tree и т. Д.
Я пытался использовать Scala для создания тех же примеров, которые моделирует бумага в разделе о рекурсии. , Мне было любопытно узнать, достаточно ли выразительна система типов Scala для реализации абстракций более высокого порядка, таких как комбинатор точек фиксации на уровне типов, который статья реализует с использованием Haskell. Оливейра и Гиббонс также провели аналогичные исследованияо пригодности Scala для общего программирования типов данных и перевели ORIGAMI Гиббонов для подмножества шаблонов GoF в Scala.
Чтобы узнать точки привязки уровня типа, я начал с точек привязки уровня значения, используя нетипизированное лямбда-исчисление. Изучив свойства фиксированной точки для функций, вы сможете найти сопоставления с точками фиксированного уровня. В первом случае используются функции и типы карт, а во втором — конструкторы типов и виды карт.
Я начну с введения и некоторых доказательств для точек фиксации уровня стоимости. По большей части это довольно простые вещи — все же я хотел сказать эти вещи, так как это может оказаться полезным для того, кто изучает мой путь. Если вы знакомы с этим, не стесняйтесь переходить к следующему разделу.
Точка фиксации уровня
Лямбда-исчисление помогает нам разделить определение рекурсивной функции на 2 части — нерекурсивное вычислимое определение, которое абстрагирует рекурсивный вызов от дополнительного параметра, и оператор с фиксированной точкой, который кодирует рекурсивную часть. Таким образом, мы снимаем рекурсию с главной функции, которую мы моделируем. Вот обычный факториал, который проходит через этот процесс и приводит к вычислению с фиксированной запятой.
FACT = λn.IF (= n 0) 1 (* n (FACT (- n 1)))) // λ calculus FACT = (λfac (λn.IF (= n 0) 1 (* n (fac (- n 1)))))) FACT // beta abstraction
Обратите внимание, что здесь мы выделили основную факториальную функцию как абстракцию, не имеющую рекурсии. Назовите приведенное выше уравнение ..
FACT = H FACT
и это кодирует рекурсивную часть. H — это функция, которая при применении к FACT возвращает FACT. Мы называем FACT фиксированной точкой H.
Что же тогда является комбинатором фиксированной точки?
Комбинатор с фиксированной точкой — это функция Y, которая принимает в качестве аргумента другую функцию и генерирует ее. например, в случае выше Y при применении к H даст нам фиксированную точку FACT.
Y H = FACT // from definition of Y #1 FACT = H FACT // from above #2 Y H = H FACT // applying #2 in #1 #3 Y H = H (Y H) // applying #1 in #3 #4
Обратите внимание, что мы начали с FACT как модели нашего факториала. Это интересное упражнение, чтобы увидеть, что FACT 4 действительно приводит к 24, следуя приведенной выше формуле.
Таким образом, Y — это магия, которая помогает нам выразить любую рекурсивную функцию как нерекурсивное вычисление. Фактически Y может быть выражен как лямбда-выражение без использования рекурсии.
Y = (λh. (λx. h(x x)) (λx. h(x x)))
Давайте посмотрим, что оценивает YH ..
Y H = (λh. (λx. h(x x)) (λx. h(x x))) H // definition of Y -> (λx. H(x x)) (λx. H(x x)) // beta reduction -> H ((λx. H(x x)) (λx. H(x x))) // beta reduction -> H (Y H)
Так что это круто … мы успешно вывели Y комбинатор как лямбда-выражение.
Выше мы делали вывод комбинатора с фиксированной точкой для любой рекурсивной функции, которая является значением. Тема сегодняшнего поста — фиксированный комбинатор типов. Мы увидим, как вышеприведенные карты соответствуют одной и той же модели при применении на уровне типа.
Y для типов
В этом посте я буду моделировать комбинатор точек фиксации на уровне типов в Scala, показывая, что система типов Scala обладает способностью выражать все общие абстракции типов данных, которые Марк делает с помощью Haskell.
Вот что мы видели в качестве фиксированной точки для значений (функций).
Y H = H (Y H)
Комбинатор с фиксированной точкой для типов обычно называется Mu .. В Haskell мы будем говорить ..
data Mu f = In (f (Mu f))
Обратите внимание на соответствие … в то время как Y принимает функции и отображает разные типы, Mu принимает конструкторы типов и отображает разные виды.
GHCi> :t Y Y :: (a -> a) -> a GHCi> :k Mu Fix :: (* -> *) -> *
Теперь в Scala мы моделируем Mu как класс case, который принимает конструктор типа в качестве параметра. Как и в статье, мы рассматриваем только конструкторы унарных типов — это не так сложно обобщить на более высокие арности.
case class Mu[F[_]](out: F[Mu[F]])
Так же, как с фиксированной точкой уровня значения Y, мы можем изолировать рекурсивную функцию в нерекурсивное вычисление, мы можем сделать то же самое для типов с Mu. Рассмотрим следующую декларацию типа данных для моделирования натуральных чисел.
trait Nat case object Zero extends Nat case class Succ(n: Nat) extends Nat
.. рекурсивный тип .. давайте разберем рекурсию, введя дополнительный параметр типа ..
trait NatF[+S] case class Succ[+S](s: S) extends NatF[S] case object Zero extends NatF[Nothing] type Nat = Mu[NatF]
.. и моделирование фактического типа Nat в качестве фиксированной точки NatF.
Mu на самом деле является точкой фиксации функтора, что означает, что она работает на функторах (точнее, на ковариантных функторах). В нашем случае нам нужно определить функтор для NatF. Нет проблем … скаляр есть … а вот экземпляр функтора для NatF ..
implicit object functorNatF extends Functor[NatF] {
def fmap[A, B](r: NatF[A], f: A => B) = r match {
case Zero => Zero
case Succ(s) => Succ(f(s))
}
}
И мы определяем пару вспомогательных функций для нулевого натурального числа и функции-преемника.
def zero: Nat = Mu[NatF](Zero) def succ: Nat => Nat = (s: Nat) => Mu[NatF](Succ(s))
Что мы сделали с Mu
До сих пор мы определяли тип данных как точку привязки функтора. Вместо того, чтобы делать определение типа данных рекурсивным, мы абстрагировали рекурсию в комбинаторе с фиксированной точкой. И мы сделали все это как общую стратегию, которая может быть применена ко многим другим рекурсивным типам данных.
Давайте применим тот же шаблон к типу данных List. Хорошо, мы используем IntList, список целых чисел, следующий за документом.
trait IntListF[+S] case object Nil extends IntListF[Nothing] case class Cons[+S](x: Int, xs: S) extends IntListF[S] // the integer list as a fixpoint of IntListF type IntList = Mu[IntListF] // convenience functions for the constructors def nil = Mu[IntListF](Nil) def cons = (x: Int) => (xs: IntList) => Mu[IntListF](Cons(x, xs))
.. и экземпляр функтора ..
implicit object functorIntListF extends Functor[IntListF] {
def fmap[A, B](r: IntListF[A], f: A => B) = r match {
case Nil => Nil
case Cons(n, x) => Cons(n, f(x))
}
}
Обратите внимание на сходство в структуре обоих типов данных Nat и IntList, а также на то, как конструкторы типов в обоих случаях IntListF и NatF определяют форму вычисления для соответствующих типов данных. Это означает, что определение типа данных параметризовано конструктором типа, который определяет форму данных, которые будут моделироваться типом данных.
А теперь для ката.
Теперь, имея указанную выше абстракцию Mu, мы можем определить комбинатор, который может показаться более обобщенным, чем складка … это катаморфизм, который мы определяем как …
def cata[A, F[_]](f: F[A] => A)(t: Mu[F])(implicit fc: Functor[F]): A = {
f(fc.fmap(t.out, cata[A, F](f)))
}
Для рекурсивных типов данных сгибы будут иметь разные типы, но cata — это более общая абстракция, способная определять все операции с типом данных. Ката похожа на фолд, просто более общая. Подпись сгиба зависит от типа данных, к которым она применяется. Но приведенное выше определение cata достаточно универсально для моделирования функций конструкторов типов, для которых есть соответствующий экземпляр функтора.
В этом посте Тони Моррис обсуждает катаморфизм в типе данных Option в Scala. Он определяет данные, специфичные для этого типа данных. Вышеупомянутое определение находится на более высоком уровне абстракции и параметризовано в форме данных, которые оно принимает. Следующие фрагменты используют одни и те же данные для определения функций для Nat, а также для IntList. Тип данных общих абстракций FTW.
Взгляните на следующие функции Nat, все они определены в терминах комбинатора cata:
def fromNat = cata[Int, NatF] {
case Zero => 0
case Succ(n) => 1 + n
} _
scala> fromNat(succ(succ(zero)))
res14: Int = 2
def addNat(m: Nat, n: Nat) = cata[Nat, NatF] {
case Zero => m
case Succ(x) => succ(x)
} (n)
scala> fromNat(addNat(succ(zero), succ(zero)))
res15: Int = 2
scala> fromNat(addNat(succ(zero), succ(succ(zero))))
res16: Int = 3
def mulNat(m: Nat, n: Nat) = cata[Nat, NatF] {
case Zero => zero
case Succ(x) => addNat(m, x)
} (n)
scala> fromNat(mulNat(succ(succ(succ(zero))), succ(succ(zero))))
res1: Int = 6
scala> fromNat(mulNat(succ(succ(succ(zero))), zero))
res2: Int = 0
def expNat(m: Nat, n: Nat) = cata[Nat, NatF] {
case Zero => succ(zero)
case Succ(x) => mulNat(m, x)
} (n)
scala> fromNat(expNat(succ(succ(succ(zero))), zero))
res0: Int = 1
scala> fromNat(expNat(succ(succ(succ(zero))), succ(succ(zero))))
res1: Int = 9
.. и еще немного о IntList с использованием того же самого ката ..
def sumList = cata[Int, IntListF] {
case Nil => 0
case Cons(x, n) => x + n
} _
scala> sumList(cons(1)(cons(2)(cons(3)(nil))))
res1: Int = 6
def len = cata[Nat, IntListF] {
case Nil => zero
case Cons(x, xs) => succ(xs)
} _
scala> fromNat(len(cons(1)(cons(2)(cons(3)(nil)))))
res1: Int = 3
С http://debasishg.blogspot.com/2011/07/datatype-generic-programming-in-scala.html