Dependently Typed Folds for Nested Data Types

Introduction

refl : (a : A) → a = a cong : (m, n : A) → (f : A → B) → (m = n) → (f(m) = f(n))

data Bush (A : 𝒰) : 𝒰 where nil_B : Bush(A) cons_B : A → Bush(Bush(A)) → Bush(A)

hmap_B : (A → B) → Bush(A) → Bush(B) hmap_B(f)(nil_B) ≡ nil_B hmap_B(f)(cons_B(x)(xs)) ≡ cons_B(f(x))(hmap_B(hmap_B(f))(xs))

hfold_B : ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (❴B : 𝒰❵ → P(B)) → (❴B : 𝒰❵ → B → P(P(B)) → P(B)) → Bush(A) → P(A) hfold_B(base)(step)(nil_B) ≡ base hfold_B(base)(step)(cons_B(x)(xs)) ≡ step(x)(hfold_B(base)(step)(hmap_B(hfold_B(base)(step))(xs)))

Contributions of the Paper

A Development of Dependently Typed Folds in a Total Type Theory via the Bush Data Type

\begin{matrix} NTimes : (𝒰 → 𝒰) → ℕ → 𝒰 → 𝒰 \\ NTimes(P)(0)(s) ≡ s \\ NTimes(P)(S(n))(s) ≡ P(NTimes(P)(n)(s)) \\ NBush : ℕ → 𝒰 → 𝒰 \\ NBush ≡ NTimes(Bush) \end{matrix}

\begin{matrix} map_B : (n : ℕ) → (A → B) → NBush(n)(A) → NBush(n)(B) \\ map_B(0)(f)(x) ≡ f(x) \\ map_B(S(n))(f)(nil_B) ≡ nil_B \\ map_B(S(n))(f)(cons_B(x)(xs)) ≡ cons_B(map_B(n)(f)(x))(map_B(S(S(n)))(f)(xs)) \end{matrix}

\begin{matrix} fold_B : ❴A : 𝒰❵ → ❴P : ℕ → 𝒰❵ → (A → P(0)) → ((n : ℕ) → P(S(n))) → ((n : ℕ) → P(n) → P(S(S(n))) → P(S(n))) → (n : ℕ) → NBush(n)(A) → P(n) \\ fold_B(base)(nil)(cons)(0)(x) ≡ base(x) \\ fold_B(base)(nil)(cons)(S(n))(nil_B) ≡ nil(n) \\ fold_B(base)(nil)(cons)(S(n))(cons_B(x)(xs)) ≡ cons(n)(fold_B(base)(nil)(cons)(n)(x))(fold_B(base)(nil)(cons)(S(S(n)))(xs)) \end{matrix}

\begin{matrix} map_B : (n : ℕ) → (A → B) → NBush(n)(A) → NBush(n)(B) \\ map_B❴A❵❴B❵(n)(f)(l) ≡ fold_B❴A❵❴λ(n).NBush(n)(B)❵(f)(λ(n).nil_B)(λ(n).cons_B)(n)(l) \end{matrix}

\begin{matrix} sum_B: Bush ℕ → ℕ \\ sum_B ≡ fold_B❴ℕ❵ ❴λ(n) → ℕ❵ (λ(x).x)(λ(_).0)(λ(n) → add)(S(0)) \end{matrix}

length_B : ❴A : 𝒰❵ → Bush(A) → ℕ length_B❴A❵ ≡ fold_B❴A❵❴λ(n).ℕ❵(λ(_).0)(λ(_).0)(λ(n)(r1)(r2) → S(r2))(S(0))

hfold_B : ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (❴B : 𝒰❵ → P(B)) → (❴B : 𝒰❵ → B → P(P(B)) → P(B)) → Bush(A) → P(A) hfold_B❴A❵ ❴P❵ (base)(step) ≡ fold_B❴A❵❴λ(n).NTimes(P)(n)(A)❵ (λ(x).x)(λ(_).base)(λ(_).step)(S(0))

