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
,
where Int, String
are the concrete types and List, Array, Either, Identity
are type
constructors. Furthermore, 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 : * -> * -> *