negative type in nLab

Negative types

Negative types

Idea

In type theory, a negative type is one whose eliminators are regarded as primary. Its constructors are derived from these by the rule that “to construct an element of a negative type, it is necessary and sufficient to specify how that element behaves upon applying all of the eliminators to it”.

The opposite notion is that of a positive type, forming two polarities of type theory.

In categorical semantics of type theory, negative types correspond to “from the right” universal properties (i.e. for mapping in).

In denotational semantics, negative types behave well with respect to “call-by-name?” and other lazy evaluation? strategies.

Examples

• dependent product type

  • function type

• coinductive type

• record type

• unit types, dependent sum types and cartesian product types can be presented both positively and negatively. The two definitions are equivalent in ordinary type theory, but distinct in linear logic. The same is true of binary sum types if we allow sequents with multiple conclusions.