Why I Never Met a Type System That I Liked
A type system is a means to represent to formal relationships between values, and constrain the possible expressions of variables. Like most tools, type systems are designed to make solving certain classes of problems easier. If you have a problem which involves optimizing compiled code or avoiding unnecessary compilation, say you are a compiler or language designer, type systems are great! They let you reason about code your users will write, and constrain them into phrasing their expressions into highly regular forms.
If you are on the receiving end of this equation, type systems aren't nearly as useful. Rather than making it easy to model your particular messy organic reality, a type system forces you to design a crystalline structure of pure math which will likely bare little resemblance to your situation. Sure the code may be fast, but it will also be inflexible, brittle, and prone to shatter under the repeated blows of changing requirements and unexpected design refactorings.
Like crystals, most type systems derive their elegance from their purity and regular internal structure. They are often works of mathematical beauty, with clean lines of symmetry. They're also notoriously hard to work and wedge into oddly shaped wholes or build load bearing structures out of.
In contrast, typeless systems, especially object oriented ones, are more like clay. They are morphable, fungible, and exceedingly malleable. They are wonderful for building conceptual models, quickly handshaping prototypes, and filling in gaps. They are however prone to deformation under load, and can easily produce unmanageable messes when used by unskilled hands.
Most production code in industry is written in what I would call metallic languages, much more rigid than the soft claylike typeless systems, but far more malleable than the strongly typed pure systems. C is the best example of these sort of languages. It has types, but they are easily avoidable. You can work around ear any type restriction with a simple cast, and can arbitrarily overlay one type over another through unions and structures. The compile only protects you as long as you keep the safety on and you do not use the language in any clever ways. Most compiler writers and language implementers exploit C's malleability to make their languages work in reality.
And this is much the issue with type systems, they're great math but horrid language. The real problem of programming in the real world is programming is an art of making believable models of systems. A program is an exercise in what some would contend is medieval thinking (others measure units of arrogance in computer science in nano-Dijkstra), an aggregation of analogies that parrot the desired reality. I would contend that this is the nature of language, and wherein it differs greatly from pure math.
In a real world, we have words and things and actions that those words represent. We string together words in complex arrangements called syntax to express concepts and communicate with others. Sometimes we try to use those same words with a machine to varying degrees of success. Underlying this world of words and things is a semantic gap, where in there is a considerable degree of play between what I said, what I meant, and what you understood. This gap arises from my mental model and your mental model containing different representations of reality.
Imagine a house, what color is it?
Imagine a goat, what color is its beard?
Odds are good, we have different answers to those questions. When I thought about it for two seconds, I realized that my answer to the house question also varied by context:
Q: Imagine a house (generic), what color is it?
Q: Imagine a home (generic), what color is it?
Q: Imagine your house (specific), what color is it?
A: Gray and lavender
And if you asked that same set of questions, you'll probably find your answers shaped by your environment, your experiences as a child, and your current situation. These sorts of realities aren't even static, and change over time as our understandings of the world change. This is why language too adapts and grows, adding new words and forms. The speakers are not static, and the living are defined by change; the dead slightly less so.
If you look at all long lived programming systems that are useful, something peculiar arises. Vocabulary. You can't help it, the sole difference between a toy language and a real language is the number of useful things one can describe in a word or two. People choose languages based on their popularity once they reach a critical mass of vocabulary. Once a word exists for most of the common idioms in your problem space, you have a sufficient vocabulary to explain how to solve he specifics of your problem. Without that vocabulary, you are reduced to either inventing it or struggling to find the right words to express the ideas in more primitive forms.
A type system is ultimately a most primitive form. No matter how elegant the engine, any time one must think in terms of the type system itself, there is a failure of applicability. Falling back to the type system as the basis of expression requires thinking in a context outside of the problem domain (unless of course you are a designer of type systems or their tools), and require a cognitive dissonance, a violation of the user illusion that makes the language suitable to the task of describing the problem.
This is where languages like Self and Smalltalk really show their true merit. The syntax is regular and small, the expressions are primarily concerned with the vocabulary of the objects which narrow vocabulary to a specific context. And it is in the context of a cluster of objects, that the programmer converses with both the reader and the computer. To understand the vocabulary of a set of objects is the only barrier to reading a program. Like with human languages, understanding the analogy between the words and the things they represent are critical to reasoning.
Behavior rather than formal relations can structure in a way that more closely models the idioms of the exterior world. In physics, we describe a model of the world through mathematics. But the conceptual model of the relationship and the nature of the bits lies outside of the math. The math alone is not a sufficient description to enable understanding:
F = ma
Is meaningless without a larger context and conceptual model. What is F, and ma? Is ma a product or a variable? Is it an assignment or a truth statement? What does it mean with respect to the reader? You can say, F is force, = is equivalence, and m is mass and a is acceleration. You can say F is measured in kilogram meters per second per second, but none of those things mean anything without a context assumed by every thinking mind in a physical universe where things move, have substance, and act upon each other by various means.
Language alone is not a sufficient description of any problem. Formal relationships alone, such as F = ma, are also insufficient. What is necessary is a semantic connection to an external context. Unreadable code is code for which the reader lack sufficient context to understand. A type system does not produce readable code or even the ability to reason about code, it merely allows you to reason about the behavior of the type system itself. It provides a self contained context into which all other contexts must be wedged. By constraining the expressiveness of the expressions, the type system limits the possible interpretations of words in accordance to rules laid down by both the programmer and the designer of the primitive types. It gives some programmers an illusion of familiarity, as there are bits they understand, although they may lack the ability to understand what the program does or how it works.
That is the reason I have never liked a type system. It gives a false sense of understanding and accomplishment to an audience who should know better. It makes programmers who practice black box programming:
"I feed it input till it doesn't blow up and does roughly what I want"
A misplaced sense of security just because of the amount of effort necessary to make the code compile. It also encourages those of the pure mathematical bent to prove they are correct even when they are wrong. A probably correct program that does the wrong thing is more worthless than an unprovable program that does not. I can not prove a program will meet the user's expectations, nor can I prove that I understood the requirements in the first place. Most program bugs result from these sorts of misunderstandings than from errors in the types of values used. No amount of formalism in language constructs wil solve that problem. If it did legalese would be the most legible language imaginable. The excessive formalism of contracts and legislation both directly impede the understanding of the vast majority of users who lack the perquisite encyclopedic knowledge of legal terminology, which like most programs, can change from contract to contract.
Some formal structure to language is good. It helps provide standards for communication that are agreeable to most parties when no generalizable ideal exists. But most formal language in the real world revolves around convention and not definition. In our dictionaries, words mean what they mean by how they are popularly used, not because of what was written in the book. Words often many, sometime contradictory meanings, like:
Dijkstra is dope, yo!
Dijkstra is a dope, yo!
Totally different meaning, same word, different usage. You can model the types of the words:
Subject VerbIntransitive Adjective, Utterance!
Subject VerbIntransitive Article PredicateObject, Utterance!
No type checking will prove which is correct.