What does k -> * mean?

Viewed 105

In the prelude, the type information about ReaderT says:

newtype ReaderT r (m :: k -> *) (a :: k)
  = ReaderT {runReaderT :: r -> m a}

What does (m :: k -> *) it mean? m takes an argument of type k, but m is a higher kinded type.

Information about higher kinded looks also wired:

Prelude> :k ReaderT
ReaderT :: * -> (k -> *) -> k -> * 
1 Answers

The fragment (m :: k -> *) indicates that m is a type variable of kind k -> *. This, in turn, means that m is a higher-kinded type that takes a type (of unspecified kind k) and produces a concrete type (i.e., a type of kind *).

All you're seeing here is GHC's attempt to infer the most general possible kind for a type (the same way it infers the most general possible type for a function).

Here's the reason this kind is inferred: The actual definition of ReaderT given in module Control.Monad.Trans.Reader in the transformers package is:

newtype ReaderT r m a = ReaderT { runReaderT :: r -> m a }

The right-hand side implies that r and m a must both be concrete types (of kind *). From this, it's possible to infer that r is of kind * and that m takes a single argument and produces a concrete type (so m is of kind something -> *). Since there is no constraint placed on the kind of a by this definition, GHC decides that it can have arbitrary kind k, implying that the kind of m is k -> * for an arbitrary k.

This explains both:

> :i ReaderT
...
newtype ReaderT r (m :: k -> *) (a :: k)
  = ReaderT {runReaderT :: r -> m a}
...

and:

> :k ReaderT
ReaderT ::    * -> (k -> *) -> k -> *
-- kinds of:  r        m       a    `-- (ReaderT r m a)

Now, just because GHC infers such a general kind doesn't indicate that it has any use or purpose. Since all monads are of kind * -> *, the only way to create a ReaderT that didn't use an a of kind * would be to use it to "transform" an m that wasn't actually a monad, and then you wouldn't be able to use any of the functions in Control.Monad.Reader that use a Monad m constraint (which is almost all of them). So, in this case, the generalization is useless.

Related