Lecture 9: Types of Types

We have seen several ways that, by carefully classifying expressions with different types, Haskell is able to provide the power to write functions that work in many settings (avoiding a lot of boilerplate code) while statically guaranteeing that a large class of run-time errors will never occur. Now, we will start learning about how Haskell carefully classifies types into different, well, types in order to push the expressive power even further.

To work up to this, let's do a bit of programming. Recall the definition of the Maybe type, which can be used in many cases to encode either "failure" or a "successful" result.


    data Maybe a = Nothing | Just a

We can write a couple example functions that "map over" Maybe values as routine recursive definitions.


    addOne :: Num a => Maybe a -> Maybe a
    addOne Nothing  = Nothing
    addOne (Just n) = Just (1 + n)

    square :: Num a => Maybe a -> Maybe a
    square Nothing  = Nothing
    square (Just n) = Just (n * n)

As usual when seeing repeated structure in our code, we look for ways to streamline, in this case by factoring out the mapping function.


    mapMaybe :: (a -> b) -> Maybe a -> Maybe b
    mapMaybe f Nothing  = Nothing
    mapMaybe f (Just x) = Just (f x)

    addOne = mapMaybe (1+)
    square = mapMaybe (\n -> n * n)

The type and expression structure of mapMaybe should look familiar. Recall our old friend map that "maps over" lists.


    map :: (a -> b) -> [a] -> [b]
    map f []     = []
    map f (x:xs) = f x : map f xs

Very many types arise in programming where having this kind of general map function is useful. So, treating them uniformly in the language will reap benefits.

*Exercise 9.1

Implement the following function that "lifts" the mapMaybe function, which works on single Maybe values, to work on lists of Maybe values.


    mapMaybes :: (a -> b) -> [Maybe a] -> [Maybe b]

Now write a similar function for lists.


    mapLists :: (a -> b) -> [[a]] -> [[b]]

Functors

In Haskell, the Functor class describes types that can be mapped over. (Learn You a Haskell describes such types as boxes, or containers, or computational contexts — analogies that you may find useful.) In particular, Functor is defined (in Data.Functor) as follows:


    class Functor f where
        fmap :: (a -> b) -> f a -> f b

As explained in the documentation but not checked by Haskell, Functor instances ought to satisfy two laws:

fmap id = id
fmap (f . g) = fmap f . fmap g

Intuitively, these requirements capture the idea that mapping should not change the "structure" of the original value. (If you are familiar with the mathematical notion of categories, functors arise as homomorphisms of categories, i.e., functions that take the objects and morphisms of a category, and map them to a possibly different category in such a way as to preserve identity arrows and compositions. The Functor type class and its associated laws are a way to describe this structure within Haskell.)

The instances of Functor defined in the Prelude and elsewhere in the standard Haskell modules all satisfy this law, and yours should, too.

There is an important aspect of the Functor definition that requires pause: the type f described by the class gets applied to other types, namely, a and b. This ability to apply type variables to other types is not something we have seen yet (except for when it peeked out in the types of some list functions, such as concat, elem, and all). At least one thing we can surmise, however, is that f describes only those types which can be applied to a type argument. We will return to the classification of types in more detail shortly.

For now, let's see how to turn the Maybe type into a Functor.


    instance Functor Maybe where
     -- fmap :: (a -> b) -> Maybe a -> Maybe b
        fmap f Nothing  = Nothing
        fmap f (Just x) = Just $ f x

Notice how, in comments, we've specialized, or instantiated, the type of fmap for this instance by substituting all occurrences of f with Maybe. Writing down specialized type signatures like this can be helpful, especially at first, but they are not allowed to appear in the program in earnest (unless the -XInstanceSigs option is set).

If you try evaluating the above, you'll get an error about duplicate instance declarations. There isn't a way to hide the instance declarations that come with an imported type. This choice is not a careless one. Rather, Haskell's type class system is designed around the invariant that there is exactly one instance declaration (hence, one set of implementations for the required methods) for each member type. For the purposes of presentation, we'll ignore the duplicate instance errors and pretend that they have not already been defined. At home, maybe you should just define your own variations of the types of interest so that you can experiment with defining their instances.

One last thing to mention is that, assuming we had defined mapMaybe elsewhere in the program, we could implement the Maybe instance as follows.


    instance Functor Maybe where
     -- fmap :: (a -> b) -> Maybe a -> Maybe b
        fmap = mapMaybe

Exercise 9.2

Write a different Maybe instance that typechecks but does not satisfy the Functor laws.

Exercise 9.3

Implement the list instance for Functor.

*Exercise 9.4

Write two different implementations of the function


    fmapList :: Functor f => (a -> b) -> [f a] -> [f b]

