11

このブログ投稿では、著者はFreeモナドを使用してコードを精製することの等式的な推論の利点について説明しています。Freeモナド変換子FreeTは、IOをラップした場合でも、これらの利点を保持しますか？

4

1 に答える 1

15

はい。 FreeTそれがモナドであるという事実を除いて、ベースモナドの特定のプロパティに依存しません。推論できるすべての方程式にFree fは、の同等の証明がありFreeT f mます。

それを実証するために、私のブログ投稿で演習を繰り返しましょう。ただし、今回はFreeT：を使用します。

data TeletypeF x
  = PutStrLn String x
  | GetLine (String -> x)
  | ExitSuccess
  deriving (Functor)

type Teletype = FreeT TeletypeF

exitSuccess :: (Monad m) => Teletype m r
exitSuccess = liftF ExitSuccess

無料のモナド変換子には次の定義を使用しましょう。

return :: (Functor f, Monad m) => r -> FreeT f m r
return r = FreeT (return (Pure r))

(>>=) :: (Functor f, Monad m) => FreeT f m a -> (a -> FreeT f m b) -> FreeT f m b
m >>= f = FreeT $ do
    x <- runFreeT m
    case x of
        Free w -> return (Free (fmap (>>= f) w))
        Pure r -> runFreeT (f r)

wrap :: (Functor f, Monad m) => f (FreeT f m r) -> FreeT f m r
wrap f = FreeT (return (Free f))

liftF :: (Functor f, Monad m) => f r -> FreeT f m r
liftF fr = wrap (fmap return fr)

等式推論を使用して、次のようになるものを推測できますexitSuccess。

exitSuccess

-- Definition of 'exitSuccess'
= liftF ExitSuccess

-- Definition of 'liftF'
= wrap (fmap return ExitSuccess)

-- fmap f ExitSuccess = ExitSuccess
= wrap ExitSuccess

-- Definition of 'wrap'
= FreeT (return (Free ExitSuccess))

これで、次のことを証明できますexitSuccess >> m= exitSuccess：

exitSuccess >> m

-- m1 >> m2 = m1 >>= \_ -> m2
= exitSuccess >>= \_ -> m

-- exitSuccess = FreeT (return (Free ExitSuccess))
= FreeT (return (Free ExitSuccess)) >>= \_ -> m

-- use definition of (>>=) for FreeT
= FreeT $ do
    x <- runFreeT $ FreeT (return (Free ExitSuccess))
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- runFreeT (FreeT x) = x
= FreeT $ do
    x <- return (Free ExitSuccess)
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Monad Law: Left identity
-- do { y <- return x; m } = do { let y = x; m }
= FreeT $ do
    let x = Free ExitSuccess
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Substitute in 'x'
= FreeT $ do
    case Free ExitSuccess of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- First branch of case statement matches 'w' to 'ExitSuccess'
= FreeT $ do
    return (Free (fmap (>>= (\_ -> m)) ExitSuccess))

-- fmap f ExitSuccess = ExitSuccess
= FreeT $ do
    return (Free ExitSuccess)

-- do { m; } desugars to 'm'
= FreeT (return (Free ExitSuccess))

-- exitSuccess = FreeT (return (Free ExitSuccess))
= exitSuccess

証明のdoブロックはベースモナドに属していましたが、それを等式的に操作するために、ベースモナドの特定のソースコードやプロパティを使用する必要はありませんでした。私たちが知る必要がある唯一の特性は、それがモナド（任意のモナド！）であり、モナドの法則に従っているということでした。

モナドの法則のみを使用して、それを推測することができましたexitSuccess >> m = exitSuccess。それがモナド法が重要である理由です。なぜなら、それがモナドであることだけを知っているので、多形ベースのモナド上のコードについて推論することができるからです。

より一般的には、これが、型クラスには常に関連する法則（モナド法、ファンクター法、カテゴリ法など）が必要であると人々が言う理由です。これらの法則により、相談せずにその型クラスを使用するコードについて推論できるからです。その型クラスの特定のインスタンス。これらの種類の法則がなければ、元のインスタンスのソースコードを参照せずにそれについて方程式的に推論することはできないため、型クラスインターフェイスは実際には緩く結合されたインターフェイスにはなりません。

また、圏論の追加量が必要な場合は、基本モナドが多形である場合、保持するすべてのプロパティも保持するFree必要があることを簡単に証明できます。FreeT私たちがしなければならないのは、次のことを証明することだけです。

(forall m. (Monad m) => FreeT f m r) ~ Free f r

~記号は「同型」を意味します。これは、、、および：の2つの関数があることを証明する必要があることを意味しfwますbw。

fw :: (forall m . (Monad m) => FreeT f m r) -> Free f r

bw :: Free f r -> (forall m . (Monad m) => FreeT f m r)

... そのような：

fw . bw = id

bw . fw = id

これは興味深い証拠であり、演習として残しておきます。

于 2013-02-16T08:14:40.890 に答える