Функторы фиксированной точки Free и Cofree

Чтобы это было ясно, я не говорю о том, как свободная монада очень похожа на комбинатор исправлений, примененный к функтору, то есть как Free f в основном неподвижная точка f. (Не то чтобы это не интересно!)

То, что я говорю, это fixpoints Free, Cofree :: (*->*) -> (*->*), то есть функторы f такие, что Free f является изоморфным самому f.

Предыстория: сегодня, чтобы укрепить мое довольно не хватающееся на свободных монадах, я решил просто написать несколько из них для разных простых функторов, для Free и для Cofree и посмотреть, какие более известные [co] монады были бы изоморфны. Меня особенно интересовало открытие , что Cofree Empty изоморфно Empty (что означает Const Void, функтор, который отображает любой тип к необитаемым). Хорошо, возможно, это просто глупо - я обнаружил, что если вы положите пустой мусор, вы получите пустой мусор, да! - но эй, это теория категорий, где целые вселенные поднимаются от кажущихся тривиальностей... правильно?

Непосредственный вопрос: если Cofree имеет такую неподвижную точку, что относительно Free? Ну, это, конечно, не может быть Empty, как это не монада. Быстрого подозреваемого было бы рядом, например, Const () или Identity, но no:

Free (Const ()) ~~ Either () ~~ Maybe
Free Identity   ~~ (Nat,)    ~~ Writer Nat

В самом деле, факт, что Free всегда добавляет дополнительный конструктор, предполагает, что структура любого функтора, что неподвижная точка должна быть уже бесконечной. Но кажется странным, что если Cofree имеет такую простую неподвижную точку, Free должна иметь только более сложную (например, fix-by-construction FixFree a = C (Free FixFree a), которую поднимает Reid Barton в комментариях).

Является ли скучная правда только тем, что Free не имеет "случайной неподвижной точки", и это простое совпадение, что Cofree имеет одно, или я что-то не хватает?

Ответ 1

Поскольку вы спросили о структуре неподвижных точек Free, я собираюсь набросать неофициальный аргумент, что Free имеет только одну неподвижную точку, которая является Functor, а именно тип

newtype FixFree a = C (Free FixFree a)

описанном Рейдом Бартоном. Действительно, я делаю несколько более жесткое требование. Начните с нескольких частей:

newtype Fix f a = Fix (f (Fix f) a)
instance Functor (f (Fix f)) => Functor (Fix f) where
  fmap f (Fix x) = Fix (fmap f x)

