Ghi chú học ngôn ngữ Haskell (30): MonadCont, Cont, và ContT

Lớp kiểu MonadCont

class Monad m => MonadCont m where
    callCC :: ((a -> m b) -> m a) -> m a
instance MonadCont (ContT r m) where
    callCC = ContT.callCC

  • class Monad m => MonadCont m where MonadCont là một lớp kiểu, nó định nghĩa giao diện chung cho các Monad như ContT đóng gói hàm CPS (Continuation Passing Style). MonadCont chỉ chứa một hàm duy nhất là callCC, cung cấp chức năng kiểm soát luồng xử lý rõ ràng cho hàm CPS.

  • instance MonadCont (ContT r m) where callCC = ContT.callCC Đối với Monad chuyển đổi ContT, định nghĩa của hàm callCC được cung cấp bởi module ContT. Lưu ý rằng toán tử ở đây không phải là hợp thành hàm mà là giới hạn tên.

Transformer Monad ContT

newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }
instance Monad (ContT r m) where
    return x = ContT ($ x)
    m >>= k  = ContT $ \c -> runContT m (\x -> runContT (k x) c)

  • newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r } ContT là một kiểu newtype, đóng gói một kiểu hiện có. Kiểu này có ba tham số kiểu: tham số kiểu Monad nội bộ m, tham số kiểu kết quả trung gian a, và tham số kiểu kết quả cuối cùng r. ContT r m a đóng gói một hàm CPS: \k -> m r (thường có dạng \k -> k a), và thông qua trường runContT, chúng ta có thể lấy hàm này ra khỏi kiểu ContT.

  • instance Monad (ContT r m) where ContT r m là một Monad. So sánh với định nghĩa của lớp kiểu Monad, ta thấy chữ ký của hàm return là: return :: a -> ContT r m a Tương đương với a -> (a -> m r) -> m r Chữ ký của toán tử bind (>>=) là: (>>=) :: ContT r m a -> (a -> ContT r m b) -> ContT r m b Tương đương với (a -> m r) -> m r -> (a -> (b -> m r) -> m r) -> (b -> m r) -> m r

  • return x = ContT ($ x) Hàm return đóng gói giá trị x kiểu a vào Monad ContT. return x = ContT $ \k -> k x Ở đây x có kiểu a, k có kiểu a -> m r, k x có kiểu m r, \k -> k x có kiểu (a -> m r) -> m r, ContT $ \k -> k x (tức ContT ($ x)) có kiểu ContT r m a.

  • m >>= k = ContT $ \c -> runContT m (\x -> runContT (k x) c) Toán tử bind kết hợp hai Monad Cont đã đóng gói hàm CPS, kết quả vẫn là một Monad Cont đã đóng gói hàm CPS. Giả sử m = ContT c1 với c1 f1 = f1 a, và k = \a -> ContT c2 với c2 f2 = f2 b. Toán tử bind hoạt động như sau: Đầu tiên, dùng runContT m để lấy hàm CPS c1 ra từ toán tử trái m, hàm c1 sẽ truyền kết quả tính toán kiểu a là x cho hàm f1, tức là hàm (\x -> runContT (k x) c), nhận được kết quả runContT (k x) c. Sau đó, runContT (k x) lại lấy hàm CPS c2 ra từ toán tử phải k. Hàm c2 sẽ truyền kết quả tính toán kiểu b là y cho hàm f2, tức là hàm ngoài cùng c, nhận được kết quả cuối cùng c y. Cuối cùng, thông qua ContT $ \c -> c y, kết quả tính toán được đóng gói lại vào Monad ContT.

Chứng minh ContT tuân thủ các quy tắc Monad:
1. return a >>= f ≡ f a
return a >>= f
≡ ContT (\k -> k a) >>= f
≡ ContT $ \c -> runContT (ContT (\k -> k a)) (\x -> runContT (f x) c)
≡ ContT $ \c -> (\k -> k a) (\x -> runContT (f x) c)
≡ ContT $ \c -> (\x -> runContT (f x) c) a
≡ ContT $ \c -> runContT (f a) c
≡ ContT $ runContT (f a)
≡ f a

2. m >>= return ≡ m
m >>= return
≡ ContT $ \c -> runContT m (\x -> runContT (return x) c)
≡ ContT $ \c -> runContT m (\x -> runContT (ContT $ \k -> k x) c)
≡ ContT $ \c -> runContT m (\x -> (\k -> k x) c)
≡ ContT $ \c -> runContT m (\x -> c x)
≡ ContT $ \c -> runContT m c
≡ ContT $ runContT m
≡ m

