Let's read: Haskell Programming from First Principles, pt XI

Algebraic Data Types: Kinds and cardinality
Excerpt from the Programming Haskell From First Principles book cover, showing just the title. There is an overlay saying 'Chapter 11' across the top right corner.

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:

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.

Bool is a fully applied type in and of itself. it takes no type parameters and as such has kind *.

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.

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

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):

The 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 ⋅ 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 ⋅ 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 ba. So if we have a function StarterType -> Bool, for instance, the number of possible implementations is 23 = 8. This relationship continues as the number of parameters increases, so for a -> b -> c it’s equal to cba (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.

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