Friday, February 27, 2009

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.
Examples

Like many languages, Haskell provides tuples: e.g. (1,"hello") or (3.14, True). Consider this type signature for the function fst:

fst :: (a, b) -> a
This reads in English "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.

Thursday, February 26, 2009

Best Invite Acceptance of 2009

At my client site, I offered a dry-run of an upcoming talk on Monads (stay tuned for more info). In my email to the team, I gave some fair warnings that the talk would be über-geeky.

One wag responded:

Oooh... a brown bag on material that's inherently dry, well outside my comfort zone, and irrelevant to my future? I'M IN!

This is a wonderfully succinct definition of being a geek. These are my people.

ps. Before you begin to riot, Haskell/FP fans: neither my respondent nor I truly think monads are irrelevant.

Sunday, February 15, 2009

A Keep-Alive Post

Though it has no formal name, every blogger eventually writes a post to reassure readers that yes, s/he is still alive and well. Call it a keep-alive post that pings on the socket between the writer and the audience.

Such a time has come for this blog: the CtJ Nation has been clamouring for something -- anything -- to put some spice in their otherwise quiet browsing.

Things have been busy at CtJ HQ. It is a busy time for some personal pursuits, and also in preparing for a talk at the Lambda Lounge in March. I also confess that I've been distracted by the evil, seductive Twitter, much as I had feared.

Here are some quick notes on ideas in store for CtJ. Drop a line if any of these resonate with you:
  • My upcoming talk is on monads, and so I've been cramming Haskell from Real World Haskell. This is a gorgeous language, and shares some psychic fingerprints with Unix, in that _everything_ is on its terms. Once you accept that, Haskell makes a very good case for the power of strong, static typing.
  • I have been working in a war room for a couple of years now. This is fertile ground for blogging, but I generally avoid any subject that might seem personal towards my colleagues. However, I think I have enough experience (direct, or overheard) that I can safely abstract themes and episodes in a way that is essentially fiction. I'm considering a series called Adventures in Agility.
  • Ted Neward has written about women in IT. I've been thinking about something similar for a long time, since I am on this list about male privilege. It pains me deeply that I'm on there, as I agree that some of the items are issues. I'm a free spirit at the pub, but I'm genuinely mortified to offend anyone in the workplace, on any criteria. I've been trying to reconcile this with the famous sticker posts. I'm considering a piece on the criteria I use to rate someone as a geek (hint: it has nothing to do with gender, race, religion, etc).
And that's the news from CtJ HQ. Stay tuned!

Tuesday, February 3, 2009

Thursday Night's Alright for Byting

If you're in St Louis, have had it with the discipline, and want to get a little action in, then check out these events:

Thursday, Feb 5, there is only one game in town: the burgeoning Lambda Lounge will feature talks on Javascript (from an FP perspective) by Nate Young, and Actor concurrency in Erlang by Alex Miller (speaker at NFJS, Java One, and occasionally outside, at the corner of Terra and Cotta).

Thursday, Feb 12, the venerable StL JUG features another NFJS speaker, Ken Sipe, with a talk on Spring 3 Annotations.

For more write-ups, events, and a great local calendar, see this post over at Alex Miller's blog. There is a lot going on in the coming weeks in the "Gateway Valley". Come on out and take real steps towards diversifying your career!