Подтвердить что ты не робот

Что представляет собой складку для других типов, кроме списка?

Рассмотрим односвязный список. Это похоже на

data List x = Node x (List x) | End

Естественно определить функцию складывания, такую ​​как

reduce :: (x -> y -> y) -> y -> List x -> y

В некотором смысле reduce f x0 заменяет каждый Node на f и каждый End на x0. Это то, что прелюдия называется складкой.

Теперь рассмотрим простое двоичное дерево:

data Tree x = Leaf x | Branch (Tree x) (Tree x)

Аналогично естественно определить такую ​​функцию, как

reduce :: (y -> y -> y) -> (x -> y) -> Tree x -> y

Обратите внимание, что это сокращение имеет совершенно другой характер; в то время как основанный на списках по сути является последовательным, этот новый, основанный на дереве, имеет больше чувства разделения и покоя. Вы даже можете себе представить, как добавить туда комбинаторов par. (Где бы вы поместили такую ​​вещь в версию списка?)

Мой вопрос: эта функция по-прежнему классифицируется как "складка", или это что-то еще? (И если да, что это?)

В принципе, всякий раз, когда кто-то говорит о сворачивании, они всегда говорят о сворачивающихся списках, который по своей сути является последовательным. Мне интересно, является ли "последовательный" частью определения того, что такое сгиб, или это просто совпадающее свойство наиболее часто используемого примера сгибания.

4b9b3361

Ответ 1

Тихон свалил технические вещи. Я думаю, что я постараюсь упростить то, что он сказал.

К сожалению, термин "складывание" с годами стал неоднозначным и означает одно из двух:

  1. Сокращение коллекции последовательно в некотором порядке. В Haskell, это то, что "складной" означает в Foldable классе, который larsmans воспитывает.
  2. Понятие, которое вы просили: "уничтожать" (противоположно построению), "наблюдать" или "исключать" алгебраический тип данных в соответствии с его структурой. Также называется катаморфизмом.

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

Но чаще всего весь путь с Fix и алгебрами и тому подобным является излишним. Давайте разработаем более простой способ написания сгиба для любого алгебраического типа данных. В качестве примеров мы будем использовать Maybe, пары, списки и деревья:

data Maybe a = Nothing | Just a
data Pair a b = Pair a b
data List a = Nil | Cons a (List a)
data Tree x = Leaf x | Branch (Tree x) (Tree x)
data BTree a = Empty | Node a (BTree a) (BTree a)

Обратите внимание, что Pair не является рекурсивным; процедура, которую я собираюсь показать, не предполагает, что "сложенный" тип является рекурсивным. Люди обычно не называют этот случай "сгибом", но на самом деле это нерекурсивный случай с той же концепцией.

Первый шаг: сгиб для данного типа будет использовать свернутый тип и в качестве результата выдаст некоторый тип параметра. Мне нравится называть последний r (для "результата"). Так:

foldMaybe :: ... -> Maybe a -> r
foldPair  :: ... -> Pair a b -> r
foldList  :: ... -> List a -> r
foldTree  :: ... -> Tree a -> r
foldBTree :: ... -> BTree a -> r

Второй шаг: в дополнение к последнему аргументу (тот, что для структуры), сгиб принимает столько аргументов, сколько у типа есть конструкторы. Pair есть один конструктор, а у других примеров - два, поэтому:

foldMaybe :: nothing -> just -> Maybe a -> r
foldPair  :: pair -> Pair a b -> r 
foldList  :: nil -> cons -> List a -> r
foldTree  :: leaf -> branch -> Tree a -> r
foldBTree :: empty -> node -> BTree a -> r

Третий шаг: каждый из этих аргументов имеет ту же арность, что и конструктор, которому он соответствует. Давайте рассматривать конструкторы как функции и записывать их типы (убедившись, что переменные типа совпадают с теми, что в сигнатурах, которые мы пишем):

Nothing :: Maybe a
Just    :: a -> Maybe a

Pair    :: a -> b -> Pair a b

Nil     :: List a
Cons    :: a -> List a -> List a

Leaf    :: a -> Tree a
Branch  :: Tree a -> Tree a -> Tree a

