Kind polymorphism

Type families gives us functions at the type-level (through type functions). Analogously, the Polykinds language extension gives us polymorphism at the type-level.

Kind polymorphism (Giving Haskell a Promotion, by Yorgey et al in 2012) allows us to describe more generic data and functions. For example, when designing a type-class, the need may arise to cater for various kind-orders. Consider the multiple Typeable classes for multiple arities as an example:

class Typeable (a :: * ) where
  typeOf :: a -> TypeRep

class Typeable1 (a :: * -> *) where
  typeOf1 :: forall b. a b -> TypeRep

The same goes for the Generic type-class we encountered earlier: we need to define different type-classes for different kind arities.

To explore kind polymorphism, we'll work with a trivialized version of Typeable, where the typeOf function simply returns a string instead of a TypeRep:

class T0 a where
  f0 :: a -> String

instance T0 Int where
  f0 _ = "T0 Int"

instance T0 Char where...