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.
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.
(3.14, True). Consider this type signature for the function
This reads in English "
fst :: (a, b) -> a
fstaccepts a 2-tuple of
band returns something of
type a". It is vital to understand that
bare types: e.g.
If you guessed that
fstreturns 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
fstis 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
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
concatflattens a list (Ed's note: or the first level -- see comments):
concat [  , [2,3],  ] = [1,2,3,4]
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
myChain :: m a -> (a -> m b) -> m b
For this post, m is a generic type. In Java, think of
In English, we say that
type a, and a function that accepts
type aand returns a
type b. The result of
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 afrom 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.
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.
myChainis known as
>>=in Haskell, and is usually called