MonadState, State và StateT trong Haskell

Lớp kiểu MonadState

class Monad m => MonadState s m | m -> s where
    layTrangThai :: m s
    layTrangThai = trangThai (\s -> (s, s))

    datTrangThai :: s -> m ()
    datTrangThai s = trangThai (\_ -> ((), s))

    trangThai :: (s -> (a, s)) -> m a
    trangThai f = do
      s <- layTrangThai
      let ~(a, s') = f s
      datTrangThai s'
      return a

sua :: MonadState s m => (s -> s) -> m ()
sua f = trangThai (\s -> ((), f s))

sua' :: MonadState s m => (s -> s) -> m ()
sua' f = trangThai (\s -> let s' = f s in s' `seq` ((), s'))

lay :: MonadState s m => (s -> a) -> m a
lay f = do
    s <- layTrangThai
    return (f s)

instance Monad m => MonadState s (Lazy.StateT s m) where
    layTrangThai = Lazy.layTrangThai
    datTrangThai = Lazy.datTrangThai
    trangThai = Lazy.trangThai

instance Monad m => MonadState s (Strict.StateT s m) where
    layTrangThai = Strict.layTrangThai
    datTrangThai = Strict.datTrangThai
    trangThai = Strict.trangThai

  • class Monad m => MonadState s m | m -> s where MonadState là một lớp kiểu, nó định nghĩa giao diện chung cho các Monad có tính năng State như StateT, RWST, v.v. Tính năng State ở đây là sự đóng gói của môi trường tính toán trạng thái, tức là đóng gói hàm \s -> (a, s). Lớp MonadState chứa ba hàm: layTrangThai, datTrangThai, và trangThai. layTrangThai đặt giá trị kết quả là giá trị trạng thái s, giữ nguyên giá trị trạng thái s. datTrangThai s đặt giá trị kết quả là rỗng, đặt giá trị trạng thái là s. trangThai f đóng gói hàm f vào Monad. Ngoài ra, cùng mô-đun này còn định nghĩa các hàm sua và lay. sua f đặt giá trị kết quả là rỗng, đặt giá trị trạng thái là f s. lay f đặt giá trị kết quả là f s, giữ nguyên giá trị trạng thái s.

Monad chuyển đổi StateT

newtype StateT s m a = StateT { chayStateT :: s -> m (a,s) }

