If you're stumbling upon this document, I'm guessing that you're just getting into a statically typed programming language and are (rightfully) confused about what all the kerfuffle regarding Monads and Higher-Kinded types are. This blog article will clear all the confusion you have about what monads and higher kinded types really are, but how to use higher kinded types (in, say, Haskell) is not covered here.
Background - Static Types
Before we can really talk about what a monad is, let's take a step back. In terms of programming, monads only exist in programming langauges which support strong static typing. That means, that the type system of the programming language follows a mathematical type system. See: Wikipedia. The reason that this is so neat is that Type Theory is the basis of all of mathematics. Every other branch, including Calculus, Algebra, Trigonometry, Statistics, etc. can all be defined in terms of Type Theory operations.
In programming languages, types denote the type of data you're working with. Numbers may be classified as "int" or "double" in a lot of languages, which are different types which represent numbers. Text may be of type "string", etc. Languages that have "strong" static types take this a step further, being a direct representation of their type-theory counterparts.
Background - Type Theory
Types in type theory work as such: there are two variations of information. 'Types' and 'Kinds'. Kinds are, in a way, the father of types.
The kind, denoted "*", is literally pronounced "type". It is used to describe any type that doesn't take a type argument (more on this later). This can include things like functions, ints, doubles, strings... pretty much every type that you're experienced with, outside of generics.
The kind * -> * is where things begin to be interesting. This is about as far as Haskell and many other strongly-typed languages truly go (with the exception of kind (* -> *) -> *, the higher-order kind). This is the kind of any type that takes one type parameter... a little unclear? Read on.
Higher Kinded Types and Monads
* -> * you can think of as a "template template". Think of, in Java, this class:
class myClass<T>{
T myItem;
}
In this case, the type "myClass" is the first * and the type "T" is the second *. In Haskell, which is strongly statically typed, a data type declaration, such as
data List a = Node a | Rest (List a)
In this case here, List a has the kind "* -> *" because it takes one type parameter (a).
The important thing to realize about this, is that kinds of this type can be generecized within the type declarations of other functions. As an example of exactly what that means:
myFunction :: l a -> [a]
would take any * -> * that takes 'a' as a type paramter, and returns an array of that type from it.
Where do Monads fit into the equation?
Monads are a concept from category theory. There, monads are an endofunctor paired with two natural operations. The details of this are interesting, but outside the scope of this quick run-down of HKT's and monads. Check out Category Theory if you'd like to know more.
The function declaration of monad's function is as such:
Monad m => m a -> (a -> m b) -> m b
So, as you can see, Monads are only possible with the use of Higher-Kinded types ((m a) and (m b), make the kind * -> *). Monads also define particular functions which follow the 'monadic laws', however, these are unrelated to their basis in the type system.
Conclusion
Type theory is a gigantic branch of mathematics, and this quick run-down of how types work in statically typed languages does not even closely begin to scratch the surface. Hopefully you've taken away a bit more about what it means to be "higher kinded", and a bit how monads use the type system to exist.
If you'd like to learn more or correct me on something I said wrong up above, by all means feel free to comment!
No comments:
Post a Comment