Against the definition of types

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.

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.

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?

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