Empty   :: BTree a
Node    :: a -> BTree a -> BTree a -> BTree a

Шаг 4: в сигнатуре каждого конструктора мы заменим все вхождения создаваемого им типа данных нашей переменной типа r (которую мы используем в наших сигнатурах сгиба):

nothing := r
just    := a -> r

pair    := a -> b -> r

nil     := r
cons    := a -> r -> r

leaf    := a -> r
branch  := r -> r -> r

empty   := r
node    := a -> r -> r -> r

Как вы можете видеть, я "назначил" полученные сигнатуры переменным фиктивного типа со второго шага. Теперь Шаг 5: заполните их в более ранних подписях сгиба эскиза:

foldMaybe :: r -> (a -> r) -> Maybe a -> r
foldPair  :: (a -> b -> r) -> Pair a b -> r 
foldList  :: r -> (a -> r -> r) -> List a -> r
foldTree  :: (a -> r) -> (r -> r -> r) -> Tree a -> r
foldBTree :: r -> (a -> r -> r -> r) -> BTree a -> r

Теперь это подписи для складок этих типов. Они имеют забавную порядок аргументов, потому что я сделал это механически, читая складку типа Офф- data деклараций и типов конструктора, но по какой - то причине в функциональном программировании обычного поставить базовые случаи первыми в data определениях еще рекурсивные обработчик регистра первыми в fold определениях, Нет проблем! Давайте перетасуем их, чтобы сделать их более обычными:

foldMaybe :: (a -> r) -> r -> Maybe a -> r
foldPair  :: (a -> b -> r) -> Pair a b -> r 
foldList  :: (a -> r -> r) -> r -> List a -> r
foldTree  :: (r -> r -> r) -> (a -> r) -> Tree a -> r
foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r

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

Начнем так:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
foldBTree = ???

Мы знаем, что требуется три аргумента, поэтому мы можем добавить переменные для их отражения. Я буду использовать длинные описательные имена:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
foldBTree branch empty tree = ???

Глядя на объявление data, мы знаем, что у BTree есть два возможных конструктора. Мы можем разделить определение на случай для каждого и заполнить переменные для их элементов:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
foldBTree branch empty Empty = ???
foldBTree branch empty (Branch a l r) = ???
    -- Let use comments to keep track of the types:
    -- a :: a
    -- l, r :: BTree a

Теперь, если не считать что-то вроде undefined, единственный способ заполнить первое уравнение - empty:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
foldBTree branch empty Empty = empty
foldBTree branch empty (Branch a l r) = ???
    -- a :: a
    -- l, r :: BTree a

Как нам заполнить второе уравнение? Опять же, если не undefined, у нас есть это:

branch :: a -> r -> r -> r
a      :: a
l, r   :: BTree a

Если бы у нас было subfold :: BTree a → r, мы могли бы сделать branch a (subfold l) (subfold r) :: r. Но, конечно, мы можем легко написать 'subfold':

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
foldBTree branch empty Empty = empty
foldBTree branch empty (Branch a l r) = branch a (subfold l) (subfold r)
    where subfold = foldBTree branch empty

Это сгиб для BTree, потому что foldBTree Branch Empty anyTree == anyTree. Обратите внимание, что foldBTree - не единственная функция этого типа; там также это:

mangleBTree :: (a -> r -> r -> r) -> r -> BTree a -> r
mangleBTree branch empty Empty = empty
mangleBTree branch empty (Branch a l r) = branch a (submangle r) (submangle l)
    where submangle = mangleBTree branch empty

Но в общем случае у mangleBTree нет обязательного свойства; например, если у нас есть foo = Branch 1 (Branch 2 Empty Empty) Empty, отсюда следует, что mangleBTree Branch Empty foo/= foo. Таким образом, mangleBTree, хотя и имеет правильный тип, не является фолдом.


