zipping church-encoded stuff

[sassa_nf]

We had a little discussion here

Basic question: if lists are Church-encoded, how do you zip two at the same time? There seems to be a difficulty in commuting list construction (new list) and list destruction (two input lists).

Initially I thought of a way to preserve the state of list destructor routine. So on each step of construction you can progress the iterator of the destructor one step at a time. But a good question chaource raised is: how can we generalise this to trees?

And then from the dark recesses of my memory the shadows of Varmo Vene's thesis whispered.

Hylo morphism to the rescue!

Wink-wink, nudge-nudge, say no more!
Executable code

{-# LANGUAGE RankNTypes #-}

newtype List a = List {list :: forall r. r -> (a -> r -> r) -> r}

newtype Option a = Option {option :: forall r. r -> (a -> r) -> r}

none :: forall a. Option a
none = Option $ const

some :: a -> Option a
some a = Option $ \_ f -> f a

nil :: forall a. List a
nil = List $ const

cons :: a -> List a -> List a
cons h t = List $ \z f -> f h $ list t z f

headOption :: List a -> Option a
headOption l = list l none $ \a _ -> some a

ttail :: List a -> List a
ttail xs = snd $ list xs (nil, nil) $ \h (t, _) -> (cons h t, t)

-- pass it three functions: (not in this order)
-- what to do on the way down, what to do on the way up,
-- and what to do to turn around
hylo :: List a -> (p -> r) -> (p -> a -> p) -> (p -> a -> r -> r) -> (p -> r)
hylo l z f g = list l z $ \h t p -> g p h $ t $ f p h

-- concatenation of lists is...
-- pass through input value on the way down
-- reconstruct the original list on the way up
-- use the passed value at the turn-around point
(+++) :: List a -> List a -> List a
xs +++ ys = hylo xs id const (const cons) ys

-- zipping of two lists is...
-- pass the tail of input list on the way down
-- reconstruct the original list with the head of the list that was passed from above
-- use empty list at the turn-around point
zzip :: List a -> List b -> List (a, b)
zzip xs ys = hylo xs
                  (const nil)
                  (\ys _ -> ttail ys)
                  (\ys a t -> option (headOption ys) nil $ \b -> cons (a, b) t)
                  ys

-- for printability of the church-encoded list, let's convert it to Haskell list
tolist l = list l [] (:)

main = print $ tolist
       $ zzip (cons 0 $ cons 1 $ cons 3 $ cons 4 nil)
            $ (cons 'a' $ cons 'b' nil) +++ (cons 'c' nil)

-- for the above we get this:
-- [(0,'a'),(1,'b'),(3,'c')]

Obvious extension for church-encoded trees:
(Some more executable)

...
newtype Tree a = Tree {tree :: forall r. r -> (a -> r -> r -> r) -> r}

leaf :: forall a. Tree a
leaf = Tree $ const

node :: a -> Tree a -> Tree a -> Tree a
node a l r = Tree $ \z f -> f a (tree l z f) (tree r z f)


root :: Tree a -> (Option a, Tree a, Tree a)
root t = tree t (none, leaf, leaf) $ \v l r -> (some v, tt l, tt r) where
  tt (v, l, r) = option v leaf $ \v -> node v l r


val :: Tree a -> Option a
val t = let (r, _, _) = root t in r

left :: Tree a -> Tree a
left t = let (_, r, _) = root t in r

right :: Tree a -> Tree a
right t = let (_, _, r) = root t in r

-- hylomorphism for a tree is similar to list, only when passing the value down
-- we also indicate did we go left or right from the parent to reach the next node
-- hence extra Bool argument to all functions
-- but essentially it is the same:
-- a function what to do on the way down
-- a function what to do on the way up
-- a function what to do to turn around
treehylo :: Tree a -> (p -> Bool -> r) ->
                      (p -> Bool -> a -> p) ->
                      (p -> Bool -> a -> r -> r -> r) ->
                      (p -> Bool -> r)
treehylo t z f g = tree t z
   $ \n l r p b -> g p b n
                     (l (f p False n) False)
                     (r (f p True n) True)

-- zipping two trees is really similar to zipping two lists
tzip :: Tree a -> Tree b -> Tree (a, b)
tzip xs ys = treehylo xs
                      (\_ _ -> leaf)
                      (\ys b _ -> if b then right ys else left ys)
                      (\ys _ x l r -> option (val ys) leaf $ \y -> node (x, y) l r)
                      ys True

-- just for printability, define tree type as data
data T a = Leaf | Node a (T a) (T a) deriving (Show)

tot :: Tree a -> T a
tot t = tree t Leaf Node

main = do
...
  print $ tot $ tzip (node 0 (node 1 leaf leaf) (node 2 leaf leaf)) (node 'a' leaf (node 'b' leaf leaf))

-- here's output for zipping the above two trees - as expected
-- > Node (0,'a') Leaf (Node (2,'b') Leaf Leaf)

Of course, we could do church-encoding of pairs as well, but I reckon we don't have to do that even for Option. The original problem was driven by the quest of expressing recursive data structures in the language that doesn't support it (to prove that the structures and types are finite). Finite non-recursive types like Maybe and Pair are not problematic.

---

After some more discussion:

So, a proper hylomorphism for zip is like so:

data Tr a x = TL | TN a x x

instance Functor (Tr a) where
  fmap f TL = TL
  fmap f (TN a l r) = TN a (f l) (f r)

thylo :: Functor f => (f b -> b) -> (a -> f a) -> a -> b
thylo psi phi = psi . fmap (thylo psi phi) . phi

tz :: Tree a -> Tree b -> Tree (a, b)
tz xs ys = thylo psi phi (xs, ys) where
  phi (xs, ys) = option (val xs) TL $
                 \x -> option (val ys) TL $
                 \y -> TN (x, y) (left xs, left ys) (right xs, right ys)

  psi TL = leaf
  psi (TN v l r) = node v l r

It works as intended.

The difficulty, of course, is the self-reference in the definition of thylo.

We can avoid that, if we can build a Tree of finite size that is large enough to include both xs and ys.

newtype Nat = Nat {nat :: forall r. (r -> r) -> r -> r}

zero :: Nat
zero = Nat $ \_ -> id

suc :: Nat -> Nat
suc n = Nat $ \f -> f . nat n f

one = suc zero

two = suc one

three = suc two

add :: Nat -> Nat -> Nat
add x y = nat x suc y

mul :: Nat -> Nat -> Nat
mul x y = nat x (add y) zero

ex :: Nat -> Nat -> Nat
ex x y = nat y (mul x) one

five = add two three

thirtytwo = ex two five

-- now we can convert any 32-bit number into a Nat without loops
tonat :: Int -> Nat
tonat n = (\(x, _, _) -> x) $ nat thirtytwo pow (zero, one, n) where
  pow (n, m, x) = (add n (if even x then zero else m), add m m, x `div` 2)

tunfold :: Int -> Tree Int
tunfold n = (nat $ tonat n) (\t -> node (option (val t) 0 (+1)) t t) leaf

height :: Tree a -> Int
height t = tree t 0 $ \_ l r -> 1 + (max l r)

-- generates a tree of a predetermined height
-- since we can't guarantee termination otherwise, this produces a size-bound recursion that produces
-- trees up to that size
ana :: Int -> (p -> Tr r p) -> p -> Tree r
ana n phi = tree (tunfold n) (\_ -> leaf) $ \_ l r p -> pp l r (phi p) where
  pp _ _ TL = leaf
  pp l r (TN a x y) = node a (l x) (r y)

tzz :: Tree a -> Tree b -> Tree (a, b)
tzz xs ys = ana (max (height xs) (height ys)) phi (xs, ys) where
  phi (xs, ys) = option (val xs) TL $
                 \x -> option (val ys) TL $
                 \y -> TN (x, y) (left xs, left ys) (right xs, right ys)

ana finds a fixed point of (Tr a) for any tree up to a given size. To do that, it precomputes a function that can produce a tree up to a given height, where each subtree is computed from a given seed value using phi, which produce a Tr with the necessary value and corresponding seed values for left and right subtrees in it.

One of the problems with the absence of recursion is that even implementing a loop becomes a problem. I don't know if the target language provides any means for bounded recursion, but here's how we can achieve that in pure Church-encoded world - we can turn integers of a bounded size into Nat, Church-encoded natural numbers.