Chapter 7. Patterns of Kind Abstraction
Type-level programming involves computation at type-level that is executed during the type-checking phase.
In earlier chapters, we saw the beginnings of type-level programming when we used functional dependencies and GADTs, but to do proper type-level programming, we need an even more enriched kind system.
We will freely interchange the terms type-level and kind-level, since in Haskell, type-level programming happens at the level of kinds.
Type-level programming stands in contrast to term-level programming, in that the former executes in the type-checking phase and the latter executes at runtime.
In this chapter, we will explore patterns of kind-abstraction as they relate to type-level programming. First, we will look at the basic kind system, extend it with the associated types, and then look at more generalized type families.
In the last round of extensions, we will add kind polymorphism and datatypes (via data type promotion) to the kind system...
