11 Type system advances

This chapter is devoted to programming at the level of types. We’ll explore a variety of Haskell features that makes 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’ll discuss features and techniques available to any Haskell programmer. While presenting them, I limit myself to simple, contrived examples. In particular, we’ll discuss the types and kinds system, data kinds, type families, generalized algebraic data types, and polymorphism. I conclude this chapter with ways to deal with errors while programming at the type level.

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

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 and values to types

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 character escaping in GHCi

11.3.3 Data families

11.3.4 Associated families

11.4 Generalized algebraic data types

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

11.6.1 Be explicit about types

11.6.2 Ask the compiler