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

Ответ 1

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

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

Я подозреваю, что, за исключением монадов с продолжением, все монады, с которыми мы имеем дело в 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 f явно генерируется операциями, закодированными с помощью f.

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

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

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

Ответ 2

См. мой ответ на ваш вопрос с прошлого года. Пусть рассмотрим r = Bool (или, вообще говоря, любой тип r, допускающий нетривиальный автоморфизм).

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

Полные вычисления в Haskell:

[email protected]:/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

Ответ 3

Здесь пара крошечных доказательств отсутствия такого 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. (Я расслаблял нормальный интервал 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.

Ответ 4

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

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 является (частным) свободной монады на себе (разумеется). Итак, теперь вы должны четко прояснить, что именно вы подразумеваете под "выражением".