such that fmapList id = id.

Your second version should stem from a Functor-specific observation. You may not simply apply the kinds of transformations we have become accustomed to (e.g. syntactic sugar, eta-equivalence, composition).

Different Kinds of Types

As implied by our discussion of the Functor class definition above, Haskell makes distinctions between different types of types, called kinds. The words "type," "kind," "sort," and "category" are all synonymous. So, to avoid confusion, type-theoretic formulations often reserve the word "type" for classifying expressions, "kind" for classifying types, and, yes, "sort" for classifying kinds. Haskell doesn't track this last, um, type-or-kind-or-sort of classification, but some other type systems do.

Just like we can query Haskell for the types of expressions (using :type), we can query the kinds of types.


    > :kind Int
    Int :: *
    > :k Bool
    Bool :: *
    > :k Int -> Bool
    Int -> Bool :: *
    > :k [Int]
    [Int] :: *
    > :k (Int, Bool)
    (Int, Bool) :: *
    > :k Maybe String
    Maybe String :: *

The kind * (pronounced "star") describes grounded types. In Haskell, only grounded types are inhabited by expressions. Conversely, all Haskell expressions e have types t that have kind *.

Well then, what are the other, uninhabited kinds of types? As we've already seen, the type [Int] desugars to [] Int, the type (Int, Bool) desugars to (,) Int Bool, and the type Maybe String... can't get any sweeter. The kinds of [], (,), and Maybe may not surprise you.


    > :k []
    [] :: * -> *
    > :k (,)
    (,) :: * -> * -> *
    > :k Maybe
    Maybe :: * -> *

These kinds look a lot like function types! The kind * -> * describes types that, given a type argument of kind *, "return" a type of kind *. The kind * -> * -> * describes types that, given two type arguments of kind *, "return" a type of kind *. So, we can think of such types as functions that maps types to types, rather than values to values.

Of course, once we have functions that takes types to types, it becomes tempting to ask whether or not Haskell's type system is itself a programming language. The answer is “no,” at least in Haskell as defined by the 1998 and 2010 language reports, but it becomes a “yes” in the presence of some fairly common GHC language extensions.

DON'T PANIC! We're not going there. Type programming in extensions of Haskell is an advanced topic, not covered in this course.

A Taste of "Type-Level Programming"

Even though the Haskell type system itself is not a full, general-purpose programming language, it does incorporate many notions from the λ-calculus, including abstraction, application, and currying.

Let's take this bit by bit. Consider the type [(String,Int)], which could arise in practice as a way to represent a function from String to Int. If we wanted to abstract over the result type Int, we can do so by introducing a new type abbreviation:


    type Dict a = [(String,a)]

Thus, a Dict can be thought of as a list of objects of some type, indexed by strings. We can now re-introduce our original type [(String,Int)] by applying Dict to Int, like this:


    type IntDict = Dict Int

Less obviously, we could have taken the inner part of the Dict definition, and abstracted it as


    type StringAssoc a = (String,a)

re-expressed the right-hand side in terms of the prefix (,)


    type StringAssoc a = (,) String a

and then, wait for it..., η-reduced the type definition to


    type StringAssoc = (,) String

Yes, Haskell really does let us do this. Having delved this deeply into madness, you won't be surprised to know that we can define


    type Compose g f a = g (f a)

and then use Compose to re-express the definition of Dict, which sets us up to η-reduce the result:


    type Dict a = Compose [] ((,) String) a
    type Dict = Compose [] ((,) String)

The question is why? We'll get there.

Back to Functors

At last, we return to the definition of Functor to consider the kinds of the type variables a, b, and f. Notice that kind annotations for type variables are not written down, because they can be inferred based on how the type variables are mentioned in other types.

The (expression-level) function fmap takes (expression) arguments of type a and returns expressions of type b. Because only grounded types are inhabited by expressions, both a and b must have kind *. Furthermore, because the type f a must also be grounded, the kind of f is * -> *.

So, types like Maybe and [] are candidates for Functor, but types like Maybe Int, List Int, and (Int -> Bool) cannot possibly be, because they are not well-kinded according to the definition of Functor.

The Typeclassopedia

The standard Haskell modules provide a tremendous amount of functionality, including polymorphic data structures such as arrays, maps, sets, lists, unions, etc. This power is further leveraged by the inclusion of these data structures into a small number of mathematically well-motivated type classes, which provide common vocabularies and interfaces to very different types. A good survey of the most important of these type classes can be found in the Typeclassopedia.

For the next several lectures, we're going to work our way through a number of Haskell type classes, paying particular attention to three of the most important category-theoretically motivated type classes: Functor (which we have started to discuss), Applicative, and Monad.

CMSC-16100