3. (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
(m >>= f) >>= g
≡ (ContT $ \c -> runContT m (\x -> runContT (f x) c)) >>= g
≡ ContT $ \c -> runContT (ContT $ \c -> runContT m (\x -> runContT (f x) c)) (\x -> runContT (g x) c)
≡ ContT $ \c -> (\c -> runContT m (\x -> runContT (f x) c)) (\x -> runContT (g x) c)
≡ ContT $ \c -> runContT m (\x -> runContT (f x) (\x -> runContT (g x) c))

m >>= (\x -> f x >>= g)
≡ ContT $ \c -> runContT m (\x -> runContT ((\x -> f x >>= g) x) c)
≡ ContT $ \c -> runContT m (\x -> runContT (f x >>= g) c)
≡ ContT $ \c -> runContT m (\x -> runContT (ContT $ \c -> runContT (f x) (\x -> runContT (g x) c)) c)
≡ ContT $ \c -> runContT m (\x -> (\c -> runContT (f x) (\x -> runContT (g x) c)) c)
≡ ContT $ \c -> runContT m (\x -> runContT (f x) (\x -> runContT (g x) c))

Hàm lift và liftIO

instance MonadTrans (ContT r) where
    lift m = ContT (m >>=)

instance (MonadIO m) => MonadIO (ContT r m) where
    liftIO = lift . liftIO

Hàm lift m đóng gói giá trị từ Monad nội bộ m vào Monad ContT. lift m = ContT $ \k -> m >>= k Ở đây m có kiểu m a, k có kiểu a -> m r, m >>= k có kiểu m r, \k -> m >>= k có kiểu (a -> m r) -> m r, ContT $ \k -> m >>= k (tức ContT (m >>=)) có kiểu ContT r m a.

Chứng minh định nghĩa hàm lift trong ContT tuân thủ các quy tắc của lift.
1. lift . return ≡ return
lift . return $ a
≡ lift (m a)
≡ ContT (m a >>=)
≡ ContT $ \k -> m a >>= k
≡ ContT $ \k -> k a
≡ return a

2. lift (m >>= f) ≡ lift m >>= (lift . f)
Giả sử m = n a và f a = n b
Khi đó m >>= f = n b
lift (m >>= f)
≡ lift (n b)
≡ ContT (n b >>=)
≡ ContT $ \k -> n b >>= k
≡ ContT $ \k -> k b
≡ return b

lift m >>= (lift . f)
≡ ContT (n a >>=) >>= \x -> ContT (f x >>=)
≡ ContT (\k -> k a) >>= \x -> ContT (\k -> f x >>= k)
≡ ContT $ \c -> runContT $ ContT (\k -> k a) (\x -> runContT $ ContT (\k -> f x >>= k) c)
≡ ContT $ \c -> (\k -> k a) (\x -> (\k -> f x >>= k) c)
≡ ContT $ \c -> (\x -> (\k -> f x >>= k) c) a
≡ ContT $ \c -> (\k -> f a >>= k) c
≡ ContT $ \c -> (\k -> n b >>= k) c
≡ ContT $ \c -> (\k -> k b) c
≡ ContT $ \c -> c b
≡ return b

Prelude Control.Monad.Trans.Cont Control.Monad.Trans> f a = if even a then Just (a `div` 2) else Nothing
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> c = lift . f :: Int -> ContT Int Maybe Int
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> runContT (c 3) return
Nothing
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> runContT (c 4) f
Just 1
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> c = lift getLine :: ContT r IO String
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> runContT c print
abc
"abc"

Hàm callCC

callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a
callCC f = ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c

CallCC là viết tắt của "Call With Current Continuation" (gọi với hàm tiếp tục hiện tại), nó cung cấp cơ thoát cho Monad ContT. CallCC có một tham số f, CallCC f trả về một Monad ContT. f có kiểu (a -> ContT r m b) -> ContT r m a, tức f là một hàm có kiểu trả về giống với CallCC f, đều là Monad ContT. f thường có dạng \exit -> do ....

Prelude Control.Monad.Trans.Cont Control.Monad.Trans> runContT (callCC (\exit -> exit 1) :: ContT Int Maybe Int) return
Just 1
Prelude Control.Monad.Trans.Cont Control.Monad.Trans> runContT (callCC (\exit -> do{exit 1; return 2}) :: ContT Int Maybe Int) return
Just 1

Khi tham số của CallCC có dạng \exit -> do {...; exit a; ...}, Monad ContT được trả về sẽ bỏ qua các xử lý sau exit a, và truyền a ra hàm bên ngoài một cách vô điều kiện. Hãy xem hàm CallCC thực hiện điều này như thế nào.

  • callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a callCC f = ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c có kiểu ContT r m a \c -> runContT (f (\x -> ContT $ \_ -> c x)) c có kiểu (a -> m r) -> m r c có kiểu a -> m r, runContT (f (\x -> ContT $ \_ -> c x)) có kiểu (a -> m r) -> m r, f (\x -> ContT $ \_ -> c x) có kiểu ContT r m a, f có kiểu (a -> ContT r m b) -> ContT r m a, \x -> ContT $ \_ -> c x có kiểu a -> ContT r m b, x có kiểu a, ContT $ \_ -> c x có kiểu ContT r m b, \_ -> c x có kiểu (b -> m r) -> m r, _ có kiểu b -> m r, c x có kiểu m r.

  • callCC f = ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c Giả sử f = \exit -> exit a >>= k. callCC f với f = \exit -> exit a >>= k = ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c = ContT $ \c -> runContT ((\exit -> exit a >>= k) (\x -> ContT $ \_ -> c x)) c = ContT $ \c -> runContT ((\x -> ContT $ \_ -> c x) a >>= k) c = ContT $ \c -> runContT ((ContT $ \_ -> c a) >>= k) c

  • m >>= k = ContT $ \c -> runContT m (\x -> runContT (k x) c) (ContT $ \_ -> c a) >>= k = ContT $ \c -> runContT (ContT $ \_ -> c a) (\x -> runContT (k x) c) = ContT $ \c -> (\_ -> c a) (\x -> runContT (k x) c) = ContT $ \c -> c a

  • callCC f với f = \exit -> exit a >>= k = ContT $ \c -> runContT ((ContT $ \_ -> c a) >>= k) c = ContT $ \c -> runContT (ContT $ \c -> c a) c = ContT $ \c -> (\c -> c a) c = ContT $ \c -> c a

  • callCC f = ContT $ \c -> runContT (f (\x -> ContT $ \_ -> c x)) c Giả sử f = \exit -> exit a >>= k >>= h. f = \exit -> exit a >>= k >>= h = \exit -> exit a >>= (\x -> k x >>= h) = \exit -> exit a >>= k' với k' = \x -> k x >>= h callCC f với f = \exit -> exit a >>= k >>= h = callCC f với f = \exit -> exit a >>= k' với k' = \x -> k x >>= h = ContT $ \c -> c a

Từ quá trình suy luận trên, ta thấy khi tham số của CallCC có dạng \exit -> do {...; exit a; ...}, Monad ContT được trả về thực sự sẽ bỏ qua các xử lý sau exit a, và truyền a ra hàm bên ngoài một cách vô điều kiện.

Các hàm khác của transformer Monad ContT

evalContT :: (Monad m) => ContT r m r -> m r
evalContT m = runContT m return

mapContT :: (m r -> m r) -> ContT r m a -> ContT r m a
mapContT f m = ContT $ f . runContT m

withContT :: ((b -> m r) -> (a -> m r)) -> ContT r m a -> ContT r m b
withContT f m = ContT $ runContT m . f

resetT :: (Monad m) => ContT r m r -> ContT r' m r
resetT = lift . evalContT

shiftT :: (Monad m) => ((a -> m r) -> ContT r m r) -> ContT r m a
shiftT f = ContT (evalContT . f)

liftLocal :: (Monad m) => m r' -> ((r' -> r') -> m r -> m r) ->
    (r' -> r') -> ContT r m a -> ContT r m a
liftLocal ask local f m = ContT $ \c -> do
    r <- ask
    local f (runContT m (local (const r) . c))

Monad Cont

cont :: ((a -> r) -> r) -> Cont r a
cont f = ContT (\c -> Identity (f (runIdentity . c)))

runCont :: Cont r a  -> (a -> r)  -> r
runCont m k = runIdentity (runContT m (Identity . k))

evalCont :: Cont r r -> r
evalCont m = runIdentity (evalContT m)

mapCont :: (r -> r) -> Cont r a -> Cont r a
mapCont f = mapContT (Identity . f . runIdentity)

withCont :: ((b -> r) -> (a -> r)) -> Cont r a -> Cont r b
withCont f = withContT ((Identity .) . f . (runIdentity .))

reset :: Cont r r -> Cont r' r
reset = resetT

shift :: ((a -> r) -> Cont r r) -> Cont r a
shift f = shiftT (f . (runIdentity .))

Cont là một trường hợp đặc biệt của ContT (transformer).

Ví dụ ứng dụng

import Control.Monad.Trans.Cont
import Control.Monad (when)

tinhTong :: Int -> Int -> Int
tinhTong x y = x + y

binhPhuong :: Int -> Int
binhPhuong x = x * x

tinhTong_cont :: Int -> Int -> Cont r Int
tinhTong_cont x y = return (tinhTong x y)

binhPhuong_cont :: Int -> Cont r Int
binhPhuong_cont x = return (binhPhuong x)

pythagoras_cont :: Int -> Int -> Cont r Int
pythagoras_cont x y = do
    x_binhPhuong <- binhPhuong_cont x
    y_binhPhuong <- binhPhuong_cont y
    tinhTong_cont x_binhPhuong y_binhPhuong

pythagoras_cont' :: Int -> Int -> Cont r Int
pythagoras_cont' x y = callCC $ \thoat -> do
    when (x < 0 || y < 0) $ thoat (-1)
    x_binhPhuong <- binhPhuong_cont x
    y_binhPhuong <- binhPhuong_cont y
    tinhTong_cont x_binhPhuong y_binhPhuong

main = do
    runCont (pythagoras_cont 3 4) print -- 25
    runCont (pythagoras_cont' 3 4) print -- 25
    runCont (pythagoras_cont' (-3) 4) print -- -1

Monad Cont trong Haskell hoạt động như thế nào và tại sao?

Thẻ: Haskell Monad Continuation functional programming MonadCont

Đăng vào ngày 8 tháng 6 lúc 18:56

Thẻ Phổ Biến

©2026 Thành phố Cuồng loạn