Let's get this out of the way before we go any further: This is a massive chapter. There is a so much content in here, and there is no way that I'll be able to summarize it all in one neatly packaged post. Instead, I'll be focusing on the things that struck me as particularly important: kinds and cardinality.
That means that in exchange for covering a few topics more thoroughly, I will not be devoting many words to /newtypes/, arity, what sum and product types are (see chapter 4 and chapter 9), or constructing and deconstructing data types (see chapter 7a).
Kinds
This section has several references to the data type known as ~Maybe~. We have not covered this data type previously in this series, so a short introduction is in order if you're not already familiar with it.
~Maybe~ is used to model data that you may or may not have. It has two data constructors: ~Just~ and ~Nothing~, takes one type parameter, and is in some ways similar to how a lot of other languages have a ~null~ value, though more robust. It is similar to the ~Option~ type in other languages such as Rust, OCaml, and F#.
The data declaration is as follows:
#+begin_src haskell
data Maybe a = Just a | Nothing
deriving (Eq, Ord)
#+end_src
For more information, please see the Haskell wiki article.Kinds are to types what types are to terms. Or, put differently, a kind can be seen as a type constructor's type or as a type one level up. It sounds convoluted, but bear with me.
Keep in mind that, as covered in chapter 4, a type constructor is one of two constructor types in Haskell (the other being data constructors). It is the name of the type. Type constructors are used only at the type level, in type signatures, and in typeclass declarations and instances.
We represent kinds with the * symbol. If you have a fully applied, concrete type constructor, such as Bool or [Int], then the kind is *. If you have a type constructor that is still waiting for a type parameter---such as Maybe---then that has the kind * -> *. A kind is not a type until it is fully applied. In other words, Maybe isn't a type, but Maybe String is.
Second, we only talk about kinds on the type level. That is, Bool is a type and has kind *. False is a term (or value) and does not have a kind. For data constructors that share names with their type constructors (e.g. []), this can be confusing, but remember that kinds only operate on type level constructors.
To make this clearer, let's turn to the ever faithful GHCi. To print the kind of a type constructor, we use the :k (or :kind) command followed by the constructor we want information on. Let's have a couple of examples and see what we can learn.
Prelude> :k Bool
Bool :: *Bool is a fully applied type in and of itself. it takes no type parameters and as such has kind *.
Prelude> :k Maybe
Maybe :: * -> *Maybe is our first higher-kinded type (more on that in a bit), which means it's a type constructor that requires another type before it's complete. In other words, you couldn't simply put Maybe in a type signature without saying what type of maybe it is.
Prelude> :k Maybe Integer
Maybe Integer :: *Maybe Integer, on the other hand, is a concrete type. As opposed to just Maybe above, we also know what the type is (Integer). As such, it is fully applied and of kind *.
Prelude> :k (,)
(,) :: * -> * -> *This one is quite interesting. This is the type constructor for a tuple. Without any type parameters, it's of kind * -> * -> * because it needs two types to be fully applied.
Higher-kinded types
According to the book, there are only 'a few' kinds, and the default (and the only one covered in this chapter) is *. Kind signatures work the same as type signatures, i.e. using the same :: and -> syntax.
Higher-kinded types are types that require type parameters to be fully applied, to become real types---that is, their kind is at least * -> *. Lists, tuples, and Maybe are good examples of higher-kinded types.
Cardinality
The cardinality of a type is the number of different values it defines. A value defined by a type is also known as an inhabitant of said type. Types' cardinalities can be anywhere from as small as 0 (empty types) and as large as infinite.
To demonstrate this concept we'll use these arbitrary sum types, modeled after the starters in the mainline Pokémon games (just pretend we're in 1999 for simplicity's sake):
data StarterType
= Grass
| Fire
| Water
data Starter
= GenI StarterType
| GenII StarterTypeThe cardinality of StarterType is 3 because it has only three possible inhabitants. The cardinality of Starter is 6, because it has two data constructors, each of which also require a StarterType. As such, we get 2 \cdot 3 (or 3 + 3), which is 6.
Above, the Starter type demonstrates why it's called a sum type: We can calculate the cardinality of the type by summing the number of possible values of each of it's data constructors.
If you've got a friend with a link cable, then maybe you've traded some pocket monsters and ended up with two starters---lucky you! In this case, you now have a tuple of starters, i.e. (Starter, Starter). A tuple is a product type, so that means we find the cardinality by multiplying the cardinality of each of its contained types. As such, the cardinality of (Starter, Starter) is 6 \cdot 6 = 36.
This is the basic concept of cardinality in types. It's pretty straightforward, and it's a good thing to keep in mind when designing systems.
The function type is exponential
We've seen that sum types are the addition operator and that product types are the multiplication operator when it comes to calculating inhabitants of types. However, we haven't mentioned function types, which act as the exponent operator: given a function a -> b, the formula for the number of inhabitants is b^a. So if we have a function StarterType -> Bool, for instance, the number of possible implementations is 2^3 = 8. This relationship continues as the number of parameters increases, so for a -> b -> c it's equal to c^{ba} (or (c ^ b) ^ a).
If this is a bit confusing: don't worry, I'm right there with ya. But let's give it a go. Let's write out all possible permutations of the function StarterType -> Bool.
acceptStarter1 :: StarterType -> Bool
acceptStarter1 Grass = True
acceptStarter1 Fire = True
acceptStarter1 Water = True
acceptStarter2 :: StarterType -> Bool
acceptStarter2 Grass = True
acceptStarter2 Fire = True
acceptStarter2 Water = False
acceptStarter3 :: StarterType -> Bool
acceptStarter3 Grass = True
acceptStarter3 Fire = False
acceptStarter3 Water = True
acceptStarter4 :: StarterType -> Bool
acceptStarter4 Grass = False
acceptStarter4 Fire = True
acceptStarter4 Water = True
acceptStarter5 :: StarterType -> Bool
acceptStarter5 Grass = False
acceptStarter5 Fire = False
acceptStarter5 Water = True
acceptStarter6 :: StarterType -> Bool
acceptStarter6 Grass = False
acceptStarter6 Fire = True
acceptStarter6 Water = False
acceptStarter7 :: StarterType -> Bool
acceptStarter7 Grass = True
acceptStarter7 Fire = False
acceptStarter7 Water = False
acceptStarter8 :: StarterType -> Bool
acceptStarter8 Grass = False
acceptStarter8 Fire = False
acceptStarter8 Water = FalseWhew. And that's with only two possible result values and three possible inputs. Yeah, this gets wild pretty quickly.
Closing up
While the format is a bit different from previous posts in the series, I hope you found something useful here too. The rest of what the chapter covers is definitely interesting, but not eye-opening in the way that kinds and cardinality are. The next chapter is on handling errors and includes Maybe, Either, more higher-kindedness, and anamorphisms (if that sounds interesting, why not check out this post on corecursion and anamorphisms in the meantime?). Stay tuned, and it should land at some unspecified future date.
Until next time: stay safe.
