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.

• Please elaborate on "fallacy by ignoring the logical significance of the transformation between 'the number 3' and 'the type represented by the number 3'".
  • Your primary failure is that it is always a fallacy for your arguments to rely upon non-given assumptions. That you ignore the transformation is the same as assuming the transformation is insignificant. Therefore, doing so is fallacy. If you'd like, you can try to prove that the transformation has no logical significance, but I'm not inclined to agree: transformations are non-unique, they change semantics, communicating the transformation requires communicating the new semantics, and this communication and transformation has a real cost in space and compute cycles. Taking 'X' and 'something represented by X' and calling them identical is generally a fallacy whether we're talking about type-descriptors and types, pictures and pictured objects, maps and territories, or anything else.
  • I'll explain further in the context of types. Types in any language are necessarily (as in any other possibility is logically precluded) represented by use of type-descriptors: words or phrases in the language for describing types. The choice of language doesn't matter... could be English or could be something more formal, such as classes and unions and enums and so on. It is possible to create languages that use the number 3 as a type-descriptor. For example, in one type-description language the number 3 might represent all types with 3 states (some homomorphism to 0,1,2). In another such language, the number 3 might represent the set-based type: the set of all values equal to 3. There are, of course, infinite possibilities. But, critically, none of those possibilities is the same as the number 3. Not for semantics. You can't add 2 to the type represented by 3. The type-descriptor is not the type; it is the semantics of the type-descriptor, which is determined by how the type-descriptor is applied in the language, that determine its type. TheRepresentationIsNotTheRealThing. The number 3 is not a type, even if it can represent a type. (and thus 'type' is falsified).
  • And is this merely a hazy mental notion, or is there an objective and clean way to test such a statement?
  • Sigh. I'll agree that it's a "hazy mental notion" for someone with a "hazy understanding of math" perhaps. When you appeal to your ignorance to call things 'hazy', it's your loss. I'm not going to deal any further with a HostileStudent; go learn the difference between representation and what is being represented on your own.
  • Continued on TopsTypeDeterminatorChallenge.

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.