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 ...