Positive types

Idea

In type theory, a positive type is one whose constructors are regarded as primary. Its eliminators are derived from these by the rule that “to use an element of a positive type, it is necessary and sufficient to specify what should be done for all possible ways that element could have been constructed”.

The opposite notion is a negative type.

In categorical semantics of type theory, positive types correspond to “from the left” universal properties (i.e. for mapping out).

In denotational semantics, positive types behave well with respect to “call-by-value” and other eager evaluation? strategies.

Examples

• inductive type

• cartesian product types can be presented both positively (as a particular inductive type) and negatively. The two definitions are equivalent in ordinary type theory, but distinct in linear logic. The same is true for binary sum types if we allow sequents with multiple conclusions.

Revised on May 29, 2012 22:04:00 by Andrew Stacey (129.241.15.200)