\begin{matrix} ind_B : ❴A : 𝒰❵ → ❴P : (n : ℕ) → NBush(n)(A) → 𝒰❵ → ((x : A) → P(0)(x)) → ((n : ℕ) → P(S(n))(nil_B)) → ((n : ℕ) → ❴x : NBush(n)(A)❵ → ❴xs : NBush (S(S(n))) A❵ → P(n)(x) → P(S(S(n)))(xs) → P(S(n))(cons_B(x)(xs))) → (n : ℕ) → (xs : NBush(n)(A)) → P(n)(xs) \\ ind_B(base)(nil)(cons)(0)(xs) ≡ base(xs) \\ ind_B(base)(nil)(cons)(S(n))(nil_B) ≡ nil(n) \\ ind_B(base)(nil)(cons)(S(n))(cons_B(x)(xs)) = cons(n)(ind_B(base)(nil)(cons)(n)(x))(ind_B(base)(nil)(cons)(S(S(n)))(xs)) \end{matrix}

identity : ❴A : 𝒰❵ → (n : ℕ) → (y : NBush(n)(A)) → y = map_B(n)(λ(x).x)(y) identity ❴A❵(n)(y) ≡ ind_B❴A❵❴λ(n) v → v = map_B(n)(λ(x).x)(v)❵ (λ(x).refl)(λ(n).refl) (λ(n) ❴x❵❴xs❵(ih1)(ih2) → cong2 cons_B(ih1)(ih2))(n)(y)

mapCompose : ❴A B c : 𝒰❵ → (n : ℕ) → (f : B → c) → (g : A → B) → (x : NBush(n)(A)) → map_B(n)(compose(f)(g))(x) = map_B(n)(f)(map_B(n)(g)(x)) mapCompose❴A❵❴B❵ ❴c❵(n)(f)(g)(x) ≡ ind_B❴A❵❴λ(n).v.map_B(n)(compose(f)(g))(v) = map_B(n)(f)(map_B(n)(g)(v))❵ (λv.refl)(λ(n).refl)(λ(n)❴x1❵❴xs❵(ih1)(ih2) → cong2 cons_B(ih1)(ih2))(n)(x)

cong2 : ❴A B c : 𝒰❵ → ❴m1 n1 : A❵ → ❴m2 n2 : B❵ → (f : A → B → c) → (m1 = n1) → (m2 = n2) → f(m1)(m2) = f(n1)(n2)

((x : A) → x = map_B(0)(λ(x).x)(x)) → ((n : ℕ) → nil_B = map_B(S(n))(λ(x).x)(nil_B)) → ((n : ℕ) → ❴x : NBush(n)(A)❵ → ❴xs : NBush(S(S(n)))(A)❵ → x = map_B(n)(λ(x).x)(x) → xs = map_B(S(S(n)))(λ(x).x)(xs) → cons_B(x)(xs) = map_B(S(n))(λ(x).x)(cons_B(x)(xs))) → (n : ℕ) → (xs : NBush(n)(A)) → xs = map_B(n)(λ(x).x)(xs)

mapNilB : forall ❴A B : 𝒰❵ → (f : A → B) → map_B(S(0))(f)(nil_B) = nil_B mapNilB❴A❵❴B❵(f) ≡ refl

mapConsB : (f : A → B) → (x : A) → (xs : Bush(Bush(A))) → map_B(S(0))(f)(cons_B(x)(xs)) = cons_B(f(x))(map_B(S(0))(map_B(S(0))(f))(xs)) mapConsB❴A❵❴B❵(f)(x)(xs) ≡ cong (cons_B(f(x)))(addMap❴A❵❴B❵(S(0))(f)(xs))

addMap : (n : ℕ) → (f : A → B) → (x : NBush(add(n)(n))(A)) → map_B(add(n)(n))(f)(x) = map_B(n)(map_B(n)(f))(x) addMap❴A❵❴B❵(n)(f)(x) ≡ ind_B❴NBush(n)(A)❵❴λ(m) v  map_B(add(m)(n))(f)(v) = map_B(m)(map_B(n)(f))(v)❵(λ(_).refl)(λ(_).refl) (λ(n)❴x❵❴xs❵(ih1)(ih2).cong2(cons_B)(ih1)(ih2))(n)(x)

