Разница между свободными монадами и фиксированными точками функторов?

Ответ 1

(N.B. это немного сочетается как с моими, так и с комментариями @Gabriel выше).

Возможно, что каждый житель точки Fix ed a Functor бесконечен, т.е. let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...)))) является единственным жителем Fix Identity. Free отличается от Fix тем, что он обеспечивает, по крайней мере, один конечный житель Free f. В самом деле, если Fix f имеет бесконечные обитатели, то Free f имеет бесконечно много конечных обитателей.

Другим непосредственным побочным эффектом этой неограниченности является то, что Functor f => Fix f больше не является Functor. Нам нужно было бы реализовать fmap :: Functor f => (a -> b) -> (f a -> f b), но Fix "заполнил все дыры" в f a, который использовался для размещения a, поэтому у нас больше нет a, чтобы применить наш fmap ' d для функции.

Это важно для создания Monad, потому что мы хотели бы реализовать return :: a -> Free f a и иметь, скажем, этот закон, fmap f . return = return . f, но он даже не имеет смысла в Functor f => Fix f.

Итак, как Free "исправить" эти недостатки Fix ed point? Он "дополняет" наш базовый функтор конструктором Pure. Таким образом, для всех Functor f, Pure :: a -> Free f a. Это наш гарантированный конечный житель этого типа. Он также сразу дает нам корректное определение return.

return = Pure

Итак, вы можете подумать об этом добавлении как о выделении потенциально бесконечного "дерева" вложенного Functor, созданного Fix, и смешивания в некотором количестве "живых" почек, представленных Pure. Мы создаем новые почки, используя return, который может быть интерпретирован как обещание "вернуться" к этому почтовому ящику позже и добавить больше вычислений. На самом деле это то, что делает flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b). Учитывая функцию продолжения f :: a -> Free f b, которая может быть применена к типам a, мы возвращаем наше дерево, возвращающееся к каждому Pure a, и заменяем его продолжением, вычисленным как f a. Это позволяет нам "расти" наше дерево.

Теперь Free явно более общий, чем Fix. Чтобы управлять этим домом, можно увидеть любой тип Functor f => Fix f как подтип соответствующего Free f a! Просто выберите a ~ Void, где у нас есть data Void = Void Void (т.е. Тип, который нельзя построить, является пустым типом, не имеет экземпляров).

Чтобы сделать это более понятным, мы можем разбить наш Fix 'd Functor на break :: Fix f -> Free f a, а затем попытаться инвертировать его с помощью affix :: Free f Void -> Fix f.

break (Fix f) = Free (fmap break f) 
affix (Free f) = Fix (fmap affix f)

Обратите внимание, что affix не нужно обрабатывать случай Pure x, потому что в этом случае x :: Void и, следовательно, на самом деле не может быть там, поэтому Pure x абсурд, и мы просто проигнорируем его.

Также обратите внимание, что тип возвращаемого типа break немного тонкий, поскольку тип типа a появляется только в возвращаемом типе Free f a, так что он полностью недоступен для любого пользователя break. "Полностью недоступные" и "не могут быть инстанцированы" дают нам первый намек на то, что, несмотря на типы, affix и break являются обратными, но мы можем просто доказать это.

(break . affix) (Free f)
===                                     [definition of affix]
break (Fix (fmap affix f))
===                                     [definition of break]
Free (fmap break (fmap affix f))
===                                     [definition of (.)]
Free ( (fmap break . fmap affix) f )
===                                     [functor coherence laws]
Free (fmap (break . affix) f)

который должен показать (коиндуктивно или просто интуитивно, возможно), что (break . affix) является тождеством. Другое направление проходит совершенно одинаково.

Итак, надеюсь, это показывает, что Free f больше, чем Fix f для всех Functor f.

Так зачем вообще использовать Fix? Ну, иногда вам нужны только свойства Free f Void из-за некоторого побочного эффекта слоя f s. В этом случае вызов Fix f делает более понятным, что мы не должны пытаться (>>=) или fmap по типу. Кроме того, поскольку Fix является просто newtype, компилятору может быть проще "скомпилировать" слои Fix, поскольку он все равно играет семантическую роль.

• Примечание. Мы можем более формально говорить о том, как Void и forall a. a являются изоморфными типами, чтобы более четко видеть, как типы affix и break являются гармоничными. Например, мы имеем absurd :: Void -> a как absurd (Void v) = absurd v и unabsurd :: (forall a. a) -> Void как unabsurd a = a. Но это немного глупо.

Ответ 2

Существует глубокая и "простая" связь.

Это следствие теоремы о присоединенном функторе, левые примыкания сохраняют начальные объекты: L 0 ≅ 0.

Категорически Free f является функтором из категории в ее алгебры F- (Free f оставляется присоединенным к забывчивому функтору, идущему в обратном направлении). Работая в Hask, наша начальная алгебра Void

Free f Void ≅ 0

и исходная алгебра в категории F- алгебр является Fix f: Free f Void ≅ Fix f

import Data.Void
import Control.Monad.Free

free2fix :: Functor f => Free f Void -> Fix f
free2fix (Pure void) = absurd void
free2fix (Free body) = Fix (free2fix <$> body)

fixToFree :: Functor f => Fix f -> Free f Void
fixToFree (Fix body) = Free (fixToFree <$> body)

Аналогично, правый сопряженными (Cofree f, функтор из HASK к категории F- совместно алгебра) сохраняют конечные объекты: R 1 ≅ 1.

В HASK это единица измерения: () и конечный объект F- совместно алгебры также Fix f (они совпадают в HASK) таким образом мы получаем: Cofree f() ≅ Fix f

import Control.Comonad.Cofree

cofree2fix :: Functor f => Cofree f () -> Fix f
cofree2fix (() :< body) = Fix (cofree2fix <$> body)

fixToCofree :: Functor f => Fix f -> Cofree f ()
fixToCofree (Fix body) = () :< (fixToCofree <$> body)

Просто посмотрите, насколько похожи определения!

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

Fix f - это Free f без переменных.

data Free f a 
  = Pure a 
  | Free (f (Free f a))

Fix f Cofree f с фиктивными значениями.

data Cofree f a 
  = a <: f (Cofree f a)

Ответ 3

Для функтора F точка фиксации T функтора F сгенерирует монаду как

data M = T + X

Чтобы упростить обсуждение, мы можем определить тип в haskell таким образом, чтобы

type T+X = Either T X

1. Что мы знаем о Т.
   Для T мы знаем, что существует изоморфизм от T к FT который

in . out = id
in :: F T -> T
out :: T -> FT

Тогда мы можем построить return :: X → T+X и join :: T + (T + X) → T + X

1. return :: X → T + X Это просто, return = Right

2. join :: T+(T+X) → T+X В коде это просто, мы объясним концепцию позже

join (Left x) = Left x
join [email protected](Right _) = r

Для T + X мы имеем морфизм f :: (T → T + X) и id :: T + X → T + X Тогда мы имеем T + (T + X) = f + id