The Brilliance of Type Signatures in Haskell
I've been soaking up some Haskell lately, and have rediscovered the beauty of type signatures. As I vaguely remember from university, the ML-family of languages are truly profound in this regard.
Background
A type signature for a function in Haskell is somewhat like a method signature in Java (particularly with generics). However, they make stronger statements, due to:
- Haskell is a pure functional language: there are no side effects (for the sake of this post). The expression
(foo 5)is mathematical in nature. - Haskell does not support type coercion (see comments).
- Haskell cannot introspect a given type.
Like many languages, Haskell provides tuples: e.g.
(1,"hello") or (3.14, True). Consider this type signature for the function fst:This reads in English "
fst :: (a, b) -> a
fst accepts a 2-tuple of types a and b and returns something of type a". It is vital to understand that a and b are types: e.g. Int, String, etc.If you guessed that
fst returns the first element in the tuple: bingo. This is intuitive and natural.However, there's more, as explained in Real World Haskell. Because of the purity of Haskell and its strong type system, it is true that the only possible behaviour for a non-pathological version of
fst is that it returns the first element. In this example, there is no other option. That is mind-blowing; this kind of reasoning predicates some of the optimizations possible in Haskell.Consider this example, noting that
[a] is a list of a in Haskell:concat :: [[a]] -> [a]
What does it do? In Java, I might provide Javadoc (which could be false) but even a method signature doesn't tell the whole story: the method might quietly log to a file, write to a database, or launch missles. Here, we might intuit that
concat flattens a list (Ed's note: or the first level -- see comments):
concat [ [1] , [2,3], [4] ] = [1,2,3,4]Bingo.
As one works more and more with Haskell, the type signatures become vital, and simply fascinating.
A final, complex example. A Haskell monad has a combining function. For simplicity, I'll call it
myChain. It has a type signature of (where m is a Monad):myChain :: m a -> (a -> m b) -> m b
For this post, m is a generic type. In Java, think of
WeakReference<T> or List<T>.In English, we say that
myChain accepts a monad m of type a, and a function that accepts type a and returns a monad of type b. The result of myChain is a monad of type b.If we stare at this long enough, we can guess the following about this function, without knowing anything about monads: it probably pulls out the item of
type a from the first parameter and applies the function provided as the second parameter.This is true. We've been able to intuit something about the mighty monad simply from the type signature.
Brilliant.
The Upshot
There has long been a tension between dynamically-typed languages and statically-typed languages. In the last few years, the dynamic languages have become the media darlings. What's not to love? They are productive and mind-bending in their own way.
However, don't sell the statically-typed languages short: especially, the functional languages with strong, static typing. This is deeply profound stuff. As I work more and more with type signatures in Haskell, I feel the psychic fingerprints of abstract algebra and other math theory: it is as though we prove programs rather than write them.
ps.
myChain is known as >>= in Haskell, and is usually called bind.
