Inductive Type

Contents

Definition

F(ΞΌX.F)β†’ΞΌX.F(X)F(X)β†’X⊒μX.F(X)β†’X

[bahareh-afshari-2019]

F:Uβ†’U,(A,B:U)β†’(Aβ†’B)β†’F(A)β†’F(B).(X:U)β†’(F(X)β†’X)β†’ΞΌFβ†’X.𝟎,F(𝟎),F(F(𝟎)),…(X:U)β†’(Xβ†’F(X))β†’Xβ†’Ξ½F.𝟏,F(𝟏),F(F(𝟏)),…

Induction Principle

(F(X)→X)→μF→X.

Coinduction Principle

(X→F(X))→X→νF.

[xavier-leroy-2019]

πŸβ‰‘Ξ½X.X.πŸŽβ‰‘ΞΌX.X.

[bahareh-afshari-2019]

Inductive Types

Church Data Type (iterative), in Ξ»2

A≑λX.(F(X)β†’X)β†’X

Scott Data Type (case), in Ξ»2ΞΌ

A≑λX.(F(A)β†’X)β†’X

Church-Scott Data Type (primitive recursive), in Ξ»2ΞΌ

A≑λX.(F(AΓ—X)β†’X)

Coinductive Types

[herman-geuvers-2015]

ΞΌ

𝟏+𝟏

𝟐, boolean.

[herman-geuvers-2014]

𝟏+A

Option, or maybe.

[andreas-abel-2013]

𝟏+X

β„•

ℕ≑μX. 𝟏+X.

Church-Scott

λA.A→(A→A)→A.μX.λA.A→(X→A)→A.μX.λA.A→(X→A→A)→A.

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

𝟏+(AΓ—X)

List.

[thorsten-altenkirch-2004]

Church-Scott

λA.A→(X→A→A)→A

[herman-geuvers-2014]

𝟏+(AΓ—XΓ—X)

Binary tree.

[thorsten-altenkirch-2004]

Church-Scott

λX.(A→X)→(B→X→X→X)→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

βˆƒX.XΓ—(Xβ†’AΓ—X)

Ξ»2ΞΌ

ΞΌY.βˆƒX.XΓ—(Xβ†’AΓ—(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)≑(a:A)Γ—B(a)β†’X.List(A)β‰…(n:β„•)Γ—Fin(n)β†’A.

[simon-hudon-2019]

Quotients of Polynomial Functors

  1. abs:P(A)β†’F(A), (abstraction)
  2. repr:F(A)β†’P(A)
  3. (x:F(A))β†’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]

References