Questions For Type Definitions

These are questions that a good definition of "type" should be able to answer:

(Note: The TypesAreSideFlags comments are more of TopOnTypes. Comments with regards to its inadequacy, especially as a representative model for answering 'QuestionsForTypeDefinitions' given that it's just a few months old and nobody has ever used it for anything at all, should be directed to the associated page. Avoid unnecessary digression on this one.) {EditHint: remove this paragraph, it's merely "side bickering".}

What is the difference between classifications, taxonomies, categories, and "types"?
- A taxonomy needn't be based upon any extant properties in the organisms, though it may be based on particular structure or lineage. In the latter case, structure would constitute a 'type' (e.g. vertebrate vs. invertebrate) that can be used for distinguishing new instances and reasoning. In the case of lineage, one also has criterion for distinguishing and reasoning (though more about temporal shifts in other properties). A taxonomy also tends to be hierarchical, which is not necessary for types.
- 'category' is quite ambiguous in this context, possessing meanings with varying degrees of formality in each of taxonomy, philosophy, topology, and math, in addition to the less formal meaning in English (which amounts to 'a particular classification' or 'division'). The CategoryTheory definition of 'category' consists of both a formal collection of sets with particular properties called a 'class', and a bunch of 'morphisms', or functions from one set to another within the category. It's all quite difficult to understand without solving problems at the end of each chapter in a CategoryTheory book. 'Types' themselves aren't the categories, but could be associated with a combination of the property used to describe the mathematical class and the properties arising from the morphisms upon it.
- 'classification' (noun) is often used as another word for 'type' as it pertains to objects (thus the C++ 'class'). However, it also has more and less formal meanings in the English language, and many of the properties are similar to 'taxonomy'. Where 'class' is assigned, it may also create extrinsic properties, such as privilege granted in society. In those cases, the 'types' would be described by the properties so created (e.g. privilege in society) even if the current 'classification' is inconsistent with this property. In this latter sense, one can say that 'classification' occurs as part of an process attempting either to keep a record of type consistent with actual type OR attempting to keep actual type consistent with the record of type.
- TypesAreSideFlags viewpoint: Although side-flags can be used to track categories and classifications if one wants to stretch their use, usually they are used for more specific, narrow, and/or context-specific situations. They can overlap, but are generally different kinds of animals. Classifications are generally attempted global or wide-scale declarations about items. For an analogy, there may be many ways to determine a person's gender. However, generally a specific technique is selected for a particular situation or use. A given institution may decide to use the gender indicator as found on one's drivers license. That becomes their "situational" indicator. They are not interested in parsing one's anatomy or examining one's chromosomes. Types are situational abstractions.
What is the difference between validation and type checking?
- Performing a check of types for the purpose of TypeSafety is an instance of validation: it returns a truth value as to whether or not the program possesses a type-consistent description (for static type checking) or will be in a type-consistent state for the next operation(s) (for dynamic type checking). Type checking for other reasons, such as to perform function dispatch based on types, is not validation. Validation certain other purposes (such as stress-testing a rope before using it, or checking whether a certificate is expired before trusting it) can constitute type-checking (where 'strong rope' or 'unexpired certificate' are types) - in a sense you can say: a sufficiently advanced language might be able to make these checks implicit.
- Input Validation cannot be type checking. Input Validation is testing that a runtime input describes a meaningful object or value. This cannot be performed statically for the obvious reasons, but (more interestingly) it cannot be done dynamically either, because you can't know until AFTER you've received the input as to whether you're in a type-consistent state. So Input Validation cannot be type-checking or type-safety, though it is necessary to perform if you're going to provide type-safety in a communicating system. Automated input validation just as convenient as automated type-checking. Good languages designed for networking will provide it where they can. (Other languages, like C++, will screw up.)
- Validation of consequence, that you've not already entered an unknown or undefined state or otherwise broken something, is not type checking. This is, however, what people often mean by 'validation'.
- Validation of non-observable properties such as true authority, cannot be type-checking. Even being super-generous to a type-system does not allow for it to 'check' for more than the observable artifacts or symptoms of authority, such as possessing a (possibly forged) ticket or presenting a (possibly stolen) eye to an iris scanner.
- TypesAreSideFlags viewpoint: Validation usually requires inspections or parsing of values themselves. Types are indicators that describe values, not analyze them. Types are a noun while validation is an activity.
  - I submit that you misread your own question. What is the difference between validation and type-checking?
  - Fair enough. Type checking only checks the type flag. Validation may also involve inspection of the value itself.
