Бесплатная монада и бесплатная работа

Один из способов описать свободную монаду - сказать, что это начальный моноид в категории эндофункторов (некоторой категории C), объекты которых являются эндофункторами от C до C, стрелки - это естественные преобразования между ними. . Если мы возьмем C за Hask, то эндофунктор - это то, что называется Functor в haskell, которое является функтором от * -> *, где * представляет объекты Hask

По умолчанию любая карта из эндофунктора t в моноид m в End(Hask) индуцирует карту из Free t в m.

Иначе говоря, любое естественное преобразование из функтора t в монаду m вызывает естественное преобразование из Free t в m

Я ожидал, что смогу написать функцию

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

но это не может быть унифицировано, тогда как следующие работы

free :: (Functor t, Monad m) => (t (m a) → m a) → (Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

или его обобщение с подписью

free :: (Functor t, Monad m) => (∀ a. t a → a) → (∀ a. Free t a → m a)

Я ошибся в теории категорий или в переводе на Haskell?

Мне было бы интересно услышать здесь немного мудрости ..

PS: код с включенным

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
import Control.Monad.Free

haskell monads category-theory free-monad
person nicolas    schedule 03.01.2016    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Перевод Haskell кажется неправильным. Большой намек в том, что ваша free реализация нигде не использует монадическое связывание (или соединение). Вы можете найти free как foldFree со следующим определением :

free :: Monad m => (forall x. t x -> m x) -> (forall a. Free t a -> m a)
free f (Pure a)  = return a
free f (Free fs) = f fs >>= free f

Ключевым моментом является то, что f специализируется на t (Free t a) -> m (Free t a), тем самым устраняя один Free слой одним махом.

person András Kovács    schedule 03.01.2016

arrow_upward
3
arrow_downward

Я не знаю о части теории категорий, но часть Haskell определенно плохо типизирована с вашей исходной реализацией и исходной сигнатурой типа.

Данный

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)

когда вы выполняете сопоставление с образцом на Free tfta, вы получаете

tfta :: t (Free t a)
f :: forall a. t a -> m a 
free :: (forall a. t a -> m a) -> forall a. Free t a -> m a

И поэтому

free f :: forall a. Free t a -> m a

ведущий к

fmap (free f) :: forall a. t (Free t a) -> t (m a)

Итак, чтобы иметь возможность свернуть этот t (m a) в желаемый m a, вам нужно применить к нему f (чтобы «превратить t в m»), а затем воспользоваться тем фактом, что m является монадой:

f . fmap (free f) :: forall a. t (Free t a) -> m (m a)
join . f . fmap (free f) :: forall a. t (Free t a) -> m a

это означает, что вы можете исправить исходное определение, изменив вторую ветвь free:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

import Control.Monad.Free
import Control.Monad

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free tfta) = join . f . fmap (free f) $ tfta

Это проверка типов, и, возможно, это может быть то, что вы хотите :)

person Cactus    schedule 03.01.2016
comment
действительно, и это хорошая альтернатива другому ответу, использующему соединение вместо связывания. Хотел бы я отметить эти два ответа как правильные - person nicolas; 03.01.2016
comment
Обратите внимание, что это free в терминах принципа рекурсии для Free: free f = fold (join . f) return, где fold :: Functor f => (f b -> b) -> (a -> b) -> Free f a -> b. Для сравнения, библиотека _5 _ с >>= не требует Functor ограничения, потому что тип данных Free в Haskell действителен для всех f :: * -> * параметров, и мы можем вычислять эту структуру напрямую (хотя Free f a с нефунктором f не очень полезен). - person András Kovács; 03.01.2016