This was a great essay. Type systems are one of the holy wars of programming, and I don't think there will ever be a truce. I think it is is great to see some writing that explains why that occurs, and how to think about the situation. It is also interesting to see some things that I haven't thought about: Type systems can encode effects that could free the programmer from thinking about locks? Dependent Type Systems can perform program synthesis? Where can I find out more?

I know anonymous predictions from nobodies on the internet are completely uninteresting, but I can totally envision this as one of the essays that gets linked hundreds of times over the next decade or two on the front page of HN with a (2015) in the title.

If nothing else, your anonymous prediction pleased the author :-). Thank you!

Dependent type literature will answer both of your questions relatively quickly. Also look at "proof search" in that context.

I personally think a truce is coming with python3 static typing. As long as type systems have an 'any' type which is the default, then dynamic languages and do everything.

The claim that the concept of "type" is not formally defined, is rather like saying that the concept of "logic" is not formally defined. In both cases there are several competing, completely formal definitions, each with their own scope and uses.

If one is really serious about studying types one should read some of Per Martin-Löf's more philosophical writings on the topic. In his dependent type theory there is a clear extensible philosophical notion of what constitutes a type (being defined by its introduction rules) — and a clear computational meaning.

The fact that one needs concepts like monads to describe effectful programs is not really more surprising than the fact that one needs the concept of a mathematical manifold to describe certain parts of physics. The cool thing is that these mathematical descriptions of effect can actually be used to do effectful programming, thanks to the computational nature of types.

Type has a formal definition for sure, but it is quite different from its more accepted informal definition. There are also those who study types for the sake of types and those who are more interested in type systems for the sake of building programming languages...these are increasingly very different fields.

While the title and some of the text is indeed a bit of trolling, the text contains a number of interesting topics for contemplation.

The content is sure to be against the grain both for pro-static-types and pro-dynamic-types crowds, but it's worth to at least skim the text.

Maybe flexible context-aware mixing of the type systems (including an absence of the one) is the answer?

They said in Shen it's possible at least - https://twitter.com/deech/status/594874467412680705

Question for the author: what books do you recommend for a gentle but still substantive introduction to type theory? Books such as Pierce get super complex very fast. Thanks!

TL;DR 1) The definition of "types" is non-static across contexts. 2) This is probably fine, so stop trying to make it so.

Did I interpret this right?

I'd say this is close, with a slight twist.

Insisting on a formal definition that would work across contexts is harmful. If someone comes up with one, that's nice (I doubt this). But even then, others might come up with "type systems" that fall outside of this definition and that's still perfectly fine.

The twist is that we do not need formal definition to talk about types across multiple contexts. I do not know what the best way to do this is, but the essay has some suggestions inspired by philosophy, which might be interesting precisely because they do not need clear formal definition.

His summary ends with:

"Rather than seeking the elusive definition of what is a type (which does not exist), I believe that we should look for innovative ways to think about and work with types that do not require an exact formal definition."

So he doesn't want to stop at your point 1, but rather wants to find generalizations that apply to the commonality between these variations.

I thought he was calling for exactly the opposite? A generalization that applies between contexts would require formal definition, no?

No. There may be some magic formal definition that would work between contexts. Until we have such a definition, though, he says it's better (at least between contexts) to work off of an informal, inexact definition, and to be aware that you are doing so.

In the introspective human experience, classification comes from observation.

First, we have a unique exemplar. This is the first thing we see of whatever "type".

Then, we notice a similarity of something else to the exemplar. The exemplar defines the "type", and this new object is classified as similar, usually with some amount of noted variance.

Once we notice a large number of similar observations, we tend to back away from a single exemplar, to a more nebulous classification defined by mostly-present similarities in that rough group. The "exemplar" of the type is now a more vague ideal, not any particular instance.

This is the point at which we try to nail down exact types, to attempt to again make concrete the exemplar of the type, but fall short in the ways similar to what the author brings up. The similarities we observed were because in some particular context, the similarities of the rough group of type members are important, while their differences are less relevant. In another context, these differences might become more important, and the similarities binding the classified population together for the defined type are no longer relevant.

The "type" is NOT a feature of the object, but emerges in the combination of a cloud of objects with the context in which the type is useful.

One common example is defining "car". Is a pickup truck a car? If not, what about an El Camino? An 18-wheeler? A van? Minivan? A 3-wheeled vehicle? Enclosed motorcycle variants? Race cars? Go-karts? Remote controlled cars?

Across the contexts of personal transport, convenience, repairs, insurance, speed/handling performance, etc, the similarities between vehicle types vary. Those vehicle instances which are of similar type in one context might not be of similar type in another context. What is exactly meant by "car" with no additional context?

I do a lot of AI work, particularly rational and symbolic. This needs to know, reason about, and explain particulars, not just return an unexplained impression of relevant associations as a lot of modern AI momentum deals with (successfully, I might add). But the notion of a "concept" or a "type" is certainly contextual, and relates to how the cloud of potential exemplars offer important characteristics to the current context. I have discarded the notion of explicit programming-language style "type" in my work, as far as the "understanding" part of AI goes, in favor of a more vague "concept" existing in a contextual cloud of exemplars, in pursuing a more hybrid classical/symbolic + modern/statistical AI approach. (The underlying implementations dealing with generating and compiling source code still has distinct data types, though.)