Inductive Data Types

Well-founded trees and corecursion
in Martin-Löf Type Theory with fixpoint


This work shows how to encode inductive types using recursion schemes. Unlike Church-Boem-Berarducci encoding that can encode inductive types without fixpoint, recursion schemes require the fixpoint constructor in the typechecker core in order to express this encoding. We will use cubicaltt type checker from Mörtberg et all. You may want to try this in Agda, Idris, Coq, or any other MLTT prover.



The core fixpoint reflection type is parametrized by a functor and has only one contructor with the value of this functor applied to fixpoint itself.

data fix (F: U -> U) = Fix (point: F (fix F))

We also need functions for projecting and embedding values to/from fixpoint functiorial stream.

unfix (F: U -> U): fix F -> F (fix F) = split Fix f -> f embed (F: U -> U): F (fix F) -> fix F = \(x: F (fix F)) -> Fix x


F-Algebras give us a categorical understanding of recursive types. Let $F : C \rightarrow C$ be an endofunctor on category $C$. An F-algebra is a pair $(A, \varphi)$, where A is an object and $\varphi\ : F\ A \rightarrow A$ is a morphism in the category $C$. The object A is the carrier and the functor F is the signature of the algebra. Reversing arrows gives us F-coalgebra.

$\require{AMScd}$ \begin{CD} F C @>\varphi>> C\\ @V F f V V\ =\ @VV f V\\ F D @>>\psi> D \end{CD} $f \circ \varphi = \psi \circ F f$
$\require{AMScd}$ \begin{CD} C @>\phi>> F C\\ @V f V V\ =\ @VV F f V\\ D @>>\psi^*> F D \end{CD} $\psi^* \circ f = F f \circ \phi$

Initial Algebra

A F-algebra $(\mu F, in)$ is the initial F-algebra if for any F-algebra $(C, \varphi)$ there exists a unique arrow $\llparenthesis \varphi \rrparenthesis : \mu F \rightarrow C$ where $f = \llparenthesis \varphi \rrparenthesis$ and is called catamorphism. Similarly, a F-coalgebra $(\nu F, out)$ is the terminal F-coalgebra if for any F-coalgebra $(C, \phi)$ there exists a unique arrow $\llbracket \phi \rrbracket : C \rightarrow \nu F$ where $f = \llbracket \phi \rrbracket$

$\require{AMScd}$ \begin{CD} F \mu F @>in>> \mu F\\ @V fmap\ =\ F \llparenthesis \varphi \rrparenthesis V V\ =\ @VV \llparenthesis \varphi \rrparenthesis\ =\ cata V\\ F C @>>\varphi> C \end{CD} $f \circ in = \varphi \circ F f == f = \llparenthesis \varphi \rrparenthesis$
$\require{AMScd}$ \begin{CD} C @>\phi>> F C\\ @V ana\ =\ \llbracket \phi \rrbracket V V\ =\ @VV fmap\ =\ F \llbracket \phi \rrbracket V\\ \nu F @>>out> F \nu F \end{CD} $out \circ f = F f \circ \phi == f = \llbracket \phi \rrbracket$

Example of Initial Algebra

The data type of $List$ over a given set $A$ can be represented as the initial algebra $\mu\ L_A in$ of the functor $L_A(X) = 1 + (A \times X)$. Denote $\mu\ L_A = List (A)$. The constructor functions $nil: 1 \rightarrow List (A)$ and $cons: A \times List(A) \rightarrow List(A)$ are defined by $nil = in \circ inl$ and $cons = in \circ inr$, so $in = [nil,cons]$.


Catamorphism is known as generalized version of fold. Assume we have fmap defined somewhere else. It is used to construct instances of inductive datatypes.

fmap (A B: U) (F: U -> U): (A -> B) -> F A -> F B = undefined

Then cata is defined as follows:

cata (A: U) (F: U -> U) (alg: F A -> A) (f: fix F): A = alg (fmap (fix F) A F (cata A F alg) (unfix F f))


Let's rewrite fix data type as an interface structure along with its fold:

ind (F: U -> U) (A: U): U = (in_: F (fix F) -> fix F) * (in_rev: fix F -> F (fix F)) * (fold_: (F A -> A) -> fix F -> A) * Unit

Then instance of this type class would be:

inductive (F: U -> U) (A: U): ind F A = (embed F,unfix F,cata A F,tt)


Anamorphism is used to build instances of coinductive data types and represents generic stream unfold.

ana (A: U) (F: U -> U) (coalg: A -> F A) (a: A): fix F = Fix (fmap A (fix F) F (ana A F coalg) (coalg a))


All arrows are reversed, in is out, fold is unfold.

coind (F: U -> U) (A: U): U = (out_: F (fix F) -> fix F) * (out_rev: fix F -> F (fix F)) * (unfold_: (F A -> A) -> fix F -> A) * Unit

Then instance of this type class would be:

coinductive (F: U -> U) (A: U) : coind A F = (unfix F,embed F,ana A F,tt)

Inductive List Nat

Here is an example of inductive encoding of list nat:

> inductive list
EVAL: (\(A : U) -> (embed F,(unfix F,(cata A F,tt)))) (F = (\(A : U) -> list))
> inductive list nat
EVAL: ((\(x : F (fix F)) -> Fix x) (F = (\(A : U) -> list)),
(unfix (\(A : U) -> list),((\(alg : Pi \(_ : F A) -> A) ->
\(f : fix F) -> alg (fmap (fix F) A F (cata A F alg)
(unfix F f))) (A = nat, F = (\(A : U) -> list)),tt)))

Coinductive Stream Nat

Here is example of coinductive encoding of stream nat:

> coinductive stream nat
EVAL: (unfix (\(A : U) -> stream),((\(x : F (fix F))
-> Fix x) (F = (\(A : U) -> stream)),((\(coalg : Pi
\(_ : A) -> F A) -> \(a : A) -> Fix (fmap A (fix F)
F (ana A F coalg) (coalg a))) (A = nat, F = (\(A :
U) -> stream)),tt)))

Recursion Schemes


Hylomorphism is a bi-functor that could be taken as axiom, since all other recursion schemas are derivable from it. More common, (Co)-Inductive types could be represented as di-algebras.

hylo (A B: U) (F: U -> U) (alg: F B -> B) (coalg: A -> F A) (a: A): B = alg (fmap A B F (hylo A B F alg coalg) (coalg a))


First we need to set up an inductive type tuple for para and either type for apomorphism.

data tuple (A B: U) = pair (a: A) (b: B) data either (A B: U) = left (a: A) | right (b: B) either_ (A B C: U): (A -> C) -> (B -> C) -> (either A B) -> C = \(b: A -> C) -> \(c: B -> C) -> [email protected](either A B -> C) with left x -> b x right y -> c y fst (A B: U): tuple A B -> A = split pair a b -> a snd (A B: U): tuple A B -> B = split pair a b -> b

Primitive Recursion


para (A: U) (F: U -> U) (psi: F (tuple (fix F) A) -> A) (f: fix F): A = psi (fmap (fix F) (tuple (fix F) A) F (\(m: fix F) -> pair m (para A F psi m)) (unfix F f))


apo (A: U) (F: U -> U) (coalg: A -> F(either (fix F) A)) (a: A): fix F = Fix(fmap (either (fix F) A) (fix F) F (\(x: either (fix F) A) -> either_ (fix F) A (fix F) (idfun (fix F)) (apo A F coalg) x) (coalg a))


gapo (A B: U) (F: U -> U) (coalg: A -> F A) (coalg2: B -> F(either A B)) (b: B): fix F = Fix((fmap (either A B) (fix F) F (\(x: either A B) -> either_ A B (fix F) (\(y: A) -> ana A F coalg y) (\(z: B) -> gapo A B F coalg coalg2 z) x) (coalg2 b)))

Morphisms on (Co)-Initial Objects

data freeF (F: U -> U) (A B: U) = ReturnF (a: A) | BindF (f: F B) data cofreeF (F: U -> U) (A B: U) = CoBindF (a: A) (f: F B) data free (F: U -> U) (A: U) = Free (_: fix (freeF F A)) data cofree (F: U -> U) (A: U) = CoFree (_: fix (cofreeF F A)) unfree (A: U) (F: U -> U): free F A -> fix (freeF F A) = split Free a -> a uncofree (A: U) (F: U -> U): cofree F A -> fix (cofreeF F A) = split CoFree a -> a


histo (A:U) (F: U->U) (f: F (cofree F A) -> A) (z: fix F): A = extract A F ((cata (cofree F A) F (\(x: F (cofree F A)) -> CoFree (Fix (CoBindF (f x) ((fmap (cofree F A) (fix (cofreeF F A)) F (uncofree A F) x)))))) z) where extract (A: U) (F: U -> U): cofree F A -> A = split CoFree f -> unpack_fix f where unpack_fix: fix (cofreeF F A) -> A = split Fix f -> unpack_cofree f where unpack_cofree: cofreeF F A (fix (cofreeF F A)) -> A = split CoBindF a -> a


futu (A: U) (F: U -> U) (f: A -> F (free F A)) (a: A): fix F = Fix (fmap (free F A) (fix F) F (\(z: free F A) -> w z) (f a)) where w: free F A -> fix F = split Free x -> unpack x where unpack_free: freeF F A (fix (freeF F A)) -> fix F = split ReturnF x -> futu A F f x BindF g -> Fix (fmap (fix (freeF F A)) (fix F) F (\(x: fix (freeF F A)) -> w (Free x)) g) unpack: fix (freeF F A) -> fix F = split Fix x -> unpack_free x


chrono (A B: U) (F: U -> U) (f: F (cofree F B) -> B) (g: A -> F (free F A)) (a: A): B = histo B F f (futu A F g a)



meta (A B: U) (F: U -> U) (f: A -> F A) (e: B -> A) (g: F B -> B) (t: fix F): fix F = ana A F f (e (cata B F g t))


mutu (A B: U) (F: U -> U) (f: F (tuple A B) -> B) (g: F (tuple B A) -> A) (t: fix F): A = g (fmap (fix F) (tuple B A) F (\(x: fix F) -> pair (mutu B A F g f x) (mutu A B F f g x)) (unfix F t))


zygo (A B: U) (F: U -> U) (g: F A -> A) (alg: F (tuple A B) -> B) (f: fix F): B = snd A B (cata (tuple A B) F (\(x: F (tuple A B)) -> pair (g(fmap (tuple A B) A F (\(y: tuple A B) -> fst A B y) x)) (alg x)) f)


prepro (A: U) (F: U -> U) (nt: F(fix F) -> F(fix F)) (alg: F A -> A) (f: fix F): A = alg (fmap (fix F) A F (\(x: fix F) -> prepro A F nt alg (cata (fix F) F (\(y: F(fix F)) -> Fix (nt(y))) x)) (unfix F f))


postpro (A: U) (F: U -> U) (nt : F(fix F) -> F(fix F)) (coalg: A -> F A) (a: A): fix F = Fix(fmap A (fix F) F (\(x: A) -> ana (fix F) F (\(y: fix F) -> nt(unfix F y)) (postpro A F nt coalg x)) (coalg a))

The code is here.