- authors: Luca Cardelli
- year: 1996
- url: https://dl.acm.org/doi/pdf/10.1145/234313.234418
- publisher: Association for Computing Machinery (ACM)
- 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→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. 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 not(3). Good behavior: Same as being well behaved.