foldBNilB : ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (base : ❴B : 𝒰❵ → P(B)) → (step : ❴B : 𝒰❵ → B → P(P(B)) → P(B)) → hfold_B❴A❵❴P❵(base)(step)(nil_B) = base foldBNilB(base)(step) ≡ refl

foldBConsB : ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (base : ❴B : 𝒰❵ → P(B)) → (step : ❴B : 𝒰❵ → B → P(P(B)) → P(B)) → (x : A) → (xs : Bush(Bush(A))) → hfold_B(base)(step)(cons_B(x)(xs)) = step(x)(hfold_B(base)(step)(map_B(S(0))(hfold_B(base)(step))(xs))) foldBConsB❴A❵❴P❵(base)(step)(x)(xs) ≡ cong(step(x))(lemmConsB❴A❵❴P❵(S(0))(base)(step)(xs))

uniqueness : (f : ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (❴B : 𝒰❵ → P(B)) → (❴B : 𝒰❵ → B → P(P(B)) → P(B)) → Bush(A) → P(A)) → (hp1 : ❴A : 𝒰❵ ❴P : 𝒰 → 𝒰❵ → (base : ❴B : 𝒰❵ → P(B)) → (step : ❴B : 𝒰❵ → B → P(P(B)) → P(B)) → f❴A❵❴P❵(base)(step)(nil_B) = base) → (hp2 : ❴A : 𝒰❵ ❴P : 𝒰 → 𝒰❵ → (base : ❴B : 𝒰❵ → P(B)) → (step : ❴B : 𝒰❵ → B → P(P(B)) → P(B)) → (x : A) → (xs : Bush (Bush(A))) → f (base)(step)(cons_B(x)(xs)) = step(x)(f(base)(step)(map_B(S(0))(f(base)(step))(xs)))) → ❴A : 𝒰❵ → ❴P : 𝒰 → 𝒰❵ → (base : ❴B : 𝒰❵ → P(B)) → (step : ❴B : 𝒰❵ → B → P(P(B)) → P(B)) → (bush : Bush(A)) → f❴A❵❴P❵(base)(step)(bush) = hfold_B❴A❵❴P❵(base)(step)(bush) uniqueness(f)(hp1)(hp2)❴A❵❴P❵(base)(step)(bush) ≡ ind_B❴A❵❴λ(n)(v). lift(n)(f (base)(step))(v) = lift(n)(hfold_B(base)(step))(v)❵

lift : ❴A : 𝒰❵ ❴P : 𝒰 → 𝒰❵ (n : ℕ) → (g : ❴A : 𝒰❵ → Bush(A) → P(A)) → NBush(n)(A) → NTimes(P)(n)(A) lift❴A❵❴P❵(0)(g)(x) ≡ x lift❴A❵❴P❵(S(n))(g)(x) ≡ g(map_B(S(0))(lift❴A❵❴P❵(n)(g))(x))

The Indexed Representations

data BushN : ℕ → 𝒰 → 𝒰 where base : ❴A : 𝒰❵ → A → BushN(0)(A) nil_BN : ❴A : 𝒰❵ → ❴n : ℕ❵ → BushN((S(n)))(A) cons_BN : ❴A : 𝒰❵ → ❴n : ℕ❵ → BushN(n)(A) → BushN((S(S(n))))(A) → BushN((S(n)))(A)

fold_BN : ❴A : 𝒰❵ → ❴P : ℕ → 𝒰❵ → (A → P(0)) → ((n : ℕ) → P(S(n))) → ((n : ℕ) → P(n) → P(S(S(n))) → P(S(n))) → (n : ℕ) → BushN(n)(A) → P(n) fold_BN(base)(nil)(cons)(0)(base(x)) ≡ base(x) fold_BN(base)(nil)(cons)(S(n))(nil_BN) ≡ nil(n) fold_BN(base)(nil)(cons)(S(n))(cons_BN(x)(xs)) ≡ cons(n)(fold_BN(base)(nil)(cons)(n)(x))(fold_BN(base)(nil)(cons)(S(S(n)))(xs))

