Inductive Type

Definition

F (μ X . F) \to μ X . F (X)

F (X) \to X ⊢ μ X . F (X) \to X

[bahareh-afshari-2019]

\begin{array}{l} F : U \to U, \\ (A, B : U) \to (A \to B) \to F (A) \to F (B) . \end{array}

(X : U) \to (F (X) \to X) \to μ F \to X .

𝟎, F (𝟎), F (F (𝟎)), \dots

(X : U) \to (X \to F (X)) \to X \to ν F .

𝟏, F (𝟏), F (F (𝟏)), \dots

Induction Principle

(F (X) \to X) \to μ F \to X .

Coinduction Principle

(X \to F (X)) \to X \to ν F .

[xavier-leroy-2019]

𝟏 \equiv ν X . X .

𝟎 \equiv μ X . X .

[bahareh-afshari-2019]

Inductive Types

Church Data Type (iterative), in λ2

A \equiv λ X . (F (X) \to X) \to X

Scott Data Type (case), in λ2μ

A \equiv λ X . (F (A) \to X) \to X

Church-Scott Data Type (primitive recursive), in λ2μ

A \equiv λ X . (F (A \times X) \to X)

Coinductive Types

[herman-geuvers-2015]

μ

𝟏+𝟏

𝟐, boolean.

[herman-geuvers-2014]

𝟏+A

Option, or maybe.

[andreas-abel-2013]

𝟏+X

ℕ

ℕ \equiv μ X . 𝟏 + X .

Church-Scott

λ A . A \to (A \to A) \to A .

μ X . λ A . A \to (X \to A) \to A .

μ X . λ A . A \to (X \to A \to A) \to A .

[herman-geuvers-2014], [herman-geuvers-2015]

𝟏+(A×X)

List.

[thorsten-altenkirch-2004]

Church-Scott

λ A . A \to (X \to A \to A) \to A

[herman-geuvers-2014]

𝟏+(A×X×X)

Binary tree.

[thorsten-altenkirch-2004]

Church-Scott

λ X . (A \to X) \to (B \to X \to X \to X) \to X .

[herman-geuvers-2014]

A+(A×X)+(X×X)

Lambda calculus.

[yigal-duppen-2000]

𝟏+X+(ℕ→X)

Ordinals.

[thorsten-altenkirch-2004]

𝟏+(X×Y)

F tree.

[thorsten-altenkirch-2004]

ν

A×X

Stream.

[andreas-abel-2013]

Church-Scott

λ2

\exists X . X \times (X \to A \times X)

λ2μ

μ Y . \exists X . X \times (X \to A \times (X + Y))

[herman-geuvers-2014]

𝟐×(A→X)

Deterministic automata.

[alexander-kurz-2018]

A×(B→X)

W-types.

[thorsten-altenkirch-2004]

μ_.(𝟏+A×X)

Colist.

[andreas-abel-2013]

ℕ×(μX.𝟏+A×X)

Vector.

[andreas-abel-2013]

Polynomial Functors

F (X) \equiv (a : A) \times B (a) \to X .

List (A) ≅ (n : ℕ) \times Fin (n) \to A .

[simon-hudon-2019]

Quotients of Polynomial Functors

$abs : P (A) \to F (A), (abstraction)$
$repr : F (A) \to P (A)$
$(x : F (A)) \to abs (repr (x)) = x .$

The class of QPFs is closed under:

composition
quotients
initial algebras
final colagebras

In particular, finset and multiset are QPFs.

[simon-hudon-2019]

Inductive Type

Definition

Induction Principle

Coinduction Principle

Inductive Types

Coinductive Types

μ

𝟏+𝟏

𝟏+A

𝟏+X

Church-Scott

𝟏+(A×X)

Church-Scott

𝟏+(A×X×X)

Church-Scott

A+(A×X)+(X×X)

𝟏+X+(ℕ→X)

𝟏+(X×Y)

ν

A×X

Church-Scott

𝟐×(A→X)

A×(B→X)

μ_.(𝟏+A×X)

ℕ×(μX.𝟏+A×X)

Polynomial Functors

Quotients of Polynomial Functors

References