information:filtering
Dependent products and sums

Two common type dependencies, dependent product and dependent sum types, allow for the theory to encode BHK intuitionistic logic by acting as equivalents to universal and existential quantification; this is formalized by Curry–Howard Correspondence. As they also connect to products and sums in set theory, they are often written with the symbols Π {\displaystyle \Pi } and Σ {\displaystyle \Sigma }, respectively. Dependent product and sum types commonly appear in function types and are frequently incorporated in programming languages.

For example, consider a function a p p e n d {\displaystyle \mathrm {append} }, which takes in a l i s t a {\displaystyle {\mathsf {list}}\,a} and a term of type a {\displaystyle a}, and returns the list with the element at the end. The type annotation of such a function would be a p p e n d: (Π a. l i s t a → a → l i s t a) {\displaystyle \mathrm {append} :(\Pi \,a.{\mathsf {list}}\,a\to a\to {\mathsf {list}}\,a)}, which can be read as "for any type a {\displaystyle a}, pass in a l i s t a {\displaystyle {\mathsf {list}}\,a} and an a {\displaystyle a}, and return a l i s t a {\displaystyle {\mathsf {list}}\,a} ".

Sum types are seen in dependent pairs, where the second type depends on the value of the first term. This arises naturally in computer science where functions may return different types of outputs based on the input. For example, the Boolean type is usually defined with an eliminator function i f {\displaystyle \mathrm {if} }, which takes three arguments and behaves as follows.

The return type of this function depends on its b o o l {\displaystyle {\mathsf {bool}}} input. If the type theory allows for dependent types, then it is possible to define a function T F: b o o l → U → U → U {\displaystyle \mathrm {TF} \colon {\mathsf {bool}}\to U\to U\to U} such that

The type of i f {\displaystyle \mathrm {if} } may then be written as (Π σ τ. b o o l → σ → τ → (Σ x: bool. T F x σ τ)) {\displaystyle (\Pi \,\sigma \,\tau.{\mathsf {bool}}\to \sigma \to \tau \to (\Sigma \,x:{\textsf {bool}}.\mathrm {TF} \,x\,\sigma \,\tau))}.