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 cubicaltt type checker from Mörtberg et all. You may want to try this in Agda, Idris, Coq, or any other MLTT prover.

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.

$\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

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.

Inductive Data Types

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