Phép thuật hệ thống kiểu Haskell nào cho phép định nghĩa tham gia?

Question

Chức năng join tiện ích được định nghĩa là:

join :: (Monad m) => m (m a) -> m a 
join x = x >>= id 

Cho rằng loại >>= là Monad m => m a -> (a -> m b) -> m b và id là a -> a, làm thế nào có thể chức năng đó cũng được gõ như a -> m b vì nó phải nằm trong định nghĩa ở trên không? m và b trong trường hợp này là gì?

Answer 1

Các a s trong các loại cho >>= và id không nhất thiết phải giống nhau a s, vì vậy chúng ta hãy xác định lại các loại như thế này:

(>>=) :: Monad m => m a  -> (a -> m b) -> m b 
id  ::      c -> c 

Vì vậy, chúng ta có thể kết luận rằng clà giống như a sau khi tất cả, ít nhất là khi id là đối số thứ hai cho >>= ... và cũng có nghĩa là c giống với m b. Vì vậy, a cũng giống như m b. Nói cách khác:

(>>= id) :: Monad m => m (m b) ->    m b 

Answer 2

dave4420 truy cập, nhưng tôi nghĩ các nhận xét sau đây vẫn có thể hữu ích.

Có các quy tắc mà bạn có thể sử dụng để hợp lệ "ghi đè" loại thành loại khác tương thích với kiểu gốc. Những quy định liên quan đến việc thay thế tất cả các lần xuất hiện của một loại biến với một số loại khác:

• Nếu bạn có id :: a -> a, bạn có thể thay a với c và nhận id :: c -> c. Loại sau này cũng có thể được viết lại thành id :: a -> a gốc, có nghĩa là hai loại này tương đương nhau. Theo nguyên tắc chung, nếu bạn thay thế tất cả các phiên bản của biến kiểu bằng một biến kiểu khác xảy ra không có nơi nào trong bản gốc, bạn sẽ nhận được một loại tương đương.
• Bạn có thể thay thế tất cả các lần xuất hiện của biến kiểu bằng loại bê tông. Ví dụ: nếu bạn có id :: a -> a, bạn có thể viết lại số đó thành id :: Int -> Int. Tuy nhiên, sau này không thể được viết lại về bản gốc, vì vậy trong trường hợp này, bạn là chuyên loại loại.
• Thông thường hơn quy tắc thứ hai, bạn có thể thay thế tất cả các lần xuất hiện của biến loại bất kỳ loại nào, cụ thể hoặc biến. Ví dụ: nếu bạn có f :: a -> m b, bạn có thể thay thế tất cả các lần xuất hiện của a bằng m b và nhận f :: m b -> m b. Vì điều này không thể được hoàn tác, nó cũng là một chuyên môn.

Ví dụ cuối cùng cho thấy cách id có thể được sử dụng làm đối số thứ hai của >>=. Vì vậy, câu trả lời cho câu hỏi của bạn là chúng tôi có thể viết lại và lấy được các loại như sau:

1. (>>=) :: m a -> (a -> m b) -> m b  (premise) 
2. id  :: a -> a       (premise) 
3. (>>=) :: m (m b) -> (m b -> m b) -> m b (replace a with m b in #1) 
4. id  :: m b -> m b      (replace a with m b in #2) 
    . 
    . 
    . 
n. (>>= id) :: m (m b) -> m b     (indirectly from #3 and #4)