Higher Kinded Types¶
Identity a = a List Int Array Int Either String Int
Above snippet registers some types like
Identity, List, Int, Array, Either, String,
Int, String are the concrete types and
List, Array, Either, Identity are type
Either stands apart from the other 3, for it can be applied twice(
Either : (a : Type) -> (b : Type) -> Either a b ), while
the other 3 could only be applied once.
To describe this internal property of types, a concept called Kind has been built and, you can regard a kind as the type of a type.
Each type has a kind ascription:
(the star * means it's the concrete type) Int : * Identity, Array, List : * -> * Either : * -> * -> *