dramforever

coding, thoughts and stuff irl

有关 monad 的一些想法 (3)

2017-01-23
{-# LANGUAGE DeriveFunctor #-}
import Control.Monad

Monad 的树型结构

我们来看一个二叉树

data F a = E a | Fork (F a) (F a)
         deriving (Functor)

它肯定是个 FunctorApplicativepure 也好办。

instance Applicative F where
    pure = E
    (<*>) = ap

我们 claim,F 也是个 Monad(>>=) 要做什么呢?先随便写写吧。

instance Monad F where

E 好像是别无选择的

    E a >>= f = f a

Fork 的话随便写写,一下就想到了这个

    Fork u v >>= f = Fork (u >>= f) (v >>= f)

写完了?但是这个靠谱么?

Monad 定律

如果用 do 写出来,看得更清楚

在命令式编程里面,你可能已经习惯于对程序做这种变换了。

在 Haskell 里,这种变换是可以出来的。就用 Monad 定律。

我们来验证一下 F 符合 Monad 定律

第一条:

return a >>= f
= E a >>= f
= f a

第二条:

m >>= return = m

对 m 用归纳法

E a >>= return = return a = E a

给定 u >>= return = uv >>= return = v,我们有

Fork u v >>= return
= Fork (u >>= return) (v >>= return)
= Fork u v

第三条

(m >>= f) >>= g

对 m 用归纳法

(E a >>= f) >>= g
= f a >>= g (由 >>= 定义)
= E a >>= (\x -> f x >>= g) (由 >>= 定义反推)

给定 uv 符合条件,我们有

(Fork u v >>= f) >>= g
= Fork (u >>= f) (v >>= f) >>= g (由 >>= 定义)
= Fork ((u >>= f) >>= g) ((v >>= f) >>= g) (由 >>= 定义)
= Fork (u >>= (\x -> f x >>= g)) (v >>= (\x -> f x >>= g)) (由归纳假设)
= Fork u v >>= (\x -> f x >>= g) (由 >>= 定义反推)

感觉好像重复写了好多东西啊。有没有更一般的结构?

Free monad

data Free f a
    = W (f (Free f a))
    | Z a
    deriving (Functor)

如果我们定义

data Pair a = Pair a a
            deriving (Functor)

那么 Free Pair 就和 F 是等效的了

Fork (Fork (E 2) (E 3)) (E 5)

对应

W (Bin (W (Bin (Z 2) (Z 3))) (Z 5))

之前的这么一步

Fork u v >>= f = Fork (u >>= f) (v >>= f)

u v 包在一个 Pair 里之后,后面的那个 u >>= fv >>= f 就可以变成 fmap (>>= f)

instance Functor f => Applicative (Free f) where
    pure = Z
    (<*>) = ap
instance Functor f => Monad (Free f) where
    Z a >>= f = f a
    W fa >>= f = W (fmap (>>= f) fa)

练习

代码在此