Higher-order kinds

Types classify values at different levels of abstraction, for example:

  –- Primitive types
 "a string"  :: String
 12             :: Int

  -- instances of higher-order, parameterized types
  Just 10  :: Maybe Int
  Left 10  :: Either Int b

  -- functions are first class values
  (* 2) :: Num a => a -> a

  -- and type-constructors are functions
  Just :: a -> Maybe a
  Left :: a -> Either a b

In a similar way, kinds classify types. For monomorphic types (that is, not polymorphic), the kind signature is just the placeholder *:

 -- TYPE         KIND
 [Char]         ::    *
 Maybe Int   ::    *

Parametric types express higher-order kinds, for example:

   Maybe  ::  * -> *
   --         a -> Maybe a

where (* -> *) is a placeholder for a -> Maybe a. Let's compare this with the kind signature of Either:

 Either       * -> *  -> *
 --              a -> b -> Either a b

The Haskell kind system can distinguish between two main...