We can perhaps relax our constraints: we do not necessarily need to Church-encode everything. What we want is to write code without recursion, where we are only allowed to use a given catamorphism for a given data type. The entire recursive and iterative functionality is encapsulated in the given catamorphism.
So, let us formulate the question like this:
We are given a type constructor `C`. We imagine that `C a` is a data structure containing some values of type `a`.
We know very little about `C` other than:
- We have a given bifunctor F. So, we have bimap: (a → p) → (b → q) → F a b → F p q
- We know that the type `C a` is isomorphic to the type `F a (C a)`. The isomorphism is witnessed by two functions:
fix: F a (C a) → C a
unfix: C a → F a (C a)
These functions are considered to be known.
- We have the catamorphism function:
cata: C a → ∀ r. (F a r → r) → r
- We have the Church encoding constructor:
church: (∀ r. (F a r → r) → r) → C a
These functions will satisfy a number of laws, but it's less important. For example: fix . unfix == id; unfix . fix == id; cata ca fix == ca; cata . church == id; church . cata == id; and so on.
And that's it. Now we want to implement various things though these functions. We are allowed to use any features of the (purely functional) language: product types, co-product types, functions, universal type quantifiers, whatever - but no recursion.
To implement some function for C a, we usually need to have a corresponding function for F a r. For example, we can implement fmap:
fmap: (a → b) → C a → C b
but only if we have bimap for F.
We can implement depth:
depth: C a → Int -- count the maximum recursion depth of a value.
but only if we have a "traverse" for F that works like this:
traverse: Applicative h => (r → h s) → F a r → h (F a s)
Using `depth`, we can transform any `C a` into a Church-encoded `Nat`, counting the maximum recursion depth. Then we can implement your `recursion-safe hylo` from this post.
So the "Church encoding approach" consists of asking: what functions can be implemented without recursion, if we are allowed to use catamorphisms and the properties of F.
Typically, F will be a simple, non-recursive polynomial bifunctor, like F a r = Maybe (a, r, r) for the type of trees that you considered. So we will have properties like bimap, traverse, bitraverse, etc., easily implementable for F without recursion.
no subject
So, let us formulate the question like this:
We are given a type constructor `C`. We imagine that `C a` is a data structure containing some values of type `a`.
We know very little about `C` other than:
- We have a given bifunctor F. So, we have bimap: (a → p) → (b → q) → F a b → F p q
- We know that the type `C a` is isomorphic to the type `F a (C a)`. The isomorphism is witnessed by two functions:
fix: F a (C a) → C a
unfix: C a → F a (C a)
These functions are considered to be known.
- We have the catamorphism function:
cata: C a → ∀ r. (F a r → r) → r
- We have the Church encoding constructor:
church: (∀ r. (F a r → r) → r) → C a
These functions will satisfy a number of laws, but it's less important. For example: fix . unfix == id; unfix . fix == id; cata ca fix == ca; cata . church == id; church . cata == id; and so on.
And that's it. Now we want to implement various things though these functions. We are allowed to use any features of the (purely functional) language: product types, co-product types, functions, universal type quantifiers, whatever - but no recursion.
To implement some function for C a, we usually need to have a corresponding function for F a r. For example, we can implement fmap:
fmap: (a → b) → C a → C b
but only if we have bimap for F.
We can implement depth:
depth: C a → Int -- count the maximum recursion depth of a value.
but only if we have a "traverse" for F that works like this:
traverse: Applicative h => (r → h s) → F a r → h (F a s)
We can implement traverse for C a but only if we have bisequence for F (see my post here https://chaource.dreamwidth.org/229017.html ).
Using `depth`, we can transform any `C a` into a Church-encoded `Nat`, counting the maximum recursion depth. Then we can implement your `recursion-safe hylo` from this post.
So the "Church encoding approach" consists of asking: what functions can be implemented without recursion, if we are allowed to use catamorphisms and the properties of F.
Typically, F will be a simple, non-recursive polynomial bifunctor, like F a r = Maybe (a, r, r) for the type of trees that you considered. So we will have properties like bimap, traverse, bitraverse, etc., easily implementable for F without recursion.