14

明確にするために、フリーモナドが functor に適用された fixpoint コンビネータにどのように似ているかについて話しているのではありません。（これは面白くないというわけではありません！）Free ff

私が話しているのは の不動点Free, Cofree :: (*->*) -> (*->*)、つまりそれ自体に同形fな関手です。Free ff

背景: 今日、自由モナドについての理解不足を補うために、 forFreeとfor のCofree両方で、さまざまな単純な関手についてそれらのいくつかを書き出すことにしました。 . 私が特に興味をそそられたのは、 と同型 (つまり、任意の型を無人にマップする関手) であるという発見Cofree EmptyでしEmptyたConst Void。OK、これはばかげているかもしれません。空のゴミを入れると、空のゴミが出てくることを発見しました。– でもねえ、これは圏論であり、宇宙全体が一見些細なことから立ち上がる... ですよね?

当面の問題は、そのCofreeような不動点がある場合、どうなるかということFreeです。まあ、それEmptyはモナドではないので、確かにあり得ません。Const ()手っ取り早い容疑者は、またはのような近くのものですが、そうIdentityではありません:

Free (Const ()) ~~ Either () ~~ Maybe
Free Identity   ~~ (Nat,)    ~~ Writer Nat

実際、Free常に余分なコンストラクターを追加するという事実は、不動点であるファンクターの構造がすでに無限でなければならないことを示唆しています。Cofreeしかし、そのような単純な固定点がある場合、( Reid Barton がコメントで取り上げたFreefix-by-construction のように) はるかに複雑な固定点しか持たないのは奇妙に思えます。FixFree a = C (Free FixFree a)

退屈な真実は「偶然の不動点」FreeがなくCofree、あるのは単なる偶然なのか、それとも何かが欠けているのでしょうか?

4

2 に答える 2

5
于 2016-12-17T22:45:53.040 に答える
1

の不動点の構造について質問されたので、型である不動点が 1 つしかないFree非公式な議論をスケッチします。FreeFunctor

newtype FixFree a = C (Free FixFree a)

リード・バートンが説明した。確かに、私はやや強い主張をします。いくつかの部分から始めましょう：

newtype Fix f a = Fix (f (Fix f) a)
instance Functor (f (Fix f)) => Functor (Fix f) where
  fmap f (Fix x) = Fix (fmap f x)

-- This is basically `MFunctor` from `Control.Monad.Morph`
class FFunctor (g :: (* -> *) -> * -> *) where
  hoistF :: Functor f => (forall a . f a -> f' a) -> g f b -> g f' b

特に、

instance FFunctor Free where
  hoistF _f (Pure a) = Pure a
  hoistF f (Free fffa) = Free . f . fmap (hoistF f) $ fffa

それで

fToFixG :: (Functor f, FFunctor g) => (forall a . f a -> g f a) -> f a -> Fix g a
fToFixG fToG fa = Fix $ hoistF (fToFixG fToG) $ fToG fa

fixGToF :: forall f b (g :: (* -> *) -> * -> *) .
           (FFunctor g, Functor (g (Fix g)))
        => (forall a . g f a -> f a) -> Fix g b -> f b
fixGToF gToF (Fix ga) = gToF $ hoistF (fixGToF gToF) ga

私が間違っていなければ (私がそうである可能性があります)、同型の各辺をこれらの関数の間fおよび各関数に渡すと、との間g fの同型の各辺が得られます。に代入すると、主張が示されます。もちろん、Haskell には一貫性がないため、この議論は非常に手の込んだものです。fFix gFreeg

于 2016-12-19T06:59:11.563 に答える