大多数情况下，effect都是用Hoare逻辑来描述的。一个Hoare三元组$\{p\}\;S\;\{q\} $， $S$ 是一段程序， $p $ 是执行这段程序的前提条件（状态）， $q$ 是执行完这段程序后的条件（状态）。然后使用这个三元组的一些规则表示语句的一些性质：
- 空语句： $\frac {} {\{p\}\;skip\;\{p\}}$
- 赋值语句： $\frac {} {\{p[u :=t]\}\;u:=t\;\{p\}}$
- 顺序语句： $\frac {\{p\}\;S_1\;\{q\}, \{q\}\;S_2\;\{r\}} {\{p\}\;S_1;\,S_2\;\{r\}}$
等等。这其实恰好是个幺半群——空语句是幺元，顺序语句是乘法。总之，用幺半群来描述作用（语句）是十分合适的。
于是用Monad来描述作用也是很自然的——Monad是自函子范畴上的幺半群。（这句话我就不解释了）
比如用m a表示带作用类型为m的程序，而m (m (m ... m a))表示一系列的作用，对应作用（语句）序列 $S_1, S_2, S_3, S_4 \dots S_n$ ：
stms :: Monad m => m (m (m (m ... m a)))
-- ^ ^ ^ ^ ^
-- | | | | ... |
-- S1 S2 S3 S4... Sn
stms = ...
然后靠join :: m (m a) -> m a将这些作用合并成一个大的作用：
oneEff :: Monad m => m a
oneEff = join (join (join .... stms))
-- (((S1; S2); S3)...; Sn)
当然也别忘了空作用pure :: a -> m a。
最能体现m (m (m (m ... m a)))表示作用序列意义的类型，莫过于Either和State了：
inc :: a -> State Int a
inc a = State $ \i -> (a, i+1)
inc3 :: State Int (State Int (State Int (State Int ())))
-- ^ ^ ^ ^
-- | | | |
-- +1s +1s +1s 0
inc3 = inc $ inc $ inc $ pure ()
execState (join $ join $ join inc3) 0 -- 3
Either就对应着异常控制流作用，请大家思考。再留给大家思考一个问题：m1是Monad，m2是Monad，m1 . m2是不是Monad呢？（这能解释为什么Monad Transformer为什么不是单纯地组合Monad）
当然我们平常用的是bind也就是(>>=)，自带合并作用的效果，不需要自己手写长串的嵌套的类型。
普通的Monad忽略了作用（语句）的前置条件和后置条件，很菜。我们可以加上，这就是Indexed Monad：
class IxMonad (m :: k -> k -> * -> *) where
ipure :: a -> m p p a
-- () -> {p} skip {p}
ijoin :: m p q (m q r a) -> m p r a
-- {p}S1{q},{q}S2{r} -> {p}S1; S2{r}
ibind :: m p q a -> (a -> m q r b) -> m p r b
对了，为了更体现Monad的“幺半群”的属性，还有一种index的方式：
class IxMonad (m :: k -> * -> *) where
type (:+:) :: k -> k -> k
type Empty :: k
ipure :: a -> m Empty a
-- 幺元
ijoin :: m i (m j a) -> m (i :+: j) a
-- 二元运算
ibind :: m i a -> (a -> m j b) -> m (i :+: j) b
indexed monad配合上dependent type可以玩出好多花样出来，比如将一个socket的状态机encode进去，这是dt中的基操，尽管这其实要多写不少“证明”。
之后围绕着monadic eff的研究可海了去了。比如
- Free Monad，将普通函子提升为一个Monad。函子内只需要定义出eff的一些atom操作就好。
- 结合data type a la carte，可以任意合并一些函子，再套上一个Free Monad，然后就得到”想要哪些操作就要哪些操作“的eff。
- mtl，利用typeclass，使得我们脱离Monad Transformer自己套洋葱的苦海*
- 。。。