[paganel]

I'm in a no way a computer-science expert, just a mere programmer, but by the looks of it this discussion all boils down to the (quite big, I'd say) impedance mismatch between real life ("computer programs" in this article) and us, as humans, trying to understand said life and applying rules to it (by in this case applying "type theory").

For example, looking at this:

>>> 0 if 1 else 'a'

made me remember one of me older thoughts on this subject, more exactly if the word 2/two from a sentence like this: "there are two apples on the table" should be treated as an Integer or a String. Some would say that we should only treat it as an Integer if we intend to do computations on it (for example adding those 2 apples to another 3 apples), to which I'd ask how come the word's essence (its "transformation" from a String to an Integer) changes depending on the type of action we intend to apply on it? (so to speak, English is not my primary language).

Anyway, things in this domain are damn complicated, and have been so for the last 2500 years at least, starting with Socrates (or was it Plato, in fact?) who was asking about the essence/idea of a table (i.e about its type), i.e. is a table still a table if it only has 3 legs remaining? what about two?, and continuing with Aristotle's categories and closer to our days with Frege and Cantor (somehow the table problem can be connected to the latter's continuum hypothesis, but I digress). So one of my points is that this is not only a computer science problem.

[Retra]

That 'table' problem is not that complicated once you understand the notions of 'approximation' and 'continuity'. A table with three legs is just a better approximation to what is meant by "table" than one with two, or worse than one with four.

It basically leads to things like this:

http://en.wikipedia.org/wiki/Domain_theory

[paganel]

And then I might respond (like many others did) that an "approximate" table is not a "real" table at all, i.e. we're back to step one of the problem.

The way I like to look at it is that Aristotle's logic principles and all that followed (including the concept of "continuity") is a very nice and especially very usefull Domain Specific Language which helped us, humans, fly rockets to the moon and build iPhones (we wouldn't have computers with NAND gates which would not respect Aristotle's logic principles). But if we go back and re-read Heraclitus, the guy against whom Aristotle fiercely battled, then the concept of "continuity" and "one vs many" concepts become a lot more blurry. But I digress, again, this was supposed to be about computer type theory.

[igravious]

If it's any consolation(?) I agree with you.

Plato's theory of Forms says: we can see around us many examples of horses. What makes them all horses? Why, the ideal form of a horse. Plato, I believe, then claims that these forms are perfect and timeless and the the actual world is inhabited by imperfect reproductions of these forms. Apologies to scholars of Plato.

Aristotle's Categories, while superficially, quite different I think is tackling the same problem. His most universal abstract categories try to answer the question, "what is it that all things regardless of their nature have in common?". And so his 10 (suspicious that, that 10) categories. His categories are very much rooted in language, as in they map readily onto parts of speech.

Both are ontological investigations. Both probe the essence of what it means to be something. And so on to the present day. Even though Russell was attempting to resolve a paradox in set theory what I think he actually did was answer the question, "what is a thing (any thing) in essence?" and I think the answer is, for our purposes, a term (instance) of a type (form).

It is not at all obvious how following these ancient investigations leads us to the door-step of type theory but all indications seem to point to it. You seem to have thought about this a good deal. I'd be interested in what you think. I've left out a _lot_ of detail but I hope what I've said is useful to somebody.

[Retra]

"Table" is just a word. If you want to know what the word means, you have to observe the structure of the patterns in it's usage. Words acquire meaning through usage (in context.)

There is no such thing as an "approximate table" per se, just things that can be approximately described by the word "table". It makes no sense to talk about a 'real table'. Every thing that exists is real, whether you call it a table or not.

I'm also confused why you'd think the concept of continuity is blurry on this issue. Continuity means that similar inputs give nearby outputs, and this is perfectly consistent with how computation works: if you construct two results through similar algorithms, they will have closely related types. Types become a measure of similarity of different computations, and thus you can use them to group things with similar linguistic structure, and thus similar meaning.

Either way, Aristotle and Plato were both ancient people with not even a tenth the information we have today, so I wouldn't consider them authorities on any part of this discussion.

[dllthomas]

"I'd ask how come the word's essence (its "transformation" from a String to an Integer) changes depending on the type of action we intend to apply on it?"

I think the problem is viewing "type" as "essence". Type is all about how we intend to use it, and which invariants we wish to enforce.

[snarfy]

Plato's Forms:

http://en.wikipedia.org/wiki/Theory_of_Forms