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)