haskell - モナドの無料モナド

Question

とx >>= f同等retract (liftF x >>= liftF . f)ですか？

つまり、モナドでもあるファンクターからの無料のモナドビルドのモナドインスタンスは、元のモナドと同等のモナドインスタンスを持つことになりますか？

Answer 1

あなたの定義が何であるかはわかりませんretractが、与えられた

retract :: Monad m => Free m a -> m a
retract (Pure a) = return a
retract (Impure fx) = fx >>= retract

と

liftF :: Functor f => f a -> Free f a
liftF fx = Impure (fmap Pure fx)

注意してください (証明は間違っている可能性があります。手で行ったものであり、チェックしていません)

retract $ liftF x
= retract (Impure (fmap Pure x))
= (fmap Pure x) >>= retract
= (x >>= return . Pure) >>= retract
= x >>= \y -> (return $ Pure y) >>= retract
= x >>= \y -> (retract (Pure y))
= x >>= \y -> return y
= x >>= return
= x

だからあなたは持っています

retract (liftF x >>= liftF . f)
= retract ((Impure (fmap Pure x)) >>= liftF . f)
= retract $ Impure $ fmap (>>= liftF . f) $ fmap Pure x
= (fmap (>>= liftF . f) $ fmap Pure x) >>= retract
= (fmap (\y -> Pure y >>= liftF . f) x) >>= retract
= (fmap (liftF . f) x) >>= retract
= (liftM (liftF . f) x) >>= retract
= (x >>= return . liftF . f) >>= retract
= x >>= (\y -> (return $ liftF $ f y >>=  retract)
= x >>= (\y -> retract $ liftF $ f y)
= x >>= (\y -> retract . liftF $ f y)
= x >>= (\y -> f y)
= x >>= f

Free m aこれは、が に同形であることを意味するのではなく、実際に撤回を目撃しているm aだけです。はモナド射ではないretractことに注意してください(には行きません)。Free はファンクターのカテゴリーのファンクターですが、モナドのカテゴリーのモナドではありません (よく似ていてよく似ているにもかかわらず)。liftFreturnreturnretractjoinliftFreturn

編集:撤回は一種の同等性を意味することに注意してください。定義

 ~ : Free m a -> Free m a -> Prop
 a ~ b = (retract a) ==_(m a) (retract b)

次に、商型を考えFree m a/~ます。この型は と同形であると断言しm aます。以来。(liftF (retract x)) ~ x_ (retract . liftF . retract $ x) ==_(m a) retract xしたがって、モナド上の自由モナドは、まさにそのモナドに追加のデータを加えたものです。これは、 isがモノイドの場合[m]と「本質的に同じ」という主張とまったく同じです。mmm

Answer 2

つまり、モナドでもあるファンクターからの無料のモナドビルドのモナドインスタンスは、元のモナドと同等のモナドインスタンスを持つことになりますか？

いいえ。ファンクターの上の無料のモナドはモナドです。したがって、Monadインスタンスが存在する場合、それを魔法のように知ることはできません。また、同じファンクターがさまざまな方法でモナドになる可能性があるため（たとえば、さまざまなモノイドのライターモナド）、それを「推測」することもできません。

もう1つの理由は、これら2つのモナドが型として同型でさえないため、これら2つのモナドが同等のインスタンスを持っているかどうかを尋ねるのはあまり意味がないということです。たとえば、ライターモナドよりも無料のモナドを考えてみましょう。リストのような構造になります。これらの2つのインスタンスが同等であるとはどういう意味ですか？

さまざまなモナドインスタンスの例

上記の説明が明確でない場合のために、これは多くの可能なモナドインスタンスを持つタイプの例です。

data M a = M Integer a

bindUsing :: (Integer -> Integer -> Integer) -> M a -> (a -> M b) -> M b
bindUsing f (M n a) k =
  let M m b = k a
  in M (f m n) b

-- Any of the below instances is a valid Monad instance
instance Monad M where
  return x = M 0 x
  (>>=) = bindUsing (+)

instance Monad M where
  return x = M 1 x
  (>>=) = bindUsing (*)