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 schemes require the fixpoint constructor
in the typechecker core in order to express this encoding.
We will use
Prerequisites
Fixpoint
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-Algebra
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.
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$
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 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
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))
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.