Hạn chế trong chữ ký của loại

Question

là gì Nếu tôi kiểm tra việc kind của Maybe tôi có được điều này:

λ> :k Maybe 
Maybe :: * -> * 

Bây giờ, nếu tôi kiểm tra các loại Monad tôi có được điều này:

λ> :k Monad 
Monad :: (* -> *) -> Constraint 

là gì Constraint và tại sao nó là cần thiết? Tại sao không chỉ * -> * này?

Answer 1

Không giống như Maybe, Monad không phải là loại; nó là typeclass.

Cũng vậy với typeclasses khác:

Num :: * -> Constraint 
Functor :: (* -> *) -> Constraint 
Bifunctor :: (* -> * -> *) -> Constraint 

đâu * đại diện cho các loại bê tông (như Bool hoặc Int), -> đại diện cho các loại cao kinded (như Maybe), và Constraint đại diện cho ý tưởng một ràng buộc kiểu. Đây là lý do tại sao:

---

Như chúng ta biết chúng ta không thể tạo ra một chữ ký như thế này:

return :: a -> Monad a -- This is nonsense! 

Vì Monad nên được sử dụng như một chế, để nói rằng, 'này phải một đơn nguyên với công việc ':

return :: (Monad m) => a -> m a 

chúng tôi làm điều này vì chúng ta biết rằng return chưa thể làm việc trên bất kỳ loại cũ m, vì vậy chúng tôi de phạt hành vi của return đối với các loại khác nhau dưới tên Monad. Nói cách khác, không có điều duy nhất có thể được gọi là Monad, nhưng chỉ có hành vi có thể được gọi là Monadic.

Vì lý do này, chúng tôi đã tạo ra ràng buộc loại này, nói rằng chúng ta phải xác định trước một cái gì đó như một Monad để sử dụng chức năng này. Đây là lý do tại sao loại Monad là (* -> *) -> Constraint - bản thân nó không phải là một loại!

---

Maybe là phiên bản Monad. Điều này có nghĩa là một nơi nào đó, ai đó đã viết:

instance Monad Maybe where 
    (>>=) = ... -- etc 

... và xác định cách Maybe sẽ hoạt động như một Monad. Đây là lý do tại sao chúng tôi có thể sử dụng Maybe với các chức năng hoặc loại có ràng buộc tiền tố Monad m => .... Về cơ bản, đây là nơi xác định ràng buộc được áp dụng bởi Monad.

Answer 2

Constraint là loại ví dụ: Show Int, Monad Maybe và Monoid [a]. Nói chung, đó là loại mọi thứ có thể xảy ra ở bên trái của => trong chú thích loại.

Bây giờ kể từ

Show Int :: Constraint 

và Int là một loại, tức là

Int :: * 

chúng ta có thể gán một loại chức năng để Show như sau

Show :: * -> Constraint 
      ^-- the result kind 
     ^-- the kind of Int 

Trong trường hợp của bạn nó chỉ xảy ra rằng một số Monad nhận đối số như Maybe, vì vậy

Maybe Int :: * 
Maybe :: * -> * 
Monad :: (* -> *) -> Constraint 
        ^-- the result kind 
     ^-- the kind of Maybe