Chức năng kiểm tra Haskell STM trả về không xác định

Question

Có lý do chính đáng nào khiến chức năng check trong thư viện Contol.Concurent.STM có loại Bool -> STM a và trả về undefined về thành công chứ không phải loại Bool -> STM()? Cách nó được thực hiện kiểm tra loại sẽ chính thức biên dịch một khối làm kết thúc với check foo chỉ để thất bại trong thời gian chạy với *** Exception: Prelude.undefined.

Answer 1

Có vẻ như đó là định nghĩa trình giữ chỗ cho GHC PrimOp, như "định nghĩa" seq _ y = y được thay thế bởi trình biên dịch bằng mã thực thi nguyên thủy thực tế. Các PrimOp implementation of check mất một biểu thức và thêm nó vào một danh sách toàn cầu của bất biến như mô tả trong STM invariants paper.

Dưới đây là một ví dụ siêu giả tạo sửa đổi từ giấy để phù hợp với kiểu mới của check:

import Control.Concurrent.STM 

data LimitedTVar = LTVar { tvar :: TVar Int 
         , limit :: Int 
         } 

newLimitedTVar :: Int -> STM LimitedTVar 
newLimitedTVar lim = do 
    tv <- newTVar 0 
    return $ LTVar tv lim 

incrLimitedTVar :: LimitedTVar -> STM() 
incrLimitedTVar (LTVar tv lim) = do 
    val <- readTVar $ tv 
    let val' = val + 1 
    check (val' <= lim) 
    writeTVar tv val' 

test :: STM() 
test = do 
    ltv <- newLimitedTVar 2 
    incrLimitedTVar ltv -- should work 
    incrLimitedTVar ltv -- should work still 
    incrLimitedTVar ltv -- should fail; we broke the invariant 

Thực tế, điều này sẽ có ích để khẳng định bất biến về trạng thái chia sẻ nơi không những khẳng định có thể là một dấu hiệu của sự mâu thuẫn tạm thời. Sau đó bạn có thể muốn thử lại với kỳ vọng về sự bất biến đó trở thành sự thật một lần nữa, nhưng kể từ khi ví dụ này kéo dài vĩnh viễn phá vỡ bất biến, nó chỉ gọi retry mãi mãi và xuất hiện để treo. Kiểm tra bài báo để biết các ví dụ tốt hơn nhiều, nhưng hãy nhớ rằng loại đã thay đổi kể từ khi xuất bản.