11 Type system advances

This chapter is devoted to programming at the level of types. We explore the variety of Haskell features that make it possible. As we’ve discussed earlier in this book, types help us to control software behavior and express our ideas on what the code should and shouldn’t do. Heavily typed code is highly resistant to some sorts of bugs. It also enables aggressive refactoring. If we do something wrong the Haskell type checker would report that.

We discuss features and techniques available to any Haskell programmer. While presenting them, I limit myself to elementary artificial examples. In particular, we discuss types and kinds system, data kinds, type families, generalised algebraic datatypes, and polymorphism. I conclude this chapter with ways to deal with errors while programming at type-level.

Almost everything discussed in this chapter is not standard Haskell and implemented in GHC via extensions. By the end of this chapter you will understand and be able to use all the GHC extensions from the following listing:

11.1  Haskell types 101

11.1.1  Terms, types, and kinds

11.1.2  Delivering information with types

11.1.3  Type operators

11.2  Data kinds and type-level literals

11.2.1  Promoting types to kinds

11.2.2  Type-level literals

11.3  Computations over types with type families

11.3.1  Open and closed type synonym families

11.3.2  Example: avoid Char-escaping in GHCi

11.3.3  Data families

11.3.4  Associated families

11.4  Generalised algebraic datatypes

11.4.1  Example: Representing dynamically-typed values with GADTs

11.4.2  Example: Representing arithmetic expressions with GADTs

11.5  Arbitrary-rank polymorphism

11.5.1  The meaning

11.5.2  Use cases

11.6  Advice on dealing with type errors