Lambda the Ultimate

(* -> *) -> * (functor application), * -> (* -> *) (or * -> * -> *)...
You can also have type systems with other base kinds.

Kinds such as *->((*->*)->*)->* are certainly possible, essentially meta-type abstractions (with * being any concrete type).

If types are described with categorical or topographical properties (invariants under certain transforms, support for a particular type-class, etc.) then one can reasonably describe kinds using the language for describing these properties of types. That gives us something other than * as the base kind.

One may also get a bit more complex with inter-dependent types, as where the accepted kinds or types for the second argument to *->*->* depends upon the first argument. I.e. you can have dependent kinding.

But all this depends on the expressiveness of the language, of course.

This is probably the simplest Haskell example:

Prelude> :k Either
Either :: * -> * -> *

How about unboxed types in haskell?
I think they belong to another kind #.

It's also

Prelude> :k (->)
(->) :: ?? -> ? -> *

but I don't know what this means.

The possible kinds of a language are, just like the possible types of a language, part of the language definition. In Haskell, the kinds are generated by the following grammar:

  k ::= type | k -> k

The kind of each type constructor in your language can then be given as:

   (*)  : type -> type -> type      -- products
   (+)  : type -> type -> type      -- sums
   (=>) : type -> type -> type      -- function space
   list : type -> type              -- lists
   mu   : (type -> type) -> type    -- recursive types
   all  : (type -> type) -> type    -- universal quantification over types

list, mu, and forall are all types with kinds other than the two you suggested.

However, you can certainly extend the language of kinds further. For example, you can add products at the kind level:

  k ::= type | k -> k | k * k 

This is useful (for example) when modelling mutually recursive types:

  mu2 : ((type * type) -> (type * type)) -> (type * type)

Is this a Haskell question? If not, in the lambda cube, there are two basic kinds, (*) for types and (o) for terms, with higher kinds built up with the (() -> ()) connective. The various kinds of abstraction in pure type systems have kind ((A -> B) -> B), where A and B range over the basic kinds, and where lambda abstraction is ((o -> o) -> o), as in LF.

Not in Haskell, but there are systems where phantom types can have kinds other than *. For example, type level naturals might be in the kind Nat, and there might be a type constructor like Vector having the kind * -> Nat -> *.

For example, Control.Monad.State.StateT has kind * -> (* -> *) -> * -> *. It's probably one of the simpler examples of a higher-kinded type.

The Ur/Web language that I'm working on has kinds for type-level records and names, which is really useful for metaprogramming.