Как можно продлить монаду с помощью свободной монады?

Question

Предположительно, все монады могут быть выражены с помощью Free (если это неверно, что такое встречный пример и почему)? Как можно определить the continuation monad или соответствующий трансформатор с помощью Free или FreeT - что было бы соответствующим функтором? Или, если они не могут, в чем причина?

Update: По выразил я имею в виду в основном изоморфно Free F где F функтор мы ищем, как, например, Writer w изоморфно Free ((,) w).

Answer 1

Продолжение monad является контрпример, который вы ищете. Я недостаточно осведомлен, чтобы предоставить полное доказательство, но я дам вам пару ссылок для поиска.

Идея состоит в том, что монады имеют понятие «ранг», связанное с ними. «Ранг» примерно означает количество операций, необходимых для обеспечения полной функциональности монады.

Я подозреваю, что, за исключением монадов с продолжением, все монады, с которыми мы имеем дело в Haskell, имеют ранг, например. Identity, Maybe, State s, Either e, ... и их комбинации через их трансформаторы. Например, Identity не производится никакими операциями, Maybe генерируется Nothing, State s по get и put s и Either e по Left e. (Возможно, это показывает, что они все на самом деле имеют конечный ранг, или, возможно, put s рассчитывает как другая операцию для каждого s, так State s имеет ранг размера s, я не уверен.)

Free монады конечно, имеют ранг, потому что Free f явно генерируется операциями, закодированными f.

Вот техническое определение ранга, но это не очень поучительно: http://journals.cambridge.org/action/displayAbstract?aid=4759448

Здесь вы можете увидеть утверждение о том, что продолжение монада не имеет ранг: http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf. Я не уверен, как они это доказывают, но подразумевается, что монада продолжения не генерируется никаким набором операций и, следовательно, не может быть выражена как (частное) от свободной монады.

Надеюсь, кто-то может прийти и убрать мои технические возможности, но это структура доказательства, которую вы хотите.

Answer 2

Вот пара крошечных доказательства того, что там не существует Functor f, что для всех a :: * и m :: * -> *FreeT f m a эквивалентно ContT r m a с помощью обычной интерпретации FreeT.

Дайте m :: * -> * таким образом, чтобы не было примера Functor m. Из-за instance Functor (ContT r m) есть экземпляр Functor (ConT r m). Если ContT r и FreeT f эквивалентны, мы ожидаем Functor (FreeT f m).Однако, используя обычную интерпретацию FreeT, instance (Functor f, Functor m) => Functor (FreeT f m), нет экземпляра Functor (FreeT f m), поскольку нет экземпляра Functor m. (Я расслабился нормальный interpreation из FreeT требовать от Monad m только требует Functor m, так как он только делает использование liftM.)

Пусть m :: * -> * таким образом, что не существует ни одного примера Monad m. Из-за instance Monad (ContT r m) есть экземпляр Monad (ConT r m). Если ContT r и FreeT f эквивалентны, мы ожидаем Monad (FreeT f m). Однако, используя обычную интерпретацию FreeT, instance (Functor f, Monad m) => Monad (FreeT f m), нет экземпляра Monad (FreeT f m), потому что нет экземпляра Monad m.

Если мы не хотим, чтобы использовать обычную интерпретацию Free или FreeT мы можем сколотить монстров, которые работают так же, как Cont r или ContT r. Например, существует Functor (f r), так что Free (f r) a может быть эквивалентно Cont r a с использованием аномальной интерпретации Free, а именно Cont r.

Answer 3

Вот глупый ответ, который показывает, что вам нужен как ваш вопрос, так и мой более ранний ответ.

Cont легко могут быть выражены с помощью Free:

import Control.Monad.Free 
import Control.Monad.Trans.Cont 

type Cont' r = Free (Cont r) 

quotient :: Cont' r a -> Cont r a 
quotient = retract 

Cont является (фактор) свободная монада на себя (конечно). Итак, теперь вы должны четко прояснить, что именно вы подразумеваете под «выражением».

Answer 4

См. my answer to a question of yours from last year. Рассмотрим r = Bool (или, вообще говоря, любой тип r, допускающий нетривиальный автоморфизм).

Определить m (до новых оберток) как m :: (() -> Bool) -> Bool; m f = not (f()). Тогда m нетривиально, но m >> m тривиально. Итак, Cont Bool не изоморфен свободной монаде.

Полный расчет в Haskell:

rwbarton@morphism:/tmp$ ghci 
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help 
Loading package ghc-prim ... linking ... done. 
Loading package integer-gmp ... linking ... done. 
Loading package base ... linking ... done. 
Prelude> import Control.Monad.Cont 
Prelude Control.Monad.Cont> let m :: Cont Bool(); m = ContT (\f -> fmap not (f())) 
Loading package transformers-0.3.0.0 ... linking ... done. 
Prelude Control.Monad.Cont> runCont m (const False) -- m not trivial 
True 
Prelude Control.Monad.Cont> runCont (m >> m) (const False) 
False 
Prelude Control.Monad.Cont> runCont (m >> m) (const True) -- (m >> m) trivial 
True