But that's not really why I find them interesting. Mostly, I just find most type theory simple and beautiful. It's fun and gives me a new perspective on how to think about computation (as transformations between types).

Also, while a type system restricts the set of possible programs, it can actually make a language more expressive. Haskell's typeclasses make a whole bunch of things much nicer: custom numeric types, overloaded string literals, monads, QuickCheck... All this is far uglier in a language without typeclasses.

Coincidentally, I'm very excited that Rust is promising to bring much of the typeclassy goodness to low-level programming. It really does make life much nicer, and promises to bring some progress to the otherwise seemingly stagnant field of systems languages. I think that's the sort of innovation we really need rather than Go, but I'm obviously very biased :).

However he is willfully ignoring the fact that perfect correctness is not a requirement for most programs. He might be unable to sleep at night without knowing that every case has been accounted for, but in the real world you can often create tremendous value hacking together a vague idea of what you need. Piping some text files through an ad-hoc perl script can be incredibly useful even if the script has horrible horrible bugs due to unconsidered cases.

Atanassow seems to be arguing that the fact that the perl script has bugs that would have easily discovered in a statically typed program nullifies the benefit of rushing a script out the door that produces the correct output for the output at hand even if the incorrect cases would never be run in practice. This mentality is a luxury afforded to PL researchers and other people who are paid purely to think, however it does more harm than good to bringing the powerful ideas in modern functional programming to the average programmer who, in my opinion, is in desperate need of them.

His reasoning is sound, but I have an intuition as to why his conclusion is a bit off: Dynamic languages may be less expressive, but it can be much simpler to write, and especially modify, code without having to worry about two different sets of type semantics. Take the situation where you have a variable whose type was originally static, but now, because of a new requirement, needs to potentially take on values of different types determined at runtime. With a dynamic language, this probably isn't a major issue -- just assign the new values to the variable, and change the code to handle the new values where necessary. With a statically-typed language, you may have to redesign the entire static type structure of your program to change what were static "types" into dynamic "tags" and create new static types to handle those tags, which can mean major surgery.

Sure, a well-designed type structure is important even with a dynamic language, but in real life there are so many cases when it just isn't worth the time to refactor your whole design just to add a new feature. More than that, big refactorings can introduce bugs, and who honestly has 100% test coverage?

In a large enough project with a large enough budget, redesigning to maintain a proper static type structure is always going to be the better choice when viewed over a long enough time frame. As another commenter put it, statically-typed language are only "asymptotically superior". My sense is that, for finite projects/budgets/timeframes, ditching strict static typing is often a useful simplification, even if just to make a program easier to understand for busy programmers with finite available attention.

Just a thought that occurred while reading the comments -- I may not really know what I'm talking about.

I've bookmarked the page for later reading as the discussion is far too huge to process in a single sitting.

Interestingly, the fact that this reduces the domain of possible functions significantly is specifically what lends static type systems incredible power, such as described by this author who has never run his own (deployed) Haskell libraries: http://r6.ca/blog/20120708T122219Z.html

For example, the only obvious function that goes from A -> A for all possible values of A is the identity function - and I'm struggling to think of any other non-obvious function that could do the same.

Of course, this only works with highly polymorphic functions, but that's still a huge statement.

    foo = head . (:[])

Not to be pedantic, but being a functor has little to do with the fact that you can add and remove elements from lists.

Knowing that a particular type is an instance of `Functor` tells you only one thing about that type: that you can `fmap` functions over its contents. But look at `fmap`'s type:

    fmap :: Functor f => (a -> b) -> f a -> f b

Extraction of contained values from a wrapper and lifting/insertion of values into a wrapper require pattern matching and constructor application respectively, which means the type must have exposed constructors, a property independent of whether that type is a functor.

  head . (:[])

The set of functions with the type \alpha -> \alpha is trivially infinite.

f(x) = x - 1 for \alpha = Z

is an obvious example that's not the identity function.

Or do you mean the function

f(x) = x

because obviously there is only one such function (and it's called the identity function).

Moreover, there is no non-⊥ value of the type ∀α. α.

There is a tool called Djinn which can actually provide functions of such sufficiently constrained types. Another example would be the type ∀α.∀β. (α, β) → α, which only contains fst.

Even types that contain an infinite number of functions can have interesting constraints from polymorphism like this. For example, the type ∀α. [α] → [α] contains a whole bunch (for sufficiently infinite values of "whole bunch" :P) of different functions. However, you are guaranteed that the functions can only affect the structure of the list: the function cannot create or modify values of type α in the list. So the function reverse would have this type, but a function which added 1 to each element of the list could not. Moreover, a function of this type would always have to map [] to [].

What? The whole point of what you're replying to is that \alpha remains undefined. Once you specify \alpha, of course you can specify more interesting functions.

IOW, write a function that works even if \alpha is a composite datatype the details of which I refuse to disclose.

That question is very weird. Not all functional programming languages are statically typed (btw the answerer specifically mentions that we're talking about static typing here).

For example I'm having lots of fun with monads in Clojure right now. Very functional. Not statically typed at all.