Tops Type Theory Discussion

Can the application of this definition be falsified? In other words, can somebody find a construct or thing which is clearly not a "type"? Example? (And I don't necessarily mean "good" types. We should allow poor typing systems to count as "types" dispite poor quality or potential contradictions.)

First, even good "type systems" are not "types", so poor typing systems shouldn't qualify as "types" either. Second, you shouldn't attempt to involve type-systems with "potential contradictions": if you accept a type-system possessing contradictions, you can use it to show that true is false, the sun and the moon are the same celestial bodies, and anything else you want... e.g. that everything is a type, and that nothing is a type (at the same time!). Third, yes, it is possible to construct a thing that is clearly not a "type" with regards to any given consistent type system.

Suppose we had a language that had a "goofy" type system. If an operation encountered two possible types to interpret an operator under, it would randomly pick one. Most would agree such a language had a "type system", just not a good one. If what you are saying holds true, then there is a disconnect between how regular Joe's see "types" and TypeTheory. It's like only allowing good bridges to be called bridges, when bridges that fall down or wobble too much are still "bridges" to most people, just not one they would want to use. The essence of bridgeness does not guarantee reliability. Thus, it seems TypeTheory is a system to produce reliable bridges....uh types, not a tool to define types in general.

TypeTheory is a mathematical discipline. Your own understanding of it seems far from the truth: TypeTheory is not a "system to produce reliable types"; it is a "study of reliable systems for typing". That is, TypeTheory studies TypeSystems, not types directly. And we do encounter the occasional crackpot approach to typing that we can disprove as unsound or inconsistent and therefore useless.

The analogy to bridges doesn't hold so well. An inconsistent type-system is more like a bridge attached to only one side and leading nowhere, and I don't believe even Joe Regular would call such a thing a bridge ([though apparently at least one American politician does - JayOsako]). If you wanted to discuss unreliable type-systems, consider instead consistent type-systems that are merely unsound or that possess loopholes in their structure.

[Computers are a virtual world where people can define silly types, such as even a TNullNull type if they want. This has nothing to do with the usefulness of types. Types are for classifying. If some idiot makes a TNullNull classification (type) then that is his own fault. Just as one can make a silly function in any programming language that supports functions or procedures. Does that make functions or procedures bad too? i.e. let's try and falsify what a function is? What is this falsifiable obsession we have?]

By "falsified" the above author refers to the practice of identifying a pattern that does not fall under a definition. It is a useful tool to judge definitions (we only need one word to describe 'everything'; more than one is redundant). But the author misapplies it, and mistakenly attempts to wield this tool as a weapon against 'types' among other things. I suppose this comes across as an 'obsession', but really it's just a classic case of a little boy with a hammer.

The basic crux of his fallacy is that he very consistently mistakes the map for the territory, the representation for the thing represented. Or at least he does so in mathematics fields. For example, if you said: "the number 3 isn't a type", he'd reply "an integer can represent the type of all values equal to that integer". And if you said: "the number 7 isn't a function", he might reply "the number 7 can represent the function that applied to another function applies that other function 7 times ((7 f) x => f (f (f (f (f (f (f x))))))))." There are, of course, any number of natural morphisms between integers and functions. His basic argument is: if X can represent (or be viewed as) Y then X must be a Y. As far as 'falsifiability' goes, he then requires 'falsifiability' while playing this HumptyDumpty game of finding some way to 'view' any proposed counter-example as an example. He doesn't 'get' that he just committed a fallacy by ignoring the logical significance of the transformation between 'the number 3' and 'the type represented by the number 3', or 'the number 7' and 'the function represented by the number 7', or 'the side-flag "interger"' and 'the type for integer values'. I don't even believe he wants to 'get' it; he wants to believe EverythingIsRelative is more than just a StrangeLoop - it's almost his religion.

As far as 'falsifying' a function, that is easy: the number 7 is not a function. Functions have domains and ranges and are applied to elements of the domain to produce just one element of the range. The number 7 has no domain, no intrinsic semantics for application, and no range. The number 7 can be viewed as a function, and can be represented as a function, but is not a function.

We're here to falsify types, not functions. Thus, your paragraph is irrelevant.

7 is also not a type. And that paragraph is not irrelevant: not only does it answer a question that was written above, but it helps explain by analogy to illustrate that, just as you cannot logically assert that 7 is a function simply because you can invertibly transform it into a function, you also cannot logically assert that 7 is a type simply because you can invertibly transform it into a type.

[The clear distinction between values, variables, and types falsifies each of them. If a value is not a type, then type and value are not equivalent, and are falsified. If variable X holds the number 7 as its value, and variable X is of some type, then 7 itself is not a type, it is a value. The type variable X is, may be an integer, or a byte, or something that allows the value 7 to be set. A HostileStudent would claim that values are just types, and values are just variables; there is no distinction between them, they are the same, and therefore nothing has been falsified. Nothing will ever be falsified with this sort of attitude. A HostileStudent would claim also that there are not different types of apples you can buy in the store, because types don't actually exist. Types of apples we purchase are just another UsefulLie. There are no types of apples. ]

Again again again again again, you are focusing on the trivial/simple examples. It's the more complicated ones that have issues we really care about. Strawman. And calling me a HostileStudent is hostility on your part. Projection. I'm not your student and take offense to implying I am. Pat your dog on the head, not me. The classification of apples may matter in special and controversial instances, such as cross-breeding with pears and border-crossing rules in agricultural states. Sometimes classification differences do cause political and social problems. Human "race" is one such example.

View edit of February 5, 2012 or FindPage with title or text search