In Haskell the "types" of types are called Kinds, denoted as *. Such as in:
Maybe :: * -> *
Either :: * -> * -> *
I was wondering if there is any equivalent for the "types" of kinds in Haskell or other strongly typed languages?
Are they of any practical importance? Are there any cases where they turn out to be very useful?
Any reference to some material would be appreciated.
From GHC 8 onwards, as part of the march towards dependent types in Haskell, there's a new extension -XTypeInType that makes the "types" of kinds to be... types.
When TypeInType is on, there are just two levels in the language: terms and types. And the type level folds back on itself, so that the "type" (in Haskell terms, "kind") of a type is again a type.
Prelude> :set -XTypeInType
Prelude> import Data.Kind
Prelude Data.Kind> :k Int
Int :: *
Prelude Data.Kind> :k (*)
(*) :: *
Also Type becomes a synonym for *, the kind of types that have actual values at the term level:
Prelude Data.Kind> :k (Int :: *)
(Int :: *) :: *
Prelude Data.Kind> :k (Int :: Type)
(Int :: Type) :: *
Prelude Data.Kind> :k (Monad :: (Type -> Type) -> Constraint)
(Monad :: (Type -> Type) -> Constraint) :: (* -> *) -> Constraint
This lets you employ with kinds all the machinery that already exists for types, enriching Haskell's support for type-level shenanigans at the cost of being inconsistent from a logical perspective (which doesn't matter because Haskell is already "inconsistent" when considered as a proof system, for a host of other reasons).