August 28, 2018
If you’ve been touching haskell for a while, you’ve probably gone across this operator
when talking about types:
* 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
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
requires a type parameter before becoming a full ‘instantiated’ type. Therefore, instead of having
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.