instance (Monad m) => Monad (StateT s m) where
    traVe a = StateT $ \ s -> traVe (a, s)
    m >>= k  = StateT $ \ s -> do
        ~(a, s') <- chayStateT m s
        chayStateT (k a) s'

  • newtype StateT s m a = StateT { chayStateT :: s -> m (a,s) } StateT là một kiểu newtype, tức là đóng gói của một kiểu hiện có. Kiểu này có ba tham số kiểu: tham số kiểu Monad bên trong m, tham số kiểu trạng thái s, và tham số kiểu kết quả a. Kiểu StateT s m đóng gói một hàm chuyển đổi trạng thái: \s -> m (a,s'), qua trường chayStateT có thể lấy ra hàm này từ kiểu StateT. Hàm này nhận một tham số trạng thái s, sau khi tính toán (chuyển đổi) sẽ trả về một cặp giá trị được đóng gói trong Monad m bên trong: kết quả tính toán a và trạng thái mới s'.
  • instance (Monad m) => Monad (StateT s m) where Nếu m là một Monad, thì StateT s m cũng là một Monad. So sánh với định nghĩa của lớp kiểu Monad, ta thấy hàm traVe có chữ ký: traVe :: a -> StateT s m a Tương đương với a -> s -> m (a,s) Trong khi hàm bind có chữ ký: (>>=) :: StateT s m a -> (a -> StateT s m b) -> StateT s m b Tương đương với (s -> m (a,s)) -> (a -> s -> m (b,s)) -> (s -> m (b,s))
  • traVe a = StateT $ \s -> traVe (a, s) Hàm traVe đóng gói a vào hàm chuyển đổi trạng thái, hàm này đặt giá trị kết quả là a, giữ nguyên giá trị trạng thái s, sau đó đóng gói cặp giá trị này vào Monad m bên trong. Ở đây, traVe bên trái là hàm traVe của Monad StateT, còn traVe bên phải là hàm traVe của Monad m bên trong.
  • m >>= k = StateT $ \s -> do Theo chữ ký hàm, m có kiểu StateT s m a, tương đương với s -> m (a,s). Trong khi k có kiểu a -> StateT s m b, tương đương với a -> s -> m (b,s) Toán tử bind kết hợp hai hàm chuyển đổi trạng thái, kết quả cuối cùng vẫn là một hàm chuyển đổi trạng thái.
  • ~(a, s') StateT s m b, ta biết k a có kiểu StateT s m b, tức k a cũng là một Monad StateT. Ở đây, trước tiên sử dụng trường chayStateT để lấy hàm chuyển đổi trạng thái được đóng gói trong Monad StateT (k a), sau đó áp dụng nó lên giá trị trạng thái s', để nhận được một cặp giá trị được đóng gói trong Monad m bên trong: giá trị kết quả cuối cùng a' và giá trị trạng thái cuối cùng s''.
Chứng minh StateT s m tuân thủ các quy tắc Monad:
1. traVe a >>= f ≡ f a
traVe a >>= f
≡ (StateT $ \s -> traVe (a, s)) >>= f
≡ StateT (\s -> m (a, s)) >>= f
≡ StateT $ \s -> do {~(a, s') <- chayStateT (StateT (\s -> m (a, s))) s; chayStateT (f a) s'}
≡ StateT $ \s -> do {~(a, s') <- m (a, s); chayStateT (f a) s'}
≡ StateT $ \s -> do {~(a, s') <- m (a, s); chayStateT (f a) s'}
≡ StateT $ \s -> chayStateT (f a) s
≡ StateT $ chayStateT (f a)
≡ f a
2. m >>= traVe ≡ m
m = StateT (\s -> m (a, s))
m >>= traVe
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT (traVe a) s'}
≡ StateT $ \s -> do {~(a, s') <- chayStateT (StateT (\s -> m (a, s))) s; chayStateT (StateT (\s -> m (a, s))) s'}
≡ StateT $ \s -> do {~(a, s') <- (\s -> m (a, s)) s; (\s -> m (a, s)) s'}
≡ StateT $ \s -> do {~(a, s') <- m (a, s); m (a, s')}
≡ StateT $ \s -> m (a, s)
≡ m
3. (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
(m >>= f) >>= g
≡ (StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT (k a) s'}) >> g
≡ StateT $ \s -> do {~(a, s') <- chayStateT (StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT (f a) s'}) s; chayStateT (g a) s'}
≡ StateT $ \s -> do {~(a, s') <- (\s -> do {~(a, s') <- chayStateT m s; chayStateT (f a) s'}) s; chayStateT (g a) s'}
≡ StateT $ \s -> do {~(a, s') <- do {~(a, s') <- chayStateT m s; chayStateT (f a) s'}); chayStateT (g a) s'}
≡ StateT $ \s -> (chayStateT m s >>= \(a, s') -> chayStateT (f a) s') >>= \(a, s') -> chayStateT (g a) s'
m >>= (\x -> f x >>= g)
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT ((\x -> f x >>= g) a) s'}
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT (f a >>= g) s'}
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; chayStateT (StateT $ \s -> do {~(a, s') <- chayStateT (f a) s; chayStateT (g a) s'}) s'}
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; (\s -> do {~(a, s') <- chayStateT (f a) s; chayStateT (g a) s'}) s'}
≡ StateT $ \s -> do {~(a, s') <- chayStateT m s; do {~(a, s') <- chayStateT (f a) s'; chayStateT (g a) s''}}
≡ StateT $ \s -> chayStateT m s >>= \(a, s') -> (chayStateT (f a) s' >>= \(a, s'') -> chayStateT (g a) s'')
Theo quy tắc của Monad bên trong: (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
StateT $ \s -> (chayStateT m s >>= \(a, s') -> chayStateT (f a) s') >>= \(a, s') -> chayStateT (g a) s'
≡ StateT $ \s -> chayStateT m s >>= (\(a, s') -> (\(a, s') -> chayStateT (f a) s')) (a, s') >>= \(a, s') -> chayStateT (g a) s'
≡ StateT $ \s -> chayStateT m s >>= \(a, s') -> (chayStateT (f a) s' >>= \(a, s') -> chayStateT (g a) s')

Hàm nâng lên (lift)

instance MonadTrans (StateT s) where
    nangLen m = StateT $ \ s -> do
        a <- m
        return (a, s)

Chứng minh định nghĩa hàm nangLen trong StateT tuân thủ các quy tắc của hàm nâng lên.
1. nangLen . traVe ≡ traVe
nangLen . traVe $ a
≡ nangLen (m a)
≡ StateT $ \s -> do {a <- m a; return (a, s)}
≡ StateT $ \s -> m (a, s)
≡ traVe a
2. nangLen (m >>= f) ≡ nangLen m >>= (nangLen . f)
Giả sử m = n a và f a = n b
Vậy m >>= f = n b
nangLen (m >>= f)
≡ nangLen (n b)
≡ StateT $ \s -> do {a <- n b; return (a, s)}
≡ StateT $ \s -> n (b, s)
nangLen m >>= (nangLen . f)
≡ (StateT $ \s -> do {a <- n a; return (a, s)}) >>= (\x -> StateT $ \s -> do {a <- f x; return (a, s)})
≡ (StateT $ \s -> n (a s)) >>= (\x -> StateT $ \s -> do {a <- f x; return (a, s)})
≡ StateT $ \s -> do {chayStateT (StateT $ \s -> do {a <- f a; return (a, s)}) s}
≡ StateT $ \s -> do {chayStateT (StateT $ \s -> do {a <- n b; return (a, s)}) s}
≡ StateT $ \s -> do {chayStateT (StateT $ \s -> n (b s)) s}
≡ StateT $ \s -> n (b s)

StateT là Functor cũng là Applicative

instance (Functor m) => Functor (StateT s m) where
    fmap f m = StateT $ \ s ->
        fmap (\ ~(a, s') -> (f a, s')) $ chayStateT m s

instance (Functor m, Monad m) => Applicative (StateT s m) where
    tinhToan a = StateT $ \ s -> traVe (a, s)
    StateT mf <*> StateT mx = StateT $ \ s -> do
        ~(f, s') <- mf s
        ~(x, s'') <- mx s'
        return (f x, s'')
    m *> k = m >>= \_ -> k

StateT là Alternative cũng là MonadPlus

instance (Functor m, MonadPlus m) => Alternative (StateT s m) where
    rong = StateT $ \ _ -> mzero
    StateT m <|> StateT n = StateT $ \ s -> m s `mplus` n s

instance (MonadPlus m) => MonadPlus (StateT s m) where
    mzero       = StateT $ \ _ -> mzero
    StateT m `mplus` StateT n = StateT $ \ s -> m s `mplus` n s

Các hàm của Monad chuyển đổi StateT

layTrangThai :: (Monad m) => StateT s m s
layTrangThai = trangThai $ \ s -> (s, s)

datTrangThai :: (Monad m) => s -> StateT s m ()
datTrangThai s = trangThai $ \ _ -> ((), s)

sua :: (Monad m) => (s -> s) -> StateT s m ()
sua f = trangThai $ \ s -> ((), f s)

sua' :: (Monad m) => (s -> s) -> StateT s m ()
sua' f = do
    s <- layTrangThai
    datTrangThai $! f s

lay :: (Monad m) => (s -> a) -> StateT s m a
lay f = trangThai $ \ s -> (f s, s)

trangThai :: (Monad m) => (s -> (a, s)) -> StateT s m a
trangThai f = StateT (traVe . f)

danhGiaStateT :: (Monad m) => StateT s m a -> s -> m a
danhGiaStateT m s = do
    ~(a, _) <- chayStateT m s
    return a

thucThiStateT :: (Monad m) => StateT s m a -> s -> m s
thucThiStateT m s = do
    ~(_, s') <- chayStateT m s
    return s'

bieuDoiStateT :: (m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
bieuDoiStateT f m = StateT $ f . chayStateT m

voiTrangThaiT :: (s -> s) -> StateT s m a -> StateT s m a
voiTrangThaiT f m = StateT $ chayStateT m . f

danhGiaStateT m s thực hiện tính toán trạng thái với Monad m sử dụng giá trị trạng thái ban đầu s, sau đó trả về giá trị kết quả cuối cùng a'. thucThiStateT m s thực hiện tính toán trạng thái với Monad m sử dụng giá trị trạng thái ban đầu s, sau đó trả về giá trị trạng thái cuối cùng s'. bieuDoiStateT f m sau khi thực hiện tính toán trạng thái với Monad m, áp dụng hàm f vào giá trị kết quả và giá trị trạng thái. voiTrangThaiT f m trước khi thực hiện tính toán trạng thái với Monad m, áp dụng hàm f vào giá trị trạng thái ban đầu.

Prelude Control.Monad.State> chayStateT (traVe 15) 1
(15,1)
Prelude Control.Monad.State> chayStateT layTrangThai 1
(1,1)
Prelude Control.Monad.State> chayStateT (datTrangThai 3) 1
((),3)
Prelude Control.Monad.State> chayStateT (sua (+1)) 1
((),2)
Prelude Control.Monad.State> chayStateT (lay (+1)) 1
(2,1)
Prelude Control.Monad.State> danhGiaStateT (lay (+1)) 1
2
Prelude Control.Monad.State> thucThiStateT (lay (+1)) 1
1
Prelude Control.Monad.State> chayStateT (do datTrangThai 3; traVe 15) 1
(15,3)
Prelude Control.Monad.State> chayStateT (datTrangThai 3 >> traVe 15) 1
(15,3)

Monad State

type State s = StateT s Identity

chayState :: State s a -> s -> (a, s)
chayState m = chayIdentity . chayStateT m

danhGiaState :: State s a -> s -> a
danhGiaState m s = fst (chayState m s)

thucThiState :: State s a -> s -> s
thucThiState m s = snd (chayState m s)

bieuDoiState :: ((a, s) -> (b, s)) -> State s a -> State s b
bieuDoiState f = bieuDoiStateT (Identity . f . chayIdentity)

voiTrangThai :: (s -> s) -> State s a -> State s a
voiTrangThai = voiTrangThaiT

Monad State là một trường hợp đặc biệt của Monad chuyển đổi StateT.

Hiểu về Monad State

Giả sử có một thực thể f của Monad State như sau:

f :: State s a

Chúng ta có thể hiểu một cách đơn giản rằng f này là một hàm thông thường với tham số kiểu s và giá trị trả về kiểu a.

Trong hàm f này, "tham số" s có thể:

  • Được truyền ngầm cho các hàm khác thông qua việc gọi các hàm sua hoặc lay.
  • Được đọc bằng cách gọi hàm layTrangThai, được đặt bằng cách gọi hàm datTrangThai, và được sửa đổi bằng cách gọi hàm sua.
  • Được phản ánh như "giá trị trả về" a thông qua việc gọi hàm lay hoặc lay.

Trong hàm f này, "giá trị trả về" a có thể:

  • Được đặt gián tiếp thông qua việc gọi hàm lay hoặc lay.
  • Được đặt trực tiếp thông qua việc gọi hàm traVe.
  • Được đặt thành rỗng bằng cách gọi hàm sua hoặc datTrangThai.

Tại sao chúng ta phải sử dụng monad trạng thái thay vì truyền trạng thái trực tiếp?

Ví dụ ứng dụng

import Control.Monad.State

type NganXep = [Int]

layDau :: State NganXep Int  
layDau = trangThai $ \(x:xs) -> (x,xs)  

them :: Int -> State NganXep ()  
them a = trangThai $ \xs -> ((),a:xs)  

xuLyNganXep :: State NganXep Int  
xuLyNganXep = do  
    them 3  
    a <- layDau  
    layDau  

lamVoiNganXep :: State NganXep ()  
lamVoiNganXep = do  
    a <- layDau  
    if a == 5  
        then them 5  
        else do  
            them 3  
            them 8  

themNganXepNua :: State NganXep ()  
themNganXepNua = do  
    a <- xuLyNganXep  
    if a == 100  
        then lamVoiNganXep  
        else traVe ()

nganXepNganXep :: State NganXep ()  
nganXepNganXep = do  
    trangThaiHienTai <- layTrangThai  
    if trangThaiHienTai == [1,2,3]  
        then datTrangThai [8,3,1]  
        else datTrangThai [9,2,1]  

main = do
    print $ chayState xuLyNganXep [5,8,2,1]
    print $ chayState lamVoiNganXep [9,0,2,1,0]
    print $ chayState nganXepNganXep [9,0,2,1,0]
    
{-
(5,[8,2,1])
((),[8,3,0,2,1,0])
((),[9,2,1])
-}

Thẻ: Haskell MonadState State StateT functional programming

Đăng vào ngày 17 tháng 6 lúc 01:41