Haskell语言学习笔记（26）Identity, IdentityT

Identity Monad

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap     = coerce

instance Applicative Identity where
    pure     = Identity
    (<*>)    = coerce

instance Monad Identity where
    m >>= k  = k (runIdentity m)

• newtype Identity a = Identity { runIdentity :: a }
  Identity 类型是个 newtype，也就是对现有类型的封装。该类型只有一个类型参数 a。
  Identity a 封装了一个值：a，用 runIdentity 字段可以取出这个值。
  Identity 是一个用于占位的 Monad。

• instance Monad Identity where
  对比 Monad 类型类的定义，可知 return 函数的类型签名为：
  return :: Identity a
  而 bind 函数的类型签名为：
  (>>=) :: a -> (a -> Identity b) -> Identity b

• m >>= k = k (runIdentity m)

证明 Identity 符合Monad法则：  
1. return a >>= f ≡ f a
return a >>= f ≡ Identity a >>= f ≡ f (runIdentity (Identity a)) ≡ f a   
2. m >>= return ≡ m
m >>= return ≡ (Identity a) >> Identity ≡ Identity (runIdentity (Identity a)) ≡ Identity a ≡ m  
3. (m >>= f) >>= g ≡ m >>= (x -> f x >>= g)
(m >>= f) >>= g
≡ ((Identity a) >>= f) >>= g
≡ f (runIdentity (Identity a)) >> = g
≡ f a >> g
m >>= (x -> f x >>= g)  
≡ (Identity a) >>= (x -> f x >>= g)  
≡ (x -> f x >>= g) (runIdentity (Identity a))
≡ (x -> f x >>= g) a
≡ f a >> g

IdentityT Monad转换器

newtype IdentityT f a = IdentityT { runIdentityT :: f a }

instance (Monad m) => Monad (IdentityT m) where
    return = IdentityT . return
    m >>= k = IdentityT $ runIdentityT . k =<< runIdentityT m

instance MonadTrans IdentityT where
    lift = IdentityT

instance (MonadIO m) => MonadIO (IdentityT m) where
    liftIO = IdentityT . liftIO

• newtype IdentityT f a = IdentityT { runIdentityT :: f a }
  IdentityT 类型是个 newtype，也就是对现有类型的封装。该类型有两个类型参数：内部 Monad 类型参数 f，以及值类型参数 a。
  IdentityT f 类型封装了一个封装在内部 Monad f 中的值：f a，用 runIdentity 字段可以取出这个值。
  Identity 是一个用于占位的 Monad转换器。

• instance (Monad m) => Monad (IdentityT m) where
  如果 m 是个 Monad，那么 IdentityT m 也是一个 Monad。
  对比 Monad 类型类的定义，可知 return 函数的类型签名为：
  return :: IdentityT m a
  而 bind 函数的类型签名为：
  (>>=) :: a -> (a -> IdentityT m b) -> IdentityT m b

• m >>= k = IdentityT $ runIdentityT . k =<< runIdentityT m

证明 IdentityT 符合Monad法则：  
1. return a >>= f ≡ f a
return a >>= f
≡ (IdentityT . return) a >>= f
≡ IdentityT (m a) >>= f
≡ IdentityT $ runIdentityT . f =<< runIdentityT (IdentityT (m a))
≡ IdentityT $ runIdentityT . f =<< m a
≡ IdentityT $ runIdentityT (f a)
≡ f a
2. m >>= return ≡ m
假设 m = IdentityT (n a)
m >>= return
≡ IdentityT $ runIdentityT . return =<< runIdentityT m
≡ IdentityT $ runIdentityT . (IdentityT . return) =<< runIdentityT (IdentityT (n a))
≡ IdentityT $ runIdentityT . (IdentityT . return) =<< n a
≡ IdentityT $ runIdentityT (IdentityT (n a))
≡ IdentityT (n a) ≡ m  
3. (m >>= f) >>= g ≡ m >>= (x -> f x >>= g)
(m >>= f) >>= g
≡ (IdentityT $ runIdentityT . f =<< runIdentityT m) >>= g
≡ IdentityT $ runIdentityT . g =<< runIdentityT (IdentityT $ runIdentityT . f =<< runIdentityT m)
≡ IdentityT $ runIdentityT . g =<< (runIdentityT . f =<< runIdentityT m)
≡ IdentityT $ (runIdentityT m >>= runIdentityT . f) >>= runIdentityT . g
m >>= (x -> f x >>= g)  
≡ IdentityT $ runIdentityT . (x -> f x >>= g) =<< runIdentityT m
≡ IdentityT $ runIdentityT . (x -> IdentityT $ runIdentityT . g =<< runIdentityT (f x)) =<< runIdentityT m
≡ IdentityT $ (x -> runIdentityT $ IdentityT $ runIdentityT . g =<< runIdentityT (f x)) =<< runIdentityT m
≡ IdentityT $ (x -> runIdentityT . g =<< runIdentityT (f x)) =<< runIdentityT m
≡ IdentityT $ runIdentityT m >>= (x -> runIdentityT (f x) >>= runIdentityT . g)
根据内部 Monad 的法则：(m >>= f) >>= g ≡ m >>= (x -> f x >>= g)
IdentityT $ (runIdentityT m >>= runIdentityT . f) >>= runIdentityT . g
≡ IdentityT $ runIdentityT m >>= (x -> (runIdentityT . f) x >>= runIdentityT . g)
≡ IdentityT $ runIdentityT m >>= (x -> runIdentityT (f x) >>= runIdentityT . g)

证明 StateT 中 lift 函数的定义符合 lift 的法则。
1. lift . return ≡ return
lift . return $ a
≡ IdentityT (m a)
≡ return a
2. lift (m >>= f) ≡ lift m >>= (lift . f)
假设 m = n a 并且 f a = n b
于是 m >>= f = n b
lift (m >>= f)
≡ lift (n b)
≡ IdentityT (n b)
lift m >>= (lift . f)
≡ IdentityT (n a) >>= (x -> lift . f $ x)
≡ IdentityT $ runIdentityT . IdentityT . f =<< runIdentityT (IdentityT (n a))
≡ IdentityT $ n a >>= f
≡ IdentityT (f a)
≡ IdentityT (n b)