natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
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, forming two polarities.
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.
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.