This section describes kind polymorphism, and extension
enabled by -XPolyKinds.
It is described in more detail in the paper
Giving Haskell a
Promotion, which appeared at TLDI 2012.
Currently there is a lot of code duplication in the way Typeable is implemented
(Section 7.5.3, “Deriving clause for extra classes (Typeable, Data, etc)”):
class Typeable (t :: *) where typeOf :: t -> TypeRep class Typeable1 (t :: * -> *) where typeOf1 :: t a -> TypeRep class Typeable2 (t :: * -> * -> *) where typeOf2 :: t a b -> TypeRep
Kind polymorphism (with -XPolyKinds)
allows us to merge all these classes into one:
data Proxy t = Proxy class Typeable t where typeOf :: Proxy t -> TypeRep instance Typeable Int where typeOf _ = TypeRep instance Typeable [] where typeOf _ = TypeRep
Note that the datatype Proxy has kind
forall k. k -> * (inferred by GHC), and the new
Typeable class has kind
forall k. k -> Constraint.
Generally speaking, with -XPolyKinds, GHC will infer a polymorphic
kind for un-decorated whenever possible. For example:
data T m a = MkT (m a) -- GHC infers kind T :: forall k. (k -> *) -> k -> *
Just as in the world of terms, you can restrict polymorphism using a signature
(-XPolyKinds implies -XKindSignatures):
data T m (a :: *) = MkT (m a) -- GHC now infers kind T :: (* -> *) -> * -> *
There is no "forall" for kind variables. Instead, you can simply mention a kind variable in a kind signature, thus:
data T (m :: k -> *) a = MkT (m a) -- GHC now infers kind T :: forall k. (k -> *) -> k -> *
Just as in type inference, kind inference for recursive types can only use monomorphic recursion. Consider this (contrived) example:
data T m a = MkT (m a) (T Maybe (m a)) -- GHC infers kind T :: (* -> *) -> * -> *
The recursive use of T forced the second argument to have kind *.
However, just as in type inference, you can achieve polymorphic recursion by giving a
complete kind signature for T. The way to give
a complete kind signature for a data type is to use a GADT-style declaration with an
explicit kind signature thus:
data T :: (k -> *) -> k -> * where MkT :: m a -> T Maybe (m a) -> T m a
The complete user-supplied kind signature specifies the polymorphic kind for T,
and this signature is used for all the calls to T including the recursive ones.
In particular, the recursive use of T is at kind *.
What exactly is considered to be a "complete user-supplied kind signature" for a type constructor? These are the forms:
A GADT-style data type declaration, with an explicit "::" in the header.
For example:
data T1 :: (k -> *) -> k -> * where ... -- Yes T1 :: forall k. (k->*) -> k -> * data T2 (a :: k -> *) :: k -> * where ... -- Yes T2 :: forall k. (k->*) -> k -> * data T3 (a :: k -> *) (b :: k) :: * where ... -- Yes T3 :: forall k. (k->*) -> k -> * data T4 a (b :: k) :: * where ... -- YES T4 :: forall k. * -> k -> * data T5 a b where ... -- NO kind is inferred data T4 (a :: k -> *) (b :: k) where ... -- NO kind is inferred
It makes no difference where you put the "::" but it must be there.
You cannot give a complete kind signature using a Haskell-98-style data type declaration;
you must use GADT syntax.
A type or data family declaration always have a
complete user-specified kind signature; no "::" is required:
data family D1 a -- D1 :: * -> * data family D2 (a :: k) -- D2 :: forall k. k -> * data family D3 (a :: k) :: * -- D3 :: forall k. k -> * type family S1 a :: k -> * -- S1 :: forall k. * -> k -> *
In a complete user-specified kind signature, any un-decorated type variable to the
left of the "::" is considered to have kind "*".
If you want kind polymorphism, specify a kind variable.