ind_BN : ❴A : 𝒰❵ → ❴P : (n : ℕ) → BushN(n)(A) → 𝒰❵ → ((x : A) → P(0)(base(x))) → ((n : ℕ) → P(S(n))(nil_BN)) → ((n : ℕ) → ❴x : BushN(n)(A)❵ → ❴xs : BushN((S(S(n))))(A)❵ → P(n)(x) → P(S(S(n)))(xs) → P(S(n))(cons_BN(x)(xs))) → (n : ℕ) → (xs : BushN(n)(A)) → P(n)(xs)

to : ❴A : 𝒰❵ → (n : ℕ) → NBush(n)(A) → BushN(n)(A) to❴A❵(n)(s) ≡ fold_B❴A❵❴λ(n) → BushN(n)(A)❵ (base)(λ(_).nil_BN)(λ(_).cons_BN)(n)(s)

from : ❴A : 𝒰❵ → (n : ℕ) → BushN(n)(A) → NBush(n)(A) from❴A❵(n)(s) ≡ fold_BN❴A❵❴λ(n) → NBush(n)(A)❵(λ(x).x)(λ(n) → nil_B)(λ(n) → cons_B)(n)(s)

The Church Encodings of the Indexed Representations

\begin{array}{l} CNBush : ℕ → 𝒰 → 𝒰 \\ CNBush(n)(A) ≡ ❴P : ℕ → 𝒰❵ → (A → P(0)) → ((n : ℕ) → P(S(n))) → ((n : ℕ) → P(n) → P(S(S(n))) → P(S(n))) → P(n) \end{array}

\begin{array}{l} cbase : ❴A : 𝒰❵ → A → CNBush(0)(A) \\ cbase(x) ≡ λ(base).nil.cons.base(x) \end{array}

\begin{array}{l} cnil : ❴A : 𝒰❵ → (n : ℕ) → CNBush (S(n)) A \\ cnil(n) ≡ λ(base) nil cons → nil(n) \end{array}

\begin{array}{l} ccons : ❴A : 𝒰❵ → (n : ℕ) → CNBush(n)(A) → CNBush(S(S(n)))(A) → CNBush(S(n))(A) \\ ccons(n)(x)(xs) ≡ λ(base) nil cons → cons(n)(x (base)(nil)(cons))(xs (base)(nil)(cons)) \end{array}

\begin{array}{l} cfold_B : ❴A : 𝒰❵ → ❴P : ℕ → 𝒰❵ → (A → P(0)) → ((n : ℕ) → P(S(n))) → ((n : ℕ) → P(n) → P(S(S(n))) → P(S(n))) → (n : ℕ) → CNBush(n)(A) → P(n) \\ cfold_B(base)(nil)(cons)(n)(b) ≡ b(base)(nil)(cons) \end{array}

\begin{array}{l} cmap_B : (n : ℕ) → (A → B) → CNBush(n)(A) → CNBush(n)(B) \\ cmap_B❴A❵❴B❵(n)(f) ≡ cfold_B❴A❵❴λ(n).CNBush(n)(B)❵(λ(x).cbase(f(x)))(cnil)(ccons)(n) \end{array}

Dependently Typed Folds for Nested Data Types

Introduction

Contributions of the Paper

A Development of Dependently Typed Folds in a Total Type Theory via the Bush Data Type

The Indexed Representations

The Church Encodings of the Indexed Representations

Case Study I: De Bruijn Notation As the Nested Data Type Term

Dependently typed folds for Incr and Term

Programming with dependently typed folds and maps

Reasoning with the induction principles indI and indT

Case Study II: De Bruijn Notation As the Nested Data Type Terme

The dependently typed fold foldE

Programming with foldE

Reasoning with the induction principle indE

Discussion

Obtaining the Dependently Typed Folds for Any Nested Data Types

A Method To Obtain Dependently Typed Folds

Specializing Dependently Typed Folds to Higher-Order Folds

Discussion

Related Work

Conclusion and Future Work