![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
chaourcePart 1, Part 2, and the relevant posts by sassa_nf: "zipping church-encoded stuff" and "Size-restricted recursion for hylomorphism"
In Part 2, I found that the `zip` function can be implemented in general for any Church-encoded data type:
which implements the least fixpoint (µ r. S a r).
The implementation of `zip` is possible if we have four functions:
The "depth" function should compute the maximum depth of recursion necessary for representing a given Church-encoded value. For lists, it is simply the length of the list; for trees, the maximum depth of all branches of the tree.
For lists:
For non-empty trees:
The "depth" function can be implemented more generically if we have a "bitraverse" function for S (that function is shown in "Traversals in Church encoding").
The "bitraverse" function is certainly available for any polynomial bifunctor S.
Currently we will only consider a bifunctor S that is itself non-recursively defined. If S were itself recursive, say, S a r = µ t. T a r t, we would have to Church-encode S itself (since our present goal is to avoid recursion). After that, implementing "bizipC", "bitraverse", etc. will depend on the properties of the 3-functor T, which should itself have methods such as "zip0", "trizip", "tritraverse" and so on. I do not expect any more than some technical difficulties when going in that direction. For now, let's assume that S is a non-recursively defined, polynomial functor.
It remains to show that zip0 and bizipC can be implemented for any polynomial bifunctor S. Then it will follow that we have implemented a `zip` method for any Church encoding C, with type signature:
The implementation goes via the function `hylo1` defined in Part 2:
where we need to set the types as:
The first argument of hylo1 (of type Natural) is computed as the maximum depth of the arguments ca and cb. This will be the recursion depth limit for the entire computation. The depth of a given value ca : C a can be computed via this function:
The second argument of hylo1 is of type p → q, that is, (C a, C b) → C (a, b). That argument is the "bad" implementation of zip, shown in Part 2, via the function zip0. It does not matter that the implementation violates the laws of zip, because it's just a stop-gap value that will never be actually used if the recursion depth limit is sufficiently large (but the stop-gap value still needs to be supplied).
The third argument of hylo1 is the coalgebra map of type p → S c p, that is, (C a, C b) → S (a, b) (C a, C b). This type is equivalent to the type of bizipC.
The fourth argumet of hylo1 is the algebra map of type S c q → q, that is, S (a, b) C (a, b) → C (a, b), and this is the standard algebra map that the type C (a, b) comes with. (The type C x is always an algebra of the functor S x.)
The fifth argument of hylo1 is of type p, that is, (C a, C b) and it is just the pair (ca, cb).
The result value of hylo1 is of type q, that is, C (a, b), and it is the result of zipping ca with cb.
Implementing zip0
To implement zip0 for any polynomial bifunctor S, we represent S via the Horner scheme for polynomials: S(a, r) = P(r) + a * Q(a, r) where Q has a lower degree in "a" than S. In the code syntax:
Because Q is a polynomial of lower degree in "a", we may assume that zip0 is already defined for Q (call it zip0_Q) by an inductive assumption.
Then zip0 is implemented case by case like this:
zip0 (Left pr) _ = Left pr -- okay to drop the argument
zip0 _ (Left pr) _ = Left pr
zip0 (Right (a, qar)) (Right (b, qbr)) = Right ((a, b), zip0_Q qar qbr) -- apply Q's zip0 here.
It does not matter that zip0 ignores some arguments, because zip0 is not required to satisfy any laws. As long as zip0 fits its required type signature, we are done.
implementing bizipC
To implement bizipC, we again use the Horner scheme but in a different way: S a r = P(a) + r * Q(a, r), where P(a) must already have a zipP function defined for it. We will also use the Horner scheme for P(a) as P(a) = P0 + a * P1(a) with P0 being a monoidal type (or else zipP would not be definable). Then:
Because Q is a polynomial of lower degree in "r", we may assume that bizipC is already defined for Q (call it bizipC_Q) by an inductive assumption.
Then bizipC is implemented case by case like this:
bizipC (Left pa) (Left pb) = Left (zipP pa pb) -- assuming that zipP: P a -> P b -> P (a, b) exists for P
bizipC (Left pa) (Right (cb, qbcb)) = ???
bizipC (Right (ca, qaca)) (Left pb) = ???
bizipC (Right (ca, qaca)) (Right (cb, qbcb)) = Right ((ca, cb), bizipC_Q qaca qbcb) -- apply Q's bizipC here.
To define bizipC in the two remaining cases, we need to use the Horner's scheme for P. We have two symmetric cases, so let's write `bizipC (Left pa) (Right (cb, qbcb))`. Horner's scheme for P is that pa can be either P0 or (a, P1 a).
This implementation discards some information (the argument of type P1 a) but this seems to be inevitable in a generic implementation.
For a specific data type where P is nontrivial, one might choose a better implementation. For example: suppose S a r = Either (a, a) (r, r). This recursion scheme describes nonempty trees whose leaves carry a pair (a, a) and whose branches have always 2 subtrees. How to implement `bizipC` for those trees?
However, it would not be so easy to figure out what to do if a tree has leaves with type (a, a) but branches with type (r, r, r), that is, 3 branches. If we want to zip a leaf with a 3-branching, somehow we need to distribute the data from the leaf across the 3 branches, but it is not obvious how. One possibility is to take the first value from the leaf and to copy it to all 3 branches. This is what the generic implementation above does: it says P a = (a, a) and then takes the Horner scheme P a = (a, P1 a) where P1 a = a. Then the data from `P1 a` will be dropped during zipping with a branching.
Whatever we implement, we still need to verify that the laws of zip will hold.
In any case, `bizipC` is available for any polynomial recursion schemes S. This makes it likely that `zip` (satisfying all the laws) can be defined generically for Church-encoded types.
In Part 2, I found that the `zip` function can be implemented in general for any Church-encoded data type:
C a = ∀(r : Type) → (S a r → r) → r
which implements the least fixpoint (µ r. S a r).
The implementation of `zip` is possible if we have four functions:
bimap: (a → c) → (b → d) → S a b → S c d depth: S a Natural → Natural zip0: S a r → S b r → S (a, b) r bizipC: S a (C a) → S b (C b) → S (a, b) (C a, C b)
The "depth" function should compute the maximum depth of recursion necessary for representing a given Church-encoded value. For lists, it is simply the length of the list; for trees, the maximum depth of all branches of the tree.
For lists:
S a r = Either Unit (a, r) depth: Either Unit (a, Natural) → Natural depth (Left ()) = 0 depth (Right (_, n)) = 1 + n
For non-empty trees:
S a r = Either a (r, r) depth: Either Unit (a, Natural) → Natural depth (Left _) = 0 depth (Right (m, n)) = 1 + max m n
The "depth" function can be implemented more generically if we have a "bitraverse" function for S (that function is shown in "Traversals in Church encoding").
The "bitraverse" function is certainly available for any polynomial bifunctor S.
Currently we will only consider a bifunctor S that is itself non-recursively defined. If S were itself recursive, say, S a r = µ t. T a r t, we would have to Church-encode S itself (since our present goal is to avoid recursion). After that, implementing "bizipC", "bitraverse", etc. will depend on the properties of the 3-functor T, which should itself have methods such as "zip0", "trizip", "tritraverse" and so on. I do not expect any more than some technical difficulties when going in that direction. For now, let's assume that S is a non-recursively defined, polynomial functor.
It remains to show that zip0 and bizipC can be implemented for any polynomial bifunctor S. Then it will follow that we have implemented a `zip` method for any Church encoding C, with type signature:
zip: C a -> C b -> C (a, b) zip ca cb = hylo1 ...
The implementation goes via the function `hylo1` defined in Part 2:
hylo1: Natural → (p → q) → (p → S c p) → (S c q → q) → p → q
where we need to set the types as:
p = (C a, C b) q = C (a, b) c = (a, b)
The first argument of hylo1 (of type Natural) is computed as the maximum depth of the arguments ca and cb. This will be the recursion depth limit for the entire computation. The depth of a given value ca : C a can be computed via this function:
depthC: C a → Natural depthC ca = ca depth
The second argument of hylo1 is of type p → q, that is, (C a, C b) → C (a, b). That argument is the "bad" implementation of zip, shown in Part 2, via the function zip0. It does not matter that the implementation violates the laws of zip, because it's just a stop-gap value that will never be actually used if the recursion depth limit is sufficiently large (but the stop-gap value still needs to be supplied).
The third argument of hylo1 is the coalgebra map of type p → S c p, that is, (C a, C b) → S (a, b) (C a, C b). This type is equivalent to the type of bizipC.
The fourth argumet of hylo1 is the algebra map of type S c q → q, that is, S (a, b) C (a, b) → C (a, b), and this is the standard algebra map that the type C (a, b) comes with. (The type C x is always an algebra of the functor S x.)
The fifth argument of hylo1 is of type p, that is, (C a, C b) and it is just the pair (ca, cb).
The result value of hylo1 is of type q, that is, C (a, b), and it is the result of zipping ca with cb.
Implementing zip0
To implement zip0 for any polynomial bifunctor S, we represent S via the Horner scheme for polynomials: S(a, r) = P(r) + a * Q(a, r) where Q has a lower degree in "a" than S. In the code syntax:
S a r = Either (P r) (a, Q a r) zip0: S a r → S b r → S (a, b) r zip0: (Either (P r) (a, Q a r)) → (Either (P r) (b, Q b r)) → (Either (P r) ((a, b), Q (a, b) r))
Because Q is a polynomial of lower degree in "a", we may assume that zip0 is already defined for Q (call it zip0_Q) by an inductive assumption.
Then zip0 is implemented case by case like this:
zip0 (Left pr) _ = Left pr -- okay to drop the argument
zip0 _ (Left pr) _ = Left pr
zip0 (Right (a, qar)) (Right (b, qbr)) = Right ((a, b), zip0_Q qar qbr) -- apply Q's zip0 here.
It does not matter that zip0 ignores some arguments, because zip0 is not required to satisfy any laws. As long as zip0 fits its required type signature, we are done.
implementing bizipC
To implement bizipC, we again use the Horner scheme but in a different way: S a r = P(a) + r * Q(a, r), where P(a) must already have a zipP function defined for it. We will also use the Horner scheme for P(a) as P(a) = P0 + a * P1(a) with P0 being a monoidal type (or else zipP would not be definable). Then:
S a r = Either (Either P0 (P a)) (r, Q a r) bizipC: S a (C a) → S b (C b) → S (a, b) (C a, C b) bizipC: Either (P a) (C a, Q a (C a)) → (Either (P b) (C b, Q b (C b))) → (Either (P (a, b)) ((C a, C b), Q (a, b) (C a, C b)))
Because Q is a polynomial of lower degree in "r", we may assume that bizipC is already defined for Q (call it bizipC_Q) by an inductive assumption.
Then bizipC is implemented case by case like this:
bizipC (Left pa) (Left pb) = Left (zipP pa pb) -- assuming that zipP: P a -> P b -> P (a, b) exists for P
bizipC (Left pa) (Right (cb, qbcb)) = ???
bizipC (Right (ca, qaca)) (Left pb) = ???
bizipC (Right (ca, qaca)) (Right (cb, qbcb)) = Right ((ca, cb), bizipC_Q qaca qbcb) -- apply Q's bizipC here.
To define bizipC in the two remaining cases, we need to use the Horner's scheme for P. We have two symmetric cases, so let's write `bizipC (Left pa) (Right (cb, qbcb))`. Horner's scheme for P is that pa can be either P0 or (a, P1 a).
bizipC (Left p0) (Right (cb, qbcb)) = Left p0 bizipC (Left (x : a, _: P1 a) (Right (cb, qbcb)) = Right ((ca, cb), qabcacb) where cb2ca: C b → C a = fmap (λ(_: b) → x) ca : C a = cb2ca cb qabcacb : Q (a, b) (C a, C b) = bimap_Q (λ(y: b) → (x, y)) (λ(cy: C b) → (ca, cy)) qbcb
This implementation discards some information (the argument of type P1 a) but this seems to be inevitable in a generic implementation.
For a specific data type where P is nontrivial, one might choose a better implementation. For example: suppose S a r = Either (a, a) (r, r). This recursion scheme describes nonempty trees whose leaves carry a pair (a, a) and whose branches have always 2 subtrees. How to implement `bizipC` for those trees?
bizipC : Either (a, a) (C a, C a) → Either (b, b) (C b, C b) → Either ((a, b), (a, b)) ((C a, C b), (C a, C b)) bizipC (Left (x1, x2)) (Left (y1, y2)) = Left ((x1, y1), (x2, y2)) bizipC (Left (x1, x2)) (Right (cb1, cb2)) = Right((ca1, cb1), (ca2, cb2)) where ca1 = fmap (λ(_: b) → x1) cb1 ca2 = fmap (λ(_: b) → x2) cb2 bizipC (Right (ca1, ca2)) (Left (y1, y2)) = -- analogous to the previous case but swap a and b, x and y everywhere bizipC (Right (ca1, ca2)) (Right (cb1, cb2)) = Right ((ca1, cb1), (ca2, cb2))
However, it would not be so easy to figure out what to do if a tree has leaves with type (a, a) but branches with type (r, r, r), that is, 3 branches. If we want to zip a leaf with a 3-branching, somehow we need to distribute the data from the leaf across the 3 branches, but it is not obvious how. One possibility is to take the first value from the leaf and to copy it to all 3 branches. This is what the generic implementation above does: it says P a = (a, a) and then takes the Horner scheme P a = (a, P1 a) where P1 a = a. Then the data from `P1 a` will be dropped during zipping with a branching.
Whatever we implement, we still need to verify that the laws of zip will hold.
In any case, `bizipC` is available for any polynomial recursion schemes S. This makes it likely that `zip` (satisfying all the laws) can be defined generically for Church-encoded types.