-- This is basically `MFunctor` from `Control.Monad.Morph`
class FFunctor (g :: (* -> *) -> * -> *) where
  hoistF :: Functor f => (forall a . f a -> f' a) -> g f b -> g f' b

Следует отметить, что

instance FFunctor Free where
  hoistF _f (Pure a) = Pure a
  hoistF f (Free fffa) = Free . f . fmap (hoistF f) $ fffa

Тогда

fToFixG :: (Functor f, FFunctor g) => (forall a . f a -> g f a) -> f a -> Fix g a
fToFixG fToG fa = Fix $ hoistF (fToFixG fToG) $ fToG fa

fixGToF :: forall f b (g :: (* -> *) -> * -> *) .
           (FFunctor g, Functor (g (Fix g)))
        => (forall a . g f a -> f a) -> Fix g b -> f b
fixGToF gToF (Fix ga) = gToF $ hoistF (fixGToF gToF) ga

Если я не ошибаюсь (каким бы я мог быть), передавая каждую сторону изоморфизма между f и g f каждой из этих функций, каждая сторона изоморфизма между f и Fix g, Подстановка Free для g будет демонстрировать претензию. Разумеется, этот аргумент очень рушительный, потому что Haskell непоследователен.

Ответ 2

Ваше наблюдение, что Empty является фиксированной точкой Cofree (что на самом деле не так актуально в Haskell, но я думаю, вы хотите работать в некоторой модели, которая игнорирует ⊥, например Set) сводится к тому факту, что

существует множество E (пустое множество) такое, что для любого множества X проекция p₂: X × E → E является изоморфизмом.

В этой ситуации мы могли бы сказать, что E является поглощающим объектом для произведения. Мы можем заменить слово "set" на "объект C" для любой категории C с продуктами, и мы получаем утверждение о C, которое может быть или не быть истинным. Для Set это правда.

Если мы выберем C = Set ^op у которого также есть продукты (потому что Set имеет копродукты), а затем дуализируйте язык, чтобы снова говорить о наборах, мы получаем утверждение

существует такое множество F, что для любого множества Y включение i₂: F → Y + F является изоморфизмом.

Очевидно, что это утверждение неверно для любого множества F (мы можем выбрать любое непустое множество Y в качестве контрпримера для любого F). Не удивительно, ведь Set ^op - это отличная категория от Set.

Таким образом, мы не получим "тривиальную неподвижную точку" Free так же, как мы получили один для Cofree, потому что Set ^op качественно отличается от Set. Исходным объектом Set является поглощающий элемент для продукта, но конечный объект Set не является поглощающим объектом для копроизведения.

Если я могу на мгновение попасть в мой ящик:

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

Предположим, что у меня есть конструкция, которую я могу выполнить для любой категории C (или любой категории с некоторой дополнительной структурой и/или свойствами). Тогда двойная конструкция в категории C является исходной конструкцией в противоположной категории C ^op (у которой лучше иметь дополнительную структуру и свойства, которые нам нужны, если они есть).

Например: понятие продуктов имеет смысл в любой категории C (хотя продукты могут не всегда существовать) через универсальные свойства, определяющие продукты. Чтобы получить двойственное представление о копроизведениях на C, мы должны спросить, какие продукты в C ^op и мы только что определили, какие продукты находятся в любой категории, поэтому это понятие имеет смысл.

Проблема с применением дуальности к настройке Haskell заключается в том, что язык Haskell предпочитает в подавляющем большинстве говорить только о одной категории, Hask, в которой мы делаем наши конструкции. Это вызывает две проблемы для разговора о двойственности:

Чтобы получить двойственное построение, как описано выше, я должен уметь иметь возможность делать конструкцию в любой категории или, по крайней мере, в любой категории конкретной формы. Поэтому мы должны сначала обобщить конструкцию, которая, как правило, мы делали только в категории Hask для более широкого класса категорий. (И, сделав это, есть много других интересных категорий, которые мы могли бы потенциально интерпретировать полученное выше понятие, помимо Хаска ^op например, категорий Кляйсли монад.)
Категория Hask обладает многими специальными свойствами, которые можно суммировать, сказав, что (игнорируя ⊥). Hask является декартовой замкнутой категорией. Например, это означает, что начальный объект является поглощающим объектом для продукта. Hask ^op не имеет этих свойств, что означает, что обобщенное понятие может не иметь смысла в Hask ^op; и это также может означать, что два понятия, которые были эквивалентны в Хаске, вообще различны и имеют разные двойники.

Для примера последнего возьмите линзы. В Hask они могут быть построены несколькими способами; два способа относятся к парам геттер/сеттер и как коалгебры для coston comonad. Первое обобщает категории с продуктами, а второе - на категории, обогащенные определенным образом над Хаском. Если применить прежнюю конструкцию к Hask ^op тогда мы выберем призмы, но если применить последнюю конструкцию к Hask ^op то мы получим алгебры для государственной монады, и это не то же самое.

Более знакомым примером может быть comonads: начиная с ориентированной на Haskell презентации

return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

Кажется, что требуется некоторое понимание, чтобы определить, какие стрелки обращаются, чтобы получить

extract :: w a -> a
extend :: w a -> (w b -> a) -> w b

Дело в том, что было бы намного легче начать с join :: m (m a) -> m a вместо (>>=); но поиск этой альтернативной презентации (эквивалентной из-за особенностей Hask) - это творческий процесс, а не механический.

В вопросе, подобном вашему, и многим другим нравится это, где довольно ясно, что подразумевается в дуальном смысле, нет абсолютно никаких оснований ожидать априори, что двойная конструкция будет фактически существовать или иметь те же свойства, что и оригинал, потому что Hask ^op качественно ведет себя совсем иначе, чем Hask. Лозунг может быть

теория категорий является самодвойственной, но теория какой-либо конкретной категории не есть!