polarity in type theory


In type theory, a type may be classed as having a polarity, either positive or negative, according to whether its constructors or eliminators are regarded as primary. The idea is due to Jean-Marc Andreoli and Jean-Yves Girard.

Positive types are inductively defined by their introduction rules and correspond to colimits and other “mapping-out” universal properties; negative types are coinductively defined by their elimination rules and correspond to limits and other “mapping-in” universal properties. Some types may be defined as both positive and negative, see, for instance, product type.

Generally, in effectful languages, the positive types are better behaved in call-by-value? evaluation strategies and negative types are better behaved in call-by-name? and other lazy evaluation? strategies. A category-theoretic explanation of this fact is that call-by-value? languages can be modeled by the Kleisli category of a monad TT on a category CC. Usually, the category CC will have both limits (negatives) and colimits (positives), however the canonical functor F:CC TF : C \to C_T is a left adjoint so it only generally preserves the colimits (positives). Dually, call-by-name languages can be modeled by the Kleisli category of a comonad WW and the canonical functor U:CC WU : C \to C_W is a right adjoint, and so preserves limits (negatives).