Consider merging this page with TypingQuadrant
TypingQuadrant seems to be about classification of languages; TypesOfTyping seems to be about defining the terms.
Actually TypingQuadrant was meant to be about defining the terms through the classification of languages. And if you're looking for good definitions there's always LucaCardelli's paper on the subject: http://citeseer.nj.nec.com/cardelli97type.html See CardelliTypeTerminology
No one seems to be able to completely agree to what they are or how they are defined. But here's a stab at it, trying to be simple:
- StaticTyping
- Types are checked by the compiler.
- DynamicTyping
- Types are checked at run-time.
- StronglyTyped
- Run-time type errors either cannot occur or cause well-defined behavior, except for "loopholes".
- StronglyTypedWithoutLoopholes
- Run-time type errors either cannot occur or cause well-defined behavior, always.
- WeaklyTyped
- Run-time type errors can occur and cause UndefinedBehavior.
- NominativeTyping?
- Types of values are differentiated by programmer-specified names (two differently-named types which are arrays of 5 ints are differert types).
- StructuralTyping
- Types are defined by the structure of values (two differently-named types which are arrays of 5 ints are the same type). See NominativeAndStructuralTyping.
I do not think that upcasting constitutes a change of type, but downcasting certainly does.
- Huh? This would require some strange rules for type (in)equivalence, or it could be argued that with B-(up)->A-(down)->B the two B-s end up with different type. (The type of A is equal to the first B but different from the second B.)
TypeInference is a separate issue; like optimization I'd consider it a compiler feature rather than a language feature.
Type inference is definitely a language issue, since it dictates where type information must be written or can be elided in the source text.
- There is TypeInference as an optional compiler feature, but more often TypeInference is a feature of a language; pure functional languages like Haskell cannot be implemented without it.
- Huh? There are dynamically-typed functional languages, such as LispLanguage. Plus, I'm sure one could write a functional language with ManifestTyping, though I'm not sure one would want to. LispLanguage is not a pure functional language.
- Um, there are typeless pure functional languages, such as the pure lambda-calculus, so the claim about the necessity of TypeInference is obviously false.
There are three axes here: static-dynamic, strong-weak and nominative-structural. You can choose to look at each as boolean (either types can be changed or they can't) or a continuum. When considering whether a language has any of these attributes, it may be most productive to consider not just what is possible in a language, but what is encouraged.
Other type terms that need simple definitions:
CategoryLanguageTyping
Types Of Typing