Cardelli Type Terminology

LucaCardelli's influential 1997 paper "Type Systems" (http://citeseer.ist.psu.edu/cardelli97type.html) gives definitions for a number of terms related to types, excerpted here. See also TypesOfTyping.

His approach and definitions are very reasonable for some purposes, but incomplete for others. Notably, he considers only typed variables, not typed cells, and hence calls LispLanguage an "untyped" language. This is not so much wrong, as it is unhelpful, for the Lisp side of the world; there are other approaches that are more helpful there.

Cardelli's approach on the other hand is very handy for discussing things like HaskellLanguage.

Abstract type: A data type whose nature is kept hidden, in such a way that only a predetermined collection of operations can operate on it.
Contravariant: A type that varies in the inverse direction from one of its parts with respect to subtyping. The main example is the contravariance of function types in their domain. For example, assume (A <: B) and vary X from A to B in (X -> C); we obtain (A -> C) :> (B -> C). Thus (X -> C) varies in the inverse direction of X.
Covariant: A type that varies in the same direction as one of its parts with respect to subtyping. For example, assume (A <: B) and vary X from A to B in (D -> X); we obtain ((D -> A) <: (D -> B)). Thus (D -> X) varies in the same direction as X.
Derivation: A tree of judgments obtained by applying the rules of a type system.
Dynamic checking: A collection of run time tests aimed at detecting and preventing forbidden errors.
Dynamically checked language: A language where good behavior is enforced during execution.
Explicitly typed language: A typed language where types are part of the syntax. (aka ManifestTyping)
First-order type system: One that does not include quantification over type variables.
Forbidden error: The occurrence of one of a predetermined class of execution errors; typically the improper application of an operation to a value, such as logical-not applied to 3.
Good behavior: Same as being well behaved.
Ill typed: A program fragment that does not comply with the rules of a given type system.
Implicitly typed language: A typed language where types are not part of the syntax (or are an optional part). (See ImplicitTyping)
Judgment: A formal assertion relating entities such as terms, types, and environments. Type systems prescribe how to produce valid judgments from other valid judgements.
Polymorphism: The ability of a program fragment to have multiple types (opposite of monomorphism). (Note: Not the same as interface polymorphism, where a program fragment has a single type but many implementations.)
Safe language: A language where no untrapped errors can occur.
Second-order type system: One that includes quantification over type variables, either universal or existential.
Static checking: A collection of compile time tests, mostly consisting of typechecking. (Orthogonal to explicit/implicit typing.)
Statically checked language: A language where good behavior is determined before execution.
Strongly checked language: A language where no forbidden errors can occur at runtime (depending on the definition of forbidden error). Generally achieved in statically checked languages by compile-time typing error. Generally achieved in dynamically checked languages by graceful abortion of the operation (e.g. throwing an exception).
Subsumption: A fundamental rule of subtyping, asserting that if a term has a type A, and (A <: B) (the subtype relationship), then the term can be passed to functions that take parameters of type B.
Subtyping: A reflexive and transitive binary relation over types that satisfies subsumption; it asserts the inclusion of collections of values. The subtype relationship is traditionally indicated with the operator '<:'.
Trapped error: An execution error that immediately results in a fault.
Type: A collection of values. An estimate of the collection of values that a program fragment can assume during program execution.
Type inference: The process of finding a type for a program within a given type system.
Type reconstruction: The process of finding a type for a program where type information has been omitted, within a given type system.
Type rule: A component of a type system. A rule stating the conditions under which a particular program construct will not cause forbidden errors.
Type safety: The property stating that programs do not cause untrapped errors.
Type soundness: The property stating that programs do not cause forbidden errors.
Type system: A collection of type rules for a typed programming language. Same as static type system.
Typechecker: The part of a compiler or interpreter that performs typechecking.
Typechecking: The process of checking a program before execution to establish its compliance with a given type system and therefore to prevent the occurrence of forbidden errors. (Dynamic typechecking will be performed upon program fragments immediately prior to their execution.)
Untyped language: A language that does not have a (static) type system, or whose type system has a single type that contains all values.
Typed language: A language with an associated (static) type system possessing at least two types, whether or not types are part of the syntax, and whether or not those types are statically checked.
Typing error: An error reported by a typechecker to warn against possible execution errors.
Untrapped error: An execution error that does not immediately result in a fault.
Valid judgment: A judgment obtained from a derivation in a given type system.
Weakly checked language: A language that is statically checked but provides no clear guarantee of absence of execution errors.
Well behaved: A program fragment that will not produce forbidden errors at run time.
Well formed: Properly constructed according to formal rules.
Well-typed program: A program (fragment) that complies with the rules of a given type system.