What is the relationship between parsing and types.
- Parsing obtains structures of implicit, known types from a representation of the language. This occurs even at the lowest levels of the lexer where one results in a stream of different tokens with different, and continues into the parser where one identifies bigger structures with different properties, such as function definitions, type descriptors that exist within the language, and procedural operations. In some languages, the parsing of structures in one space can affect how one parses structures in another space... this is common with ExtensibleProgramming? using extensible syntax. In this case, types described within the language may, themselves, directly affect further parsing.
- However, there is no direct or necessary correlation between the types required to understand language structures and the types available to the programmer for purpose of consistency checks between language expressions.
- TypesAreSideFlags viewpoint: Parsing is the activity of analyzing a value. Types are indicators, not an activity that inspects values. A type could be comparable to the Gender indicator on your driver's license, but a gender test to qualify for the Olympics is more comparable to parsing because it requires inspecting details of the value (your chromosomes from inside of you).
If a program, interpreter, or compiler does not explicitly track types, do types still exist?
- That question waxes philosophical, like asking: "If I shred my math homework, do the solutions still exist?" The answer depends on whether you view yourself as having found a solution that exists whether or not you find it, or as having created a solution that didn't exist before you wrote it down. Most mathematicians would say they find solutions, and would say that the types always exist (even if they never use or think about them). OTOH, they don't have the solution after shredding... unless they happen to remember it. In either case, the answer is 'yes' if the program, interpreter, or compiler still implicitly tracks types (e.g. in the structure of description). That's not an interesting answer, though, so we'll move past it.
- Reworded: If a program, interpreter, or compiler does not track types (explicitly or implicitly), does it still have types?
- The answer is no. An interpreter or compiler takes a programming language source that describes meaningful types for such tasks as type-based dispatch and consistency checks. Then, after performing these checks and dispatching, they often translate it into another programming language (like machine code, or bytecode) that lacks these type-descriptions... or any way to find them, explicitly or implicitly. Since the types are no longer represented in this final programming language, it cannot be said to 'have' them.
- TypesAreSideFlags viewpoint: Types do not exist until a flag(s) that is distinct from the value is created or is readily identifiable as separate. If types are determined from parsing of a value(s), then the "type" is the determination (result value) left over from the parsing process. When the flag (determination) is discarded, such as after a subroutine is finished, then the type ceases to exist.
Must a 'type system' have one or more types?
- A system of types needs at least two types such that you can usefully distinguish between the one type and the other type. Further note that in a system with exactly two types, one of the two types is 'all these things', and the other type must be 'everything else'. Hence, the answer is yes.
Is it necessary to represent types as part of a 'type system'?
- This is a greater question, one founded more in a definition of 'type system' than of 'type', and the answer is 'yes'. If the meaningful use and representation of types implies that a 'type system' already exists, then, trivially, yes... but it's hardly an interesting property. If, instead, you define a 'type system' as something that includes both means of describing types and associating them meaningfully with objects (either via percept or concept) AND possesses rules on how these objects of certain types interact with one another, then the answer is still 'yes': the rules themselves are what ultimately give meaning to the type-descriptors. The rules are what can prove you wrong if, based upon observation of properties and behavior, you assign a type to an object; you're 'wrong' the moment the object does something inconsistent with the type you assigned it. And, if you create an object that is to be consistent with a particular type, the rules are what bind its properties and behavior.
- TypesAreSideFlags viewpoint: Yes. A "type system" is the management and tracking rules for type flags. If there are no types, then there are no flags to track. "Types" can still be created by and tracked by the application, but that is a case of an informal, ad-hoc, or self-rolled type system. Values are often parsed and re-parsed frequently in languages without a formal type system (or a reduced one). This may slow the run-time process down, but may have other benefits, such as ad-hoc module inclusion, WYSIWYG value inspection, and faster testing.
Are type systems required to provide conversion and substitutions among types?
- No. An implementation of a type system would be incorrect if it failed to provide substitution or or coercion among types in at least the case where one type strictly encompasses another (e.g. 'abstract syntax tree' to 'tree'). However, there are plenty of type-systems that do not allow people to describe types such that one wholly encompasses another (indeed, some languages don't allow people to define their own types at all), so not all type-systems have need to provide this.
- It is also common that type-systems in mid-level languages (like C++) tend to conflate type and representation of the type, which is harmful for flexibility and theoretical correctness, but good for efficiency. (To be fair, it should be noted that the next generation of C++ will possess far greater ability to handle different representations of the same type of object using what they're terming 'concepts'.)
- TypesAreSideFlags viewpoint: No. Substitution and conversion are often a nice feature, but not necessary to qualify as a "type". For example, a language may offer only two supported variable types: strings and arrays. (Assume strings are used to store numbers also, similar to what many dynamic or weak-typed languages do.) The language may not offer any built-in way to convert from a string to an array and visa versa. It may also not allow one to be used in place of the other. However, variables are (at least) internally flagged as being either an array or a string (scalar). Thus, types still exist despite the strong wall between the two types in this example.
Are types based on trees or sets or some other data structure?
- The notion of 'type' isn't tied to any particular data-structure. Rather, types are based in computation and making distinctions between one thing and another. That said, any modifiable or configurable type-system will need to leverage data structures to describe the relevant types. It's just that the choice of which particular data structure to use is arbitrary and doesn't at all affect the nature of the types. A representation is not the thing so represented.
- TypesAreSideFlags viewpoint: No. Trees, sets, etc. may be useful to implement a type system, but that kind of detail is below the definitional level of "types" and is an implementation detail of a specific language or tool. There are many ways to implement types and type systems.
What is the relationship between "types" and SetTheory?
- There is no logical relationship, but there are some relationships between the two in practice of TypeTheory. I will generalize these relationships into two cases: (1) systems that use 'sets' as a DataType, (2) a TypeTheory based on SetTheory. These cases are not mutually exclusive. In both cases, SetTheory might be indirectly referenced (via lattices, equivalence classes, relations, CategoryTheory, etc.)
- Theories that represent 'sets' as DataTypes themselves fall into a couple different classes:
  - First, there are theories that use 'sets' to describe complex structures. For example, the number 3 might be represented as {0 1 2} or, fully expanded, {{} {{}} {{} {{}}}}. These are often based on ZermeloFraenkelSetTheory? due to its well-founded property (see WikiPedia). A practical approach along this lines is ExtendedSetTheory, which identifies the 'roles' each element plays in a given set, thus offering convenient means to precisely describe subsets (which is necessary for projections, transforms, etc.)
  - Second, there are theories that use 'sets' as more a collection principle, where the 'set' contains items of a uniform structure (i.e. another type). These types could further be refined with partial uniqueness requirements (e.g. 'candidate keys'). There isn't anything really special for TypeTheory here... but from a LanguageDesign perspective, sets as collections offer a convenient principle for data-parallel operations and logical operations with automatic refinement (via uniquification).
- There are many, many TypeTheory systems that have some basis in SetTheory or a related discipline (like CategoryTheory), especially for description of either DataTypes or functions. However, in practice, the full power of SetTheory is often restricted quite heavily. I suspect the author of the question is looking more for a relationship to 'set' characteristics (in particular, support for overlap of types) than the relationship to SetTheory axioms, so I'll name a few general classes of TypeTheory systems that are close (in characteristics) to sets:
  - Type-theories that support PredicateTyping allows refinement of a structural type (for example: integers) into a subset (for example: even integers, or positive integers). Using PredicateTyping systems allows for subtypes to overlap (some positive integers are even integers). (In practice, languages that support PredicateTyping must do so dynamically).
  - Type-theories that support structural equivalences form inherent subsets and infinite lattice-structured (http://en.wikipedia.org/wiki/Partially_ordered_set) subtype relationships. For example, a record (a:Number, b:String) is a subset of (b:String) and a superset of (a:Number, b:String, c:Function) based on operations equivalence. This is sometimes called StructuralTyping (see NominativeAndStructuralTyping), and (more specifically to OOP) it is called DuckTyping. Dynamic languages often support DuckTyping. C++ (via template programming) and Scala (mixins and re-interpretations) support static DuckTyping.
  - TermRewriteSystem?s are based on equivalency-classes between values, and the 'modules' in such system tend to define types in terms of sets. You could learn more by exploring MaudeLanguage? or ObjLanguage.
  - Attribution types (common instance including volatile, read-only, write-only, etc.) tend towards combinatorial factors and have (vaguely) set-like properties for overlap (e.g. 'integer' may be usable as a 'read-only integer' or a 'write-only integer').