Теперь давайте mangleTree от деталей и сконцентрируемся на этом последнем пункте с примером mangleTree. Сгиб (в структурном смысле, # 2 вверху моего ответа) - это не что иное, как простейшая, нетривиальная функция для алгебраического типа, такая, что, когда вы передаете конструкторы типов в качестве аргументов, это становится функцией идентичности для этого типа. (Под нетривиальным я подразумеваю, что такие вещи, как foo fz xs = xs, не допускаются.)

Это очень важно. Мне нравится думать об этом двумя способами:

  1. Сгиб для данного типа может "видеть" всю информацию, содержащуюся в любом значении этого типа. (Вот почему он способен "реконструировать" любое значение этого типа с нуля, используя конструкторы типов.)
  2. Сгиб - самая общая "потребительская" функция для этого типа. Любая функция, которая использует значение рассматриваемого типа, может быть написана так, чтобы единственными операциями, которые она использует из этого типа, были складка и конструкторы. (Хотя версии некоторых функций, предназначенные только для сгиба, сложно написать и выполнить плохо; попробуйте написать tail :: [a] → [a] с помощью foldr, (:) и [] в качестве болезненного упражнения.)

И второй пункт идет еще дальше, в том, что вам даже не нужны конструкторы. Вы можете реализовать любой алгебраический тип без использования объявлений data или конструкторов, используя только сгибы:

{-# LANGUAGE RankNTypes #-}

-- | A Church-encoded list is a function that takes the two 'foldr' arguments
-- and produces a result from them.
newtype ChurchList a = 
    ChurchList { runList :: forall r. 
                            (a -> r -> r)  -- ^ first arg of 'foldr'
                         -> r              -- ^ second arg of 'foldr'
                         -> r              -- ^ 'foldr' result
               }

-- | Convenience function: make a ChurchList out of a regular list
toChurchList :: [a] -> ChurchList a
toChurchList xs = ChurchList (\kons knil -> foldr kons knil xs)

-- | 'toChurchList' isn't actually needed, however, we can make do without '[]'
-- completely.
cons :: a -> ChurchList a -> ChurchList a
cons x xs = ChurchList (\f z -> f x (runlist xs f z))

nil :: ChurchList a
nil = ChurchList (\f z -> z)

foldr' :: (a -> r -> r) -> r -> ChurchList a -> r
foldr' f z xs = runList xs f z

head :: ChurchList a -> Maybe a
head = foldr' ((Just .) . const) Nothing

append :: ChurchList a -> ChurchList a -> ChurchList a
append xs ys = foldr' cons ys xs

-- | Convert a 'ChurchList' to a regular list.
fromChurchList :: ChurchList a -> [a]
fromChurchList xs = runList xs (:) []

В качестве упражнения вы можете попробовать написать другие типы таким способом (который использует расширение RankNTypes прочитайте это для начинающих). Этот метод называется церковным кодированием и иногда полезен в реальном программировании - например, GHC использует нечто, называемое foldr/build Fusion, для оптимизации кода списка для удаления промежуточных списков; посмотрите эту страницу на Haskell Wiki и обратите внимание на тип build:

build :: (forall b. (a -> b -> b) -> b -> b) -> [a]
build g = g (:) []

За исключением newtype, это то же самое, что и мой fromChurchList выше. По сути, одно из правил, которые GHC использует для оптимизации кода обработки списков:

-- Don't materialize the list if all we're going to do with it is
-- fold it right away:
foldr kons knil (fromChurchList xs) ==> runChurchList xs kons knil

Благодаря реализации базовых функций списка для внутреннего использования кодировок Церкови, агрессивного встраивания их определений и применения этого правила к встроенному коду, вложенное использование таких функций, как map может быть объединено в узкий цикл.

Ответ 2

Сгиб на каждый случай

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

Это общее понятие fold соответствует катаморфизму @pelotom, упомянутому в его комментарии.

Рекурсивные типы

Основная идея заключается в том, что эти функции fold определены для рекурсивных типов. Особенно:

data List a = Cons a (List a) | Nil
data Tree a = Branch (Tree a) (Tree a) | Leaf a

Оба эти типа четко перечислены recursive-- List в случае Cons и Tree в случае Branch.

Фиксированные очки

Как и функции, мы можем переписать эти типы, используя фиксированные точки. Запомните определение fix:

fix f = f (fix f)

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

newtype Fix f = Roll (f (Fix f))

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

Это позволяет нам переписывать типы List следующим образом:

data ListContainer a rest = Cons a rest | Nil
type List a = Fix (ListContainer a)

По сути, Fix позволяет нам ListContainer в произвольную глубину. Таким образом, мы могли бы иметь:

Roll Nil
Roll (Cons 1 (Roll Nil))
Roll (Cons 1 (Roll (Cons 2 (Roll Nil))))

которые соответствуют [], [1] и [1,2] соответственно.

ListContainer что ListContainer является Functor, легко:

instance Functor (ListContainer a) where
  fmap f (Cons a rest) = Cons a (f rest)
  fmap f Nil           = Nil

Я думаю, что отображение из ListContainer в List довольно естественно: вместо явного рекурсивного преобразования мы делаем рекурсивную часть переменной. Затем мы просто используем Fix чтобы заполнить эту переменную соответствующим образом.

Мы можем написать аналогичный тип для Tree.

"Развертывание" фиксированных точек

Итак, почему мы заботимся? Мы можем определить fold для произвольных типов, написанных с использованием Fix. Особенно:

fold :: Functor f => (f a -> a) -> (Fix f -> a)
fold h = h . fmap (fold h) . unRoll
  where unRoll (Roll a) = a

По сути, все, что делает сгиб - это разворачивает "свернутый" тип по одному слою за раз, применяя функцию к результату каждый раз. Это "развертывание" позволяет нам определить сгиб для любого рекурсивного типа и аккуратно и естественно обобщить концепцию.

Для примера списка это работает так:

  1. На каждом шаге мы разворачивать Roll, чтобы получить или Cons или Nil
  2. Мы вернемся к остальной части списка, используя fmap.
    1. В случае Nil, fmap (fold h) Nil = Nil, поэтому мы просто возвращаем Nil.
    2. В Cons случае fmap просто продолжает складку над остальной частью списка.
  3. В конце мы получаем несколько вложенных вызовов для fold заканчивающихся на Nil --just, как на стандартном foldr.

Сравнение типов

Теперь давайте посмотрим на типы двух функций сгиба. Сначала foldr:

foldr :: (a -> b -> b) -> b -> [a] -> b

Теперь fold специализированный ListContainer:

fold :: (ListContainer a b -> b) -> (Fix (ListContainer a) -> b)

Сначала они выглядят совершенно иначе. Однако, немного помассируя, мы можем показать, что они одинаковы. Первые два аргумента для foldr - a → b → b и b. У нас есть функция и константа. Мы можем думать о b как () → b. Теперь у нас есть две функции _ → b где _ is () и a → b. Чтобы упростить жизнь, позвольте карри второй функции, дающей нам (a, b) → b. Теперь мы можем написать их как одну функцию, используя Either:

Either (a, b) () -> b

Это верно, потому что, учитывая f :: a → c и g :: b → c, мы всегда можем написать следующее:

h :: Either a b -> c
h (Left a) = f a
h (Right b) = g b

Так что теперь мы можем рассматривать foldr как:

foldr :: (Either (a, b) () -> b) -> ([a] -> b)

(Мы всегда можем добавить круглые скобки вокруг -> как это, если они правы-ассоциативны.)

Теперь давайте посмотрим на ListContainer. Этот тип имеет два случая: Nil, который не несет никакой информации, и Cons, которые имеют как a и b. Другими словами, Nil - это как () а Cons - как (a, b), поэтому мы можем написать:

type ListContainer a rest = Either (a, rest) ()

Очевидно, это то же самое, что я использовал в foldr выше. Итак, теперь мы имеем:

foldr :: (Either (a, b) () -> b) -> ([a] -> b)
fold  :: (Either (a, b) () -> b) -> (List a -> b)

Так что, по сути, типы изоморфных --just разных способов написания одной и той же вещи! Я думаю, что это довольно круто.

(В качестве примечания: если вы хотите узнать больше о такого рода рассуждениях с типами, ознакомьтесь с "Алгеброй алгебраических типов данных", прекрасной серией постов в блоге об этом.)

Вернуться к деревьям

Итак, мы увидели, как мы можем определить общую fold для типов, написанных как фиксированные точки. Мы также видели, как это напрямую foldr с foldr для списков. Теперь давайте посмотрим на ваш второй пример, двоичное дерево. У нас есть тип:

data Tree a = Branch a (Tree a) (Tree a) | Leaf a

мы можем переписать это, используя Fix, следуя правилам, которые я делал выше: мы заменяем рекурсивную часть переменной типа:

data TreeContainer a rest = Branch rest rest | Leaf a
type Tree a = Fix (TreeContainer a)

Теперь у нас есть fold дерева:

fold :: (TreeContainer a b -> b) -> (Tree a -> b)

Ваша оригинальная foldTree выглядит так:

foldTree :: (b -> b -> b) -> (a -> b) -> Tree a -> b

foldTree принимает две функции; мы объединим их в один, сначала используя карри, а затем используя Either:

foldTree :: (Either (b, b) a -> b) -> (Tree a -> b)

Мы также можем видеть, как Either (b, b) a изоморфен TreeContainer ab. Дерево контейнера имеет два случая: Branch, содержащая два b и Leaf, содержащий один a.

Таким образом, эти типы сгиба изоморфны так же, как и в примере списка.

обобщающий

Появляется четкая закономерность. Учитывая нормальный рекурсивный тип данных, мы можем систематически создавать нерекурсивную версию типа, которая позволяет нам выражать тип как фиксированную точку функтора. Это означает, что мы можем механически придумать функции fold для всех этих различных типов - фактически, мы могли бы, вероятно, автоматизировать весь процесс с использованием GHC Generics или чего-то в этом роде.

В некотором смысле это означает, что у нас на самом деле нет разных функций fold для разных типов. Скорее, у нас есть единственная функция fold которая очень полиморфна.

Больше

Сначала я полностью понял эти идеи из выступления Конала Эллиота. Это более подробно, а также говорит о unfold, которое является двойным fold.

Если вы хотите еще глубже вникнуть в подобные вещи, прочитайте фантастическую статью "Функциональное программирование с помощью бананов, линз, конвертов и колючей проволоки". Среди прочего, это вводит понятия "катаморфизмы" и "анаморфизмы", которые соответствуют складкам и разворачиваниям.

Алгебры (и коалгебры)

Кроме того, я не могу не добавить плагин для себя: P. Вы можете увидеть некоторые интересные сходства между тем, как мы используем Either здесь, и тем, как я использовал его, когда говорим об алгебрах в другом ответе SO.

На самом деле существует глубокая связь между fold и алгебрами; кроме того, unfold --the выше двойственная fold --is подключены к коалгебрам, которые являются двойственной алгеброй. Важная идея состоит в том, что алгебраические типы данных соответствуют "начальным алгебрам", которые также определяют сгибы, как описано в остальной части моего ответа.

Вы можете увидеть эту связь в общем типе fold:

fold :: Functor f => (f a -> a) -> (Fix f -> a)

fa → a термин выглядит очень знакомым! Помните, что f-алгебра была определена как что-то вроде:

class Functor f => Algebra f a where
  op :: f a -> a

Таким образом, мы можем думать о fold как о:

fold :: Algebra f a => Fix f -> a

По сути, fold просто позволяет нам "суммировать" структуры, определенные с помощью алгебры.

Ответ 3

Сгиб заменяет каждый конструктор функцией.

Например, foldr cons nil заменяет каждый (:) на cons а [] на nil:

foldr cons nil ((:) 1 ((:) 2 [])) = cons 1 (cons 2 nil)

Для дерева foldTree branch leaf заменяет каждый Branch branch а каждый Leaf leaf:

foldTree branch leaf (Branch (Branch (Leaf 1) (Leaf 2)) (Leaf 3))
    = branch (branch (leaf 1) (leaf 2)) (leaf 2)

Вот почему каждая свёртка принимает аргументы, которые имеют тот же тип, что и конструкторы:

foldr :: (a -> list -> list) -> list -> [a] -> list

foldTree :: (tree -> tree -> tree) -> (a -> tree) -> Tree a -> tree