haskelltype-kindsconstraint-kinds

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 * -> * ?


Solution

  • 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.