26

おそらく、すべてのモナドは次を使用して表現できますFree(これが正しくない場合、反例とは何ですか?その理由は何ですか)? 継続モナドまたはそれに対応する変換子は、or を使用してどのように表現FreeできますFreeTか?対応するファンクターは何でしょうか? または、できない場合、その理由は何ですか?

更新:表現とは、基本的にwhereが探しているファンクタと同型Free Fであることを意味します。たとえば、は と同型です。FWriter wFree ((,) w)

4

4 に答える 4

15

継続モナドはあなたが探している反例です。私は完全な証拠を提供するのに十分な知識を持っていませんが、調べるための参考文献をいくつか紹介します.

モナドには「ランク」という概念が関連付けられているという考え方です。「ランク」とは、モナドの完全な機能を提供するために必要な操作の数を大まかに意味します。

継続派生モナドを除いて、Haskell で扱うすべてのモナドにはランク ( 、Identity、、... など) があり、トランスフォーマーによるそれらの組み合わせがあるのではないかと思います。たとえば、は操作なしで生成され、は、およびによって生成されます。(おそらくこれは、それらすべてが実際に有限のランクを持っていることを示しているか、またはおそらくそれぞれの異なる操作としてカウントされているため、サイズのランクが であることを示しています。よくわかりません。)MaybeState sEither eIdentityMaybeNothingState sgetput sEither eLeft eput ssState ss

Free fによってエンコードされた操作によって明示的に生成されるため、自由モナドは確かにランクを持ちfます。

これはランクの技術的な定義ですが、あまり啓発的ではありません: http://journals.cambridge.org/action/displayAbstract?aid=4759448

ここで、継続モナドにはランクがないという主張を見ることができます: http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf。彼らがそれをどのように証明したのかはわかりませんが、意味は、継続モナドは操作のコレクションによって生成されないため、フリーモナド (の商) として表現できないということです。

うまくいけば、誰かが来て私の技術を整理してくれますが、これはあなたが望む証明の構造です。

于 2014-09-14T10:25:03.630 に答える
2

昨年のあなたの質問に対する私の回答をご覧ください。考えてみましょうr = Bool(または、より一般的にはr、非自明な自己同形を認める任意の型)。

m(newtype ラッパーまで) として定義しm :: (() -> Bool) -> Bool; m f = not (f ())ます。その後mは自明でm >> mはありませんが、自明です。SoCont 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
于 2014-09-18T18:08:08.093 に答える
1

これは、 の通常の解釈を使用するのと同等であるFunctor fような が存在しないことを示すいくつかの小さな証明です。a :: *m :: * -> * FreeT f m aContT r m aFreeT

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 mliftM

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) aCont r aFreeCont r

于 2014-09-17T02:50:04.227 に答える