Они изоморфны c?
Да, они изоморфны c в Haskell. См. В чем разница между Fix, Mu и Nu в пакете схемы рекурсии Эда Кметта для некоторых дополнительных замечаний.
Если да, как вы докажете это?
Начнем с определения функций для выполнения преобразований:
muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix
fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
Чтобы показать, что эти функции являются изоморфизмами, мы должны показать, что:
muToFix . fixToMu = id
fixToMu . muToFix = id
От Fix и обратно
Одно из направлений изоморфизма проявляется несколько прямолинейнее, чем другое:
muToFix (fixToMu t) = t
muToFix (fixToMu t) -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t -- See below.
t -- LHS = RHS
Последний отрывок, cata Fix t = t, может быть проверено с помощью определения cata:
cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix
cata Fix t, то есть Fix (fmap (cata Fix) (unfix t)). Мы можем использовать индукцию, чтобы показать, что она должна быть t, по крайней мере, для конечной t (она становится более тонкой с бесконечными структурами - см. Добавление в конце этого ответа). Есть две возможности для рассмотрения:
unfix t :: f (Fix f) пусто, не имеет рекурсивных позиций, в которые можно копаться. В этом случае он должен быть равен fmap absurd z для некоторых z :: f Void, и, таким образом:
cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (fmap (cata Fix) (fmap absurd z))
Fix (fmap (cata Fix . absurd) z)
-- fmap doesn't do anything on an empty structure.
Fix (fmap absurd z)
Fix (unfix t)
t
unfix t не является пустым. В этом случае мы, по крайней мере, знаем, что fmap (cata Fix) не может ничего сделать, кроме применения cata Fix к рекурсивным позициям. Гипотеза об индукции заключается в том, что при этом эти позиции останутся неизменными. Тогда мы имеем:
cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (unfix t) -- Induction hypothesis.
t
(В конечном счете, cata Fix = id является следствием Fix :: f (Fix f) -> Fix x, являющегося начальной F-алгеброй. Прибегая непосредственно к этому факту в контексте этого доказательства было бы слишком много ярлыков.)
С Mu и обратно
Учитывая muToFix . fixToMu = id, чтобы доказать, что fixToMu . muToFix = id достаточно доказать либо:
, что muToFix инъективно, или
, что fixToMu сюръективно.
Давайте возьмем второй вариант и рассмотрим соответствующие определения:
newtype Mu f = Mu (forall a. (f a -> a) -> a)
fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
fixToMu, будучи сюръективным, означает, что при любом заданном c Functor f, все функции типа forall a. (f a -> a) -> a могут быть определены как \alg -> cata alg t, для некоторых спецификаций c t :: Fix f. Таким образом, задача состоит в том, чтобы каталогизировать функции forall a. (f a -> a) -> a и посмотреть, можно ли все их выразить в этой форме.
Как мы можем определить функцию forall a. (f a -> a) -> a, не опираясь на fixToMu? Независимо от того, что это должно включать использование f a -> a алгебры, предоставленной как аргумент, чтобы получить a результат Прямой маршрут будет применять его к некоторому значению f a. Главное предостережение заключается в том, что, поскольку a является полиморфом c, мы должны иметь возможность вызвать указанное значение f a для любого выбора a. Это осуществимая стратегия, пока существуют f -значения. В этом случае мы можем сделать:
fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)
Чтобы сделать запись более понятной, давайте определим тип для вещей, которые мы можем использовать для определения forall a. (f a -> a) -> a функций:
data Moo f = Empty (f Void)
fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)
Помимо прямой маршрут, есть еще одна возможность. Учитывая, что f является Functor, если у нас каким-то образом есть значение f (Moo f), мы можем применить алгебру дважды, причем первое приложение находится под внешним слоем f, через fmap и fromMoo:
fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
Учитывая, что мы также можем сделать forall a. (f a -> a) -> a из f (Moo f) значений, имеет смысл добавить их как случай Moo:
data Moo f = Empty (f Void) | Layered (f (Moo f))
Соответственно, fromLayered могут быть включены в fromMoo:
fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
Empty z -> \alg -> alg (fmap absurd z)
Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
Обратите внимание, что, таким образом, мы хитро перешли от применения alg под одним f слоем к рекурсивному применению alg под произвольным числом из f слоев.
Далее мы можем заметить, что значение f Void может быть введено в конструктор Layered:
emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)
Это означает, что нам на самом деле не нужно Empty конструктор:
newtype Moo f = Moo (f (Moo f))
unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u
А как насчет случая Empty в fromMoo? Единственная разница между этими двумя случаями заключается в том, что в случае Empty вместо \moo -> fromMoo moo alg мы имеем absurd. Поскольку все Void -> a функции absurd, нам не нужен отдельный случай Empty:
fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
Возможный косметический c твик переворачивает аргументы fromMoo, поэтому нам не нужно записывать аргумент в fmap в виде лямбды:
foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)
Или, более бессмысленно :
foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo
На этом этапе второй взгляд на наши определения предполагает некоторое переименование в порядке:
newtype Fix f = Fix (f (Fix f))
unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u
cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix
fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t
И вот оно: все forall a. (f a -> a) -> a функции имеют вид \alg -> cata alg t для некоторых t :: Fix f. Следовательно, fixToMu сюръективен, и у нас есть желаемый изоморфизм.
Добавление
В комментариях был задан уместный вопрос о применимости аргумента индукции в выводе cata Fix t = t , Как минимум, функтор l aws и параметричность гарантируют, что fmap (cata Fix) не создаст дополнительную работу (например, она не увеличит структуру или не введет дополнительные рекурсивные позиции, чтобы копаться в ней), что оправдывает необходимость вступления в рекурсивные позиции - это все, что имеет значение на индуктивном этапе деривации. При этом, если t является конечной структурой, базовый случай пустого f (Fix t) будет в конечном итоге достигнут, и все будет ясно. Если мы позволим t быть бесконечным, мы можем продолжать бесконечно снижаться, fmap после fmap после fmap, не достигая базового случая.
Ситуация с бесконечными структурами, хотя , не так ужасно, как может показаться на первый взгляд. Лень, которая делает бесконечные структуры жизнеспособными в первую очередь, позволяет нам лениво потреблять бесконечные структуры:
GHCi> :info ListF
data ListF a b = Nil | Cons a b
-- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1
Хотя последовательность рекурсивных позиций расширяется бесконечно, мы можем остановиться в любой точке и получить полезные результаты из окружающих ListF функториальных контекстов. Следует повторить, что такие контексты не зависят от fmap, и поэтому любой конечный сегмент структуры, который мы могли бы потреблять, не будет затронут cata Fix.
Эта отсрочка лени отражает то, как, как упоминалось в другом месте в этом В дискуссии лень сводит на нет различия между фиксированными точками Mu, Fix и Nu. Без лени, Fix недостаточно для кодирования продуктивного ядра, и поэтому мы должны переключиться на Nu, самую большую фиксированную точку. Вот небольшая демонстрация различия:
GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.