# Double Bailout Fold

Posted on 2018-01-10 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module DoubleBailoutFold (
dbfoldr, _test_dbfoldr, main_dbfoldr
) where

import Testing
import Booleans
import Tuples
import DisjointUnions
import NaturalNumbers
import Lists
import HeadAndTail

In this post we’ll construct a hybrid of double fold and bailout fold.

Let $$A$$ and $$B$$ be sets. Suppose we have maps $\delta : B \rightarrow C,$ $\beta : A \times \lists{A} \times B \rightarrow \bool,$ $\mu : B \rightarrow B,$ $\psi : A \times \lists{A} \times B \rightarrow C,$ and $\chi : A \times B \times C \times C \rightarrow C.$ Then there is a unique map $$\Theta : \lists{A} \times B \rightarrow C$$ such that $\Theta(\nil,b) = \delta(b)$ and $\Theta(\cons(a,x),b) = \left\{\begin{array}{ll} \psi(a,x,b) & \mathrm{if}\ \beta(a,x,b) \\ \chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b))) & \mathrm{otherwise}. \end{array}\right.$ We denote this $$\Theta$$ by $$\dbfoldr(\delta)(\beta)(\mu)(\psi)(\chi)$$.

Define $$\varepsilon : B \times \lists{A} \rightarrow C$$ by $\varepsilon(b,x) = \delta(b)$ and $$\varphi : A \times C^{B \times \lists{A}} \rightarrow C^{B \times \lists{A}}$$ casewise by $\varphi(a,g)(b,x) = \left\{\begin{array}{ll} \psi(a,\tail(x),b) & \mathrm{if}\ \beta(a,\tail(x),b) \\ \chi(a,\tail(x),b,g(b,\tail(x)),g(\mu(b),\tail(x))) & \mathrm{otherwise}, \end{array}\right.$ and let $$\Theta(x,b) = \foldr(\varepsilon)(\varphi)(x)(b,x)$$. To see that $$\Theta$$ solves the given equations, note that $\begin{eqnarray*} & & \Theta(\nil,b) \\ & = & \foldr(\varepsilon)(\varphi)(\nil)(b,\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varepsilon(b,\nil) \\ & = & \delta(b), \end{eqnarray*}$ that $\begin{eqnarray*} & & \Theta(\cons(a,x),b) \\ & = & \foldr(\delta)(\varphi)(\cons(a,x))(b,\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(\delta)(\varphi)(x))(b,\cons(a,x)) \\ & = & \bif{\beta(a,\tail(\cons(a,x)),b)}{\psi(a,\tail(\cons(a,x)),b)}{\chi(a,\tail(\cons(a,x)),b,\foldr(\varepsilon)(\varphi)(x)(b,\tail(\cons(a,x))),\foldr(\varepsilon)(\varphi)(x)(\mu(b),\tail(\cons(a,x))))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\foldr(\varepsilon)(\varphi)(x)(b,x),\foldr(\varepsilon)(\varphi)(x)(\mu(b),x))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b)))} \end{eqnarray*}$ as needed. Now suppose $$\Psi : \lists{A} \times B \rightarrow C$$ also satisfies the equations; we show that $$\Psi = \Theta$$ by list induction. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \Psi(\nil,b) \\ & = & \delta(b) \\ & = & \Theta(\nil,b) \end{eqnarray*}$ as needed. For the inductive step, suppose the equations hold for all $$b$$ for some $$x$$, and let $$a \in A$$. Then we have $\begin{eqnarray*} & & \Psi(\cons(a,x),b) \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Psi(x,b),\Psi(x,\mu(b)))} \\ & = & \bif{\beta(a,x,b)}{\psi(a,x,b)}{\chi(a,x,b,\Theta(x,b),\Theta(x,\mu(b)))} \\ & = & \Theta(\cons(a,x),b) \end{eqnarray*}$ as needed.

## Implementation

We can implement $$\dbfoldr$$ using the definition or the universal property.

dbfoldr, dbfoldr'
:: (List t)
=> (b -> c)
-> (a -> t a -> b -> Bool)
-> (b -> b)
-> (a -> t a -> b -> c)
-> (a -> t a -> b -> c -> c -> c)
-> t a -> b -> c

dbfoldr' delta beta mu psi chi x b = foldr epsilon phi x (b,x)
where
epsilon (a,_) = delta a

phi a g (c,w) = if beta a (tail w) c
then psi a (tail w) c
else chi a (tail w) c (g (c, tail w)) (g (mu c, tail w))

-- terrible notation, or the worst notation?
dbfoldr δ β μ ψ χ = ξ
where
ξ z b = case uncons z of
Left () -> δ b
Right (Pair a x) -> if β a x b
then ψ a x b
else χ a x b (ξ x b) (ξ x (μ b))

We should check that these two agree.

_test_dbfoldr_equiv :: (List t, Equal (t a), Equal c)
=> t a -> b -> c
-> Test ((b -> c) -> (a -> t a -> b -> Bool) -> (b -> b) -> (a -> t a -> b -> c) -> (a -> t a -> b -> c -> c -> c) -> t a -> b -> Bool)
_test_dbfoldr_equiv _ _ _ =
testName "dbfoldr(delta,beta,mu,psi,chi)(x,b) == dbfoldr'(delta,beta,mu,psi,chi)(x,b)" \$
\delta beta mu psi chi x b -> eq
(dbfoldr delta beta mu psi chi x b)
(dbfoldr' delta beta mu psi chi x b)

## Testing

Suite:

_test_dbfoldr ::
( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a), CoArbitrary (t a)
, CoArbitrary b, Arbitrary b, Show b, CoArbitrary c, Arbitrary c
, TypeName b, TypeName c, Equal b, Equal c
) => Int -> Int -> t a -> b -> c -> IO ()
_test_dbfoldr size cases t b c = do
testLabel3 "dbfoldr" t b c

let args = testArgs size cases

runTest args (_test_dbfoldr_equiv t b c)

Main:

main_dbfoldr :: IO ()
main_dbfoldr = do
_test_dbfoldr 50 500 (nil :: ConsList Bool)  (zero :: Unary) (zero :: Unary)
_test_dbfoldr 50 500 (nil :: ConsList Unary) (zero :: Unary) (zero :: Unary)
_test_dbfoldr 50 500 (nil :: ConsList Bool)  (zero :: Unary) (true :: Bool)
_test_dbfoldr 50 500 (nil :: ConsList Unary) (zero :: Unary) (true :: Bool)