Types of types: Haskell's Kind system

Contents · 7 sectionsValuesTypesKindsHigher-Kinded TypesHigher-Kinded DataCustom KindsConclusionWhile working to add typed configuration to my Haskell Redis server clone, I found myself learning some new tricks, all of them stemming from Haskell's Kind system. In this article, we're gonna discuss what I learned and the things I managed to build with it. We'll start from the beginning, with Values. Values These are the constructs we manipulate in our programs, things like 1, 2, True, "hello", etc… In functional programming contexts, they're also called "terms." They are the things we consume, create, compute with, and output. The management and manipulation of values is a big part of the practice of programming and software engineering. We all work with different values in our day to day. Like creatures in a fantasy setting, values that share certain characteristics – that are created, used, and manipulated in the same way – belong to the same species. Formally, these "species" are called Types. Types Types are groups of related values. Put another way, the notion of a type offers us a means of collectively referencing/referring to a group of related values. In many programming languages, we use words like Int, string, Bool, Text, etc… to denote a type. The main benefit, in grouping values into types, IMO, is abstraction. Types inform us – the programmer and the compiler – of the characteristics of a value and the kinds of operations that can and can't be performed on or with it. Think of weapon classes in a game. In many RPGs there are weapon classes and the class of a weapon often dictates the kinds of attacks that you can perform or the kinds of skills you can use with it; types do the same for values. Taking this one step further, you might ask yourself, how do we classify types? Do we even need to do that? Why? To answer those questions, we must step into the realm of Kinds. Kinds Kinds are to types what types are to values. My intuition for the Kind system is that it is a means of classification for all things type level. You would think "all things type level" would simply refer to everyday types, but in Haskell (and a couple other languages), other type-level constructs exist, like type-level numbers (of Kind Nat), type-level strings (of Kind Symbol), or the constraints from Typeclasses (of Kind Constraint). We won't be going into much detail about any of those, but Nats and Symbols do often appear in type-level programming contexts. On the other hand, entities of Kind Constraint are likely more familiar because they're just (fully applied) Typeclasses for the most part. For example, the Show Typeclass belongs to the Kind Type -> Constraint and Show Int belongs to the Kind Constraint. Regular types belong to the Kind Type. Confusing, I know. Type constructors, that is, things like Maybe, Either, Last, Proxy, Dual, etc…, have their Kind determined by both their arity and the Kind of their parameters as showcased by the table below. Value Type-level construct Kind 1 Int Type True Bool Type not Bool -> Bool Type [1, 2, 3] [Int] Type Just "hello" Maybe String Type Right 5 Either String Int Type Maybe Type -> Type [] (the list type constructor) Type -> Type Either Type -> Type -> Type Either String Type -> Type Three (from data Three a b c = …) Type -> Type -> Type -> Type 5 (a type-level number) Nat (GHCi prints Natural) "hello" (a type-level string) Symbol Show Int Constraint Show Type -> Constraint Functor (Type -> Type) -> Constraint Compose (simplified) (Type -> Type) -> (Type -> Type) -> Type -> Type * vs TypeIn older docs and in some GHC error messages, you'll see * where I write Type. They're the same thing. AFAICT * is a synonym for Type and vice versa. * is the older name, and GHC plans to deprecate it (-Wall already warns when you use it). Fun factTechnically, regular types are also type constructors, type constructors with no parameters. You may find them being referred to as "nullary type constructors". Without Kinds, there'd be no way to tell type-level constructs like Maybe, Maybe Int, and Show apart, IMO. Depending on where you are in your Haskell journey, the benefit of having some of these other type-level entities may not be entirely apparent, but I can assure you that they all work to make the Haskell type system more expressive, allowing us to codify more things in the type system, which in turn makes it easier to write safer programs. Higher-Kinded Types Now, we mentioned before that types allow us to abstract over values. This means that we can collectively refer to a set of values through their type. Similarly, with a given Kind, we name a collection of type-level constructs. For example, the Kind Type -> Type collectively refers to all type constructors that take a single regular type as an argument: that covers things like Maybe, but also partial applications like Either String or Three Int String. Likewise, the Kind Type -> Type -> Type collectively refers to all type constructors that take two regular types as arguments. To tie this back down to the value/term level, it's similar to function signatures. A function signature of Int -> Bool collectively refers to all functions that take an Int as argument and return a Bool. Now, we know that a signature like Int -> Bool collectively refers to a set of functions, but what about something like (Int -> Int) -> Bool? What does that mean? That signature represents all functions that return a boolean only after accepting a function with a signature of Int -> Int as argument. This type of signature is quite common, and functions with signatures like this are called higher-order functions. Okay, now, what happens if we try to extrapolate this idea to the Kind level? What if we replaced the Type param in Type -> Type with (Type -> Type)? Well, for starters, we get a signature like (Type -> Type) -> Type. We know that Type is the Kind for all regular types and Type -> Type is the Kind for all type constructors that take a single regular type as argument. Putting that together means that the signature (Type -> Type) -> Type represents the Kind for all type-level constructs that take a type constructor as argument. You see where I'm going with this? Just as functions with signatures like (Int -> Int) -> Bool are called higher-order functions, type constructors with Kinds like (Type -> Type) -> Type or (Type -> Type) -> (Type -> Type) -> Type are collectively called higher-Kinded types or HKTs for short. Here's a small example: data Wrap (f :: Type -> Type) = Wrap (f Int) Wrap takes a type constructor f and puts an Int inside it, so its Kind is (Type -> Type) -> Type. Wrap Maybe is a regular type, and so is Wrap []. Wrap (Just 5) and Wrap [1, 2, 3] are values of each. Compose from the table earlier is another example, just with more parameters. From another angle, if parameterized types like Maybe or Either are what other languages call generics, then HKTs are generics that can take other generics as arguments. The concept of HKTs, when coupled with Typeclasses, gives us the ability to implement certain functionality on type-level constructs. That's useful because it lets us reuse operations in many more contexts. To illustrate, let's take Functor :: (Type -> Type) -> Constraint. Functor isn't an HKT itself, since its Kind ends in Constraint, not Type. However, its parameter is a type constructor, which makes it higher-Kinded. Now, if a type constructor has a Functor instance, we can map over its contents using the fmap function. Furthermore, thanks to the higher-Kinded nature of Functor, we only need to define a single Functor instance for an appropriately Kinded type constructor (Type -> Type specifically) to be able to use fmap with any specialization of said type constructor. What I mean is, because we define the Functor instance on, say, Maybe and not some Maybe a, we can use fmap on all concrete versions of Maybe a (Maybe Int, Maybe String, Maybe Bool, etc…). In fact, it can't work any other way: Functor's Kind signature only accepts type constructors of Kind Type -> Type, so something like Maybe Int, of Kind Type, isn't even a candidate. The instance belongs to Maybe itself. This principle applies to all other higher-Kinded Typeclasses and appropriately Kinded type constructors. In non-technical terms, take a bowl for eating. Make the bowl itself microwave-safe and you can use it to warm any food you put in it. In this case, the bowl is our "appropriately Kinded type constructor"; the standard that determines whether something is "microwave-safe" is our higher-Kinded Typeclass (like Functor); the "microwave-safe" label we put on our bowl is its Typeclass instance; and the bowl of food we're able to microwave represents a specialization of our type constructor. Here too, it can't work any other way: nobody certifies a bowl of soup as microwave-safe. The label belongs to the bowl and applies regardless of the bowl's contents. Higher-Kinded Data Higher-Kinded data, or HKD for short, is the name of a pattern where, instead of a type-level thing, a data type takes one or more type constructors as parameters and uses them to wrap some or all of its fields. People might consider this "advanced", but it's actually pretty straightforward once you wrap your head around higher-Kinded types. Here's an example: -- The `f` parameter is a type constructor, making `Profile` higher-Kinded data Profile (f :: Type -> Type) = Profile { age :: f Int , name :: f String , profession :: f String , address :: f String } -- `f = Identity`: every field must be present grace :: Profile Identity grace = Profile (Identity 37) (Identity "Grace") (Identity "Computer scientist") (Identity "New York") -- `f = Maybe`: any field can be missing, like a half-filled sign-up form draft :: Profile Maybe draft = Profile Nothing (Just "Grace") Nothing Nothing -- `f = Const String`: every field holds a `String`, whatever its type, like a form label