Существует ли свободная монада?

Из теории категорий известно, что не все эндофункторы в Set допускают свободную монаду. Канонический контрпример является функтором функций.

Но Haskell может превратить любой функтор в свободную монаду.

data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Monad (Free f) where
  return = Pure
  Pure a >>= f = f a
  Free m >>= f = Free ((>>= f) <$> m)

Что делает эту конструкцию для любого функтора Haskell, но разбивается на Установить?

Ответы

Ответ 1

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

Рассмотрим набор мощности в Set. Если у нас есть функция f : S -> T, мы можем образовать f' : PS S -> PS T на f' X = f [X]. Хороший ковариантный функтор (я думаю). Мы могли бы также сформировать f'' X = f^(-1) [X], хороший контравариантный функтор (я думаю).

Посмотрите на "power set" в Haskell:

newtype PS t = PS (t -> Bool)

Это не Functor, а только Contravariant:

instance Contravariant PS where
  contramap f (PS g) = PS (g . f)

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

Я бы предположил, что причина, по которой Хаскелл допускает свободную монаду для каждого ковариантного функтора, состоит в том, что она исключает те ковариантные функторы, которые вызывают проблемы для Set.

Ответ 2

I (скорее) есть подозрение, что это не совсем определение. Скажем, эта рекурсивная формула определяет фиксированную точку; теперь, откуда мы знаем, что эта фиксированная точка существует? Откуда мы знаем только одну контрольную точку? И еще, как Free m >>= определяет что-либо, кроме, может быть, в том случае, когда мы предполагаем, что мы имеем только конечные последовательности приложений Free?