Why types? -- lambda, the main course

First the surreal, then possibly one of the most interesting threads I think I've seen on lambda. Probably why I'm now clocking 10 hours catching up on lambda, and not only am I still at it, but I'm still motivated.

In Why type systems are interesting, Anton van Straaten lifted a comment by Luke Gorrie to a toplevel discussion:

If someone could next show what makes type systems so interesting in terms that I'll understand then I'll be well on my way into the modern functional programming world.. :-)

and in doing so launched a fascinating thread that has seen 44 posts so far and launched at least one independent thread. I seriously recommend this thread to anyone who considers themselves a serious programmer. A few highlights:

Anton managed to summarise the thread in the introduction:

When you write code, even in the most dynamic language, you always know something about the types of the values you're operating on. You couldn't write useful code otherwise - if you doubt that, try coming up with some examples of operations you can perform on a value without knowing something about the type of that value. Type systems provide a way to encode, manipulate, communicate and check this type knowledge. In an earlier thread, you mentioned that you write the types of functions in the comments. That's an informal type system! Why do you do use a type system? Because type systems are useful, important, and as a result, interesting.

Note that the first paragraph is deceptively simple. Consider the most common example of a generic data-structure, the list. If you have a truely hetrogeneous list, one whose contents are truely untyped, you your list is actually indistinguishable from a natural number! The only operations you can perform on a completely typeless list form the monoid ([], Lists, concat) which of course form a monoid isomorphic with (0, Naturals, +), and supports the Isomorphic Arrow length() mapping lists and naturals. For a fuller discussion of this I recommend Basic Category Theory for Computer Scientists, Benjamin Pierce (and before I get asked, I borrowed it from my local university library).

Anyone who has been reading lambda much immediately recognises Frank Atanassow, his writing style is distinctive, and his opinions both strongly held, and consistent. One of the really exciting things about this thread was that Frank's comment Rebuttal finally managed to clarify for me, what he has been talking about these past months. Although if you haven't been reading lambda much and intend to read that post I would strongly advise you read No contraints[sic], and keep in mind Anton's comment in Constraints

if b then 42 else "ha!" becomes something like: if b then Num 42 else Str "ha!" ...where Num and Str are type constructors for the Univ type. This is kind of ironic, considering that it's the latter language that's supposed to be able to inference types. You can think of dynamically-typed languages as a shortcut syntax for creating programs which rely on a universal type. This demonstrates that statically-typed languages can be less expressive than dynamically-typed ones. emphasis mine

It was also very amusing to watch a curveball from Julian Squires who wanted to know how static type systems interact with his desire to actively develop an executing application (think smalltalk, or possibly php) in Re: Software development as a static activity. Personally I'm not sure any existing languages combine a modern static type system with the ability to do runtime modifications. Still even if you only consider static type checking a safety net, surely one time you would really really like to have it is when doing something as delicate as runtime development.