(Co)-Inductive Data Types

Well-founded Trees and Corecursion in Martin-Löf Type Theory with Fixpoint

Article

Abstract

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

Fixpoint

The core fixpoint reflection type is parametrized by functor and has only one contructor with 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 valued 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-Algebra

F-Algebras gives us a categorical understanding 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 an 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. Similar a F-coalgebra $(\nu F, out)$ is the terminal F-coalgebra if for any F-coalgebra $(C, \phi)$ there exists 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

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))

Inductive

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

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))

Coinductive

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

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 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)))

Hylomorphism

Hylomorphism is a bi-functor that could be taken as axiom, as 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))

Prelude

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

Paramorphism

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))

Apomorphism

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))

Gapomorphism

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

Histomorphism

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

Futumorphism

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

Chronomorphism

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)

Appendix

Metamorphism

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))

Mutumorphism

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))

Zygomorphism

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)

Prepromorphism

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))

Postpromorphism

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.