Spaghetti Code and Meatballs

Higher Kinded Types: Intro (part: 1 / 2)

August 28, 2018

If you’ve been touching haskell for a while, you’ve probably gone across this operator when talking about types: *. This * is what we call a kind. There are many different uses of kinds, but see them as categories for different types (or as some people who have no regard for saying confusing things call them, types for types).

If you’ve ever really thought about types that have parametric types, like for example the option type Maybe and the type of a basic type, Int, you’d notice that two types are different. Maybe takes in type parameters, Maybe itself does not have values. there is nothing out there of type Maybe, there are things out there of type Maybe a. Maybe requires a type parameter before becoming a full ‘instantiated’ type. Therefore, instead of having kind * like Int it has kind * -> *.

Kinds can be even more complex than that however. What is more complex than kinds with one paramater? Why kinds with two parameters of course. Enter the famed either type:

data Either a b = Left a | Right b

It takes two type paramaters, therefore it has kind * -> * -> *.

For haskell, the kind of a type is important not only to differentiate types, but also to specify type classes. Ever notice how haskell only allows functors of kind * -> *? In the definition of functor:

class  Functor f where
    fmap        :: (a -> b) -> f a -> f b
    (<$)        :: a -> f b -> f a
    (<$)        =  fmap . const

Haskell’s type system implicitly can derive that f here must be of kind * -> * and will subsequently require all instances be of that kind too. but that’s not all that haskell can do. Haskell can also have higher order kinds like (* -> *) -> *

-- this has kind (* -> *) -> *
type Intify a = a Int

-- this has kind (* -> *) -> * -> *
type Apply a b = a b

Both these types are valid and would typecheck with the latest version of ghc. Now you may ask, why would anyone ever need those types, and the answer to that question is most of the type you won’t need higher kinded types, but on the occasions that you do you’ll be glad that GHC can support it. I’m writing up a blog post of my favorite use-case of higher kinded types, recursion-schemes. I’ll post a link to it soon! Stay tuned.


Shalom YibletWritten by Shalom Yiblet, a Senior at Carnegie Mellon University. He studies Computer Science with interests in Machine Learning and Programming Languages. He is a Teacher's Assistant for Compilers.