What is Constraint in kind signature

问题:

If I inspect the kind of Maybe I get this:

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

Now, if I inspect the kind of Monad I get this:

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

What is Constraint there and why it is needed ? Why not just this * -> * ?

回答1:

Unlike Maybe, Monad is not a type; it is a typeclass.

The same goes for other typeclasses:

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

Where * represents concrete types (such as Bool or Int), -> represent higher-kinded types (such as Maybe), and Constraint represents the idea of a type constraint. This is why:

---

As we know we can't make a signature like this:

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

Because Monad should be used as a constraint, to say that, 'this must be a monad to work':

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

We do this because we know that return can't work on any old type m, so we define the behaviour of return for different types under the name Monad. In other words, there is no single thing that can be called a Monad, but only behaviour that can be called Monadic.

For this reason, we have created this type constraint, saying that we must have pre-defined something as a Monad to use this function. This is why the kind of Monad is (* -> *) -> Constraint - it itself is not a type!

---

Maybe is an instance of Monad. This means that somewhere, someone has written:

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

...and defined how Maybe should behave as a Monad. This is why we can use Maybe with functions or types that have the prefix constraint Monad m => .... This is essentially where one defines the constraint applied by Monad.

回答2:

Constraint is the kind of e.g. Show Int, Monad Maybe, and Monoid [a]. Roughly, it is the kind of everything that can occur on the left side of => in type annotations.

Now since

Show Int :: Constraint

and Int is a type, i.e.

Int :: *

we can assign a functional kind to Show as follows

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

In your case it just happens that a Monad takes argument like Maybe, so

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