# TakeWhile and DropWhile

Posted on 2017-12-16 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module TakeWhileAndDropWhile
( takeWhile, dropWhile
, _test_takewhile_dropwhile, main_takewhile_dropwhile
) where

import Testing
import Booleans
import NaturalNumbers
import Lists
import ConsumingFold
import Cat
import PrefixAndSuffix
import Sublist

Today we’ll define two functions, $$\takeWhile$$ and $$\dropWhile$$, similar to $$\take$$ and $$\drop$$, but instead of taking or dropping a prefix of some length, we will take or drop the longest prefix satisfying some predicate. We’d like $$\takeBut$$ to have a signature like $\takeWhile : \bool^A \rightarrow {\lists{A}}^{\lists{A}}.$

As usual, suppose $$\takeWhile$$ can be defined in terms of fold; say $\takeWhile(p)(x) = \foldr(e)(\varphi)(x)$ for some $$e$$ and $$\varphi$$. To make the types work out we need $$e \in \lists{A}$$ and $$\varphi : A \times \lists{A} \rightarrow \lists{A}$$. Thinking about the desired behavior for $$\takeWhile$$, we need

$\begin{eqnarray*} & & \nil \\ & = & \takeWhile(p)(\nil) \\ & = & \foldr(e)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e \end{eqnarray*}$

and

$\begin{eqnarray*} & & \bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil} \\ & = & \takeWhile(p)(\cons(a,x)) \\ & = & \foldr(e)(\varphi)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(x)) \\ & = & \varphi(a,\takeWhile(p,x)) \end{eqnarray*}$

With this in mind, we define $$\takeWhile$$ like so.

Let $$A$$ be a set, with $$p : A \rightarrow \bool$$. Define $$\varphi(p) : A \times \lists{A} \rightarrow \lists{A}$$ by $\varphi(p)(a,x) = \left\{ \begin{array}{ll} \cons(a,x) & \mathrm{if}\ p(a) = \btrue \\ \nil & \mathrm{otherwise}. \end{array} \right.$

We define $$\takeWhile : \bool^A \times \lists{A} \rightarrow \lists{A}$$ by $\takeWhile(p,x) = \foldr(\nil)(\varphi(p))(x).$

takeWhile :: (List t) => (a -> Bool) -> t a -> t a
takeWhile p = foldr nil phi
where
phi a x = if eq (p a) true
then cons a x
else nil

As usual, since $$\takeWhile$$ is defined directly in terms of foldr it is the unique solution to a system of functional equations.

Let $$A$$ be a set. Then $$\takeWhile$$ is the unique function $f : \bool^A \times \lists{A} \rightarrow \lists{A}$ satisfying the following system of equations for all $$p : A \rightarrow \bool$$, $$a \in A$$, and $$x \in \lists{A}$$. $\left\{\begin{array}{l} f(p,\nil) = \nil \\ f(p,\cons(a,x)) = \bif{p(a)}{\cons(a,f(p,x))}{\nil}. \end{array}\right.$

_test_takeWhile_nil :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> Bool)
_test_takeWhile_nil t =
testName "takeWhile(p)(nil) == nil" $\p -> eq (takeWhile p nil) (nil withTypeOf t) _test_takeWhile_cons :: (List t, Equal a, Equal (t a)) => t a -> Test ((a -> Bool) -> a -> t a -> Bool) _test_takeWhile_cons t = testName "takeWhile(p)(cons(a,x)) == if(p(a),cons(a,takeWhile(p)(x),nil))"$
\p a x -> eq
(takeWhile p (cons a x))
(if p a then cons a (takeWhile p x) else nil)

$$\takeWhile$$ gives prefixes.

Let $$A$$ be a set and $$p : A \rightarrow \bool$$. For all $$x \in \lists{A}$$, we have $\prefix(\takeWhile(p,x),x) = \btrue.$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \prefix(\takeWhile(p,\nil),\nil) \\ & = & \prefix(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x \in \lists{A}$$, and let $$a \in A$$. We have $\begin{eqnarray*} & & \prefix(\takeWhile(p,\cons(a,x),\cons(a,x))) \\ & = & \prefix(\bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil},\cons(a,x)) \\ & = & \bif{p(a)}{\prefix(\cons(a,\takeWhile(p,x)),\cons(a,x))}{\prefix(\nil,\cons(a,x))} \\ & = & \bif{p(a)}{\prefix(\takeWhile(p,x),x)}{\btrue} \\ & = & \bif{p(a)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}$ as needed.

_test_takeWhile_prefix :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_prefix _ =
testName "prefix(takeWhile(p,x),x) == true" $\p x -> eq (prefix (takeWhile p x) x) true So $$\takeWhile$$ also gives a sublists. Let $$A$$ be a set, with $$p : A \rightarrow \bool$$ and $$x \in \lists{A}$$. Then we have $\sublist(\takeWhile(k,x),x) = \btrue.$ We have $\prefix(\takeWhile(k,x),x) = \btrue,$ so $\infix(\takeWhile(k,x),x) = \btrue,$ so $\sublist(\takeWhile(k,x),x) = \btrue$ as claimed. _test_takeWhile_sublist :: (List t, Equal a, Equal (t a)) => t a -> Test ((a -> Bool) -> t a -> Bool) _test_takeWhile_sublist _ = testName "sublist(takeWhile(p,x),x) == true"$
\p x -> eq (sublist (takeWhile p x) x) true

$$\takeWhile$$ is idempotent.

Let $$A$$ be a set with $$p : A \rightarrow \bool$$. Then for all $$x \in \lists{A}$$ we have $\takeWhile(p,\takeWhile(p,x)) = \takeWhile(p,x).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, note that $\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,x)) \\ & = & \takeWhile(p,\takeWhile(p,\nil)) \\ & = & \takeWhile(p,\nil) \\ & = & \takeWhile(p,x) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x \in \lists{A}$$, and let $$a \in A$$. If $$p(a) = \btrue$$, we have $\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,\cons(a,x))) \\ & = & \takeWhile(p,\cons(a,\takeWhile(p,x))) \\ & = & \cons(a,\takeWhile(p,\takeWhile(p,x))) \\ & = & \cons(a,\takeWhile(p,x)) \\ & = & \takeWhile(p,\cons(a,x)) \end{eqnarray*}$ as needed. If $$p(a) = \bfalse$$, we have $\begin{eqnarray*} & & \takeWhile(p,\takeWhile(p,\cons(a,x))) \\ & = & \takeWhile(p,\nil) \\ & = & \nil \\ & = & \takeWhile(p,\cons(a,x)) \end{eqnarray*}$ as needed.

_test_takeWhile_idempotent :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> t a -> Bool)
_test_takeWhile_idempotent _ =
testName "takeWhile(p,takeWhile(p,x)) == takeWhile(p,x)" $\p x -> eq (takeWhile p (takeWhile p x)) (takeWhile p x) $$\takeWhile$$ commutes with itself (kind of). Let $$A$$ be a set with $$p$$ and $$q$$ mappings $$A \rightarrow \bool$$. Then for all $$x \in \lists{A}$$ we have $\takeWhile(p,\takeWhile(q,x)) = \takeWhile(q,\takeWhile(p,x)).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, note that $\begin{eqnarray*} & & \takeWhile(p,\takeWhile(q,x)) \\ & = & \takeWhile(p,\takeWhile(q,\nil)) \\ & = & \takeWhile(p,\nil) \\ & = & \nil \\ & = & \takeWhile(q,\nil) \\ & = & \takeWhile(q,\takeWhile(p,\nil)) \\ & = & \takeWhile(q,\takeWhile(p,x)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x \in \lists{A}$$, and let $$a \in A$$. If $$p(a) = \btrue$$, we have $\begin{eqnarray*} & & \takeWhile(p,\takeWhile(q,\cons(a,x))) \\ & = & \takeWhile(p,\bif{q(a)}{\cons(a,\takeWhile(q,x))}{\nil}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \bif{q(a)}{\takeWhile(p,\cons(a,\takeWhile(q,x)))}{\takeWhile(p,\nil)} \\ & = & \bif{q(a)}{\bif{p(a)}{\cons(a,\takeWhile(p,\takeWhile(q,x)))}{\nil}}{\nil} \\ & = & \bif{q(a)}{\bif{p(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\bif{p(a)}{\nil}{\nil}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-ifnest} = & \bif{p(a)}{\bif{q(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\bif{q(a)}{\nil}{\nil}} \\ & = & \bif{p(a)}{\bif{q(a)}{\cons(a,\takeWhile(q,\takeWhile(p,x)))}{\nil}}{\nil} \\ & = & \bif{p(a)}{\takeWhile(q,\cons(a,\takeWhile(p,x)))}{\takeWhile(q,\nil)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-iffunc} = & \takeWhile(q,\bif{p(a)}{\cons(a,\takeWhile(p,x))}{\nil}) \\ & = & \takeWhile(q,\takeWhile(p,\cons(a,x))) \end{eqnarray*}$ as needed. _test_takeWhile_commutes :: (List t, Equal a, Equal (t a)) => t a -> Test ((a -> Bool) -> (a -> Bool) -> t a -> Bool) _test_takeWhile_commutes _ = testName "takeWhile(p,takeWhile(q,x)) == takeWhile(q,takeWhile(p,x))"$
\p q x ->
eq (takeWhile p (takeWhile q x)) (takeWhile q (takeWhile p x))

Now for $$\dropWhile$$. This function should drop the longest prefix satisfying some predicate, again with signature $$\bool^A \times \lists{A} \rightarrow \lists{A}$$. If we try defining this using foldr in the “obvious” way, we run into trouble, where the $$\varphi$$ parameter needs to have its argument and eat it too. (try it!) One way around this is the trick we used to define $$\zip$$.

Suppose $\dropWhile(p,x) = \foldr(e)(\varphi)(x)(x)$ for some $$e$$ and $$\varphi$$. To make the types work out, we need $e \in \lists{A}^{\lists{A}}$ and $\varphi : A \times \lists{A}^{\lists{A}} \rightarrow \lists{A}^{\lists{A}};$ now $\begin{eqnarray*} & & \nil \\ & = & \dropWhile(p,\nil) \\ & = & \foldr(e)(\varphi)(\nil)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e(\nil) \end{eqnarray*}$ and $\begin{eqnarray*} & & \varphi(a,\foldr(e)(\varphi)(x))(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(e)(\varphi)(\cons(a,x))(\cons(a,x)) \\ & = & \dropWhile(p,\cons(a,x)) \\ & = & \bif{p(a)}{\dropWhile(p,x)}{\cons(a,x)} \end{eqnarray*}$

(that last line is why using a plain fold doesn’t work.) In cases like this, the consuming fold is handy.

Let $$A$$ be a set with $$p : A \rightarrow \bool$$. Define $$\sigma : A \times \lists{A} \times \lists{A} \rightarrow \lists{A}$$ by $\sigma(a,x,y) = \bif{p(a)}{y}{\cons(a,x)}.$ Now define $$\dropWhile : \bool^A \rightarrow {\lists{A}}^{\lists{A}}$$ by $\dropWhile(p) = \cfoldr(\nil)(\sigma).$

dropWhile :: (List t) => (a -> Bool) -> t a -> t a
dropWhile p = cfoldr nil sigma
where
sigma a x y = if p a then y else cons a x

Because $$\dropWhile$$ is defined as a consuming fold, it can be characterized as the unique solution to a system of functional equations.

Let $$A$$ be a set, with $$p$$ a predicate on $$A$$. Then $$\dropWhile(p)$$ is the unique map $$f : \lists{A} \rightarrow \lists{A}$$ satisfying the following equations for all $$a \in A$$ and $$x \in \lists{A}$$. $\left\{\begin{array}{l} f(\nil) = \nil \\ f(\cons(a,x)) = \bif{p(a)}{f(x)}{\cons(a,x)} \end{array}\right.$

_test_dropWhile_nil :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> Bool)
_test_dropWhile_nil t =
testName "dropWhile(p)(nil) == nil" $\p -> eq (dropWhile p nil) (nil withTypeOf t) _test_dropWhile_cons :: (List t, Equal a, Equal (t a)) => t a -> Test ((a -> Bool) -> a -> t a -> Bool) _test_dropWhile_cons t = testName "dropWhile(p)(cons(a,x)) == if(p(a),dropWhile(p)(x),cons(a,x))"$
\p a x -> eq
(dropWhile p (cons a x))
(if p a then dropWhile p x else cons a x)

Now $$\dropBut$$ is a $$\suffix$$:

Let $$A$$ be a set. For all $$x \in \lists{A}$$ and $$p : A \rightarrow \bool$$, we have $\suffix(\dropWhile(p)(x),x) = \btrue.$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \suffix(\dropWhile(p)(\nil),\nil) \\ & = & \suffix(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-suffix-nil-left} = & \btrue \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$ and let $$a \in A$$. By the inductive hypothesis we have $$\suffix(\dropWhile(p)(x),x)$$, so that $$\suffix(\dropWhile(p)(x),\cons(a,x))$$. Now $\begin{eqnarray*} & & \suffix(\dropWhile(p)(\cons(a,x)),\cons(a,x)) \\ & = & \suffix(\bif{p(a)}{\dropWhile(p)(x)}{\cons(a,x)},\cons(a,x)) \\ & = & \bif{p(a)}{\suffix(\dropWhile(p)(x),\cons(a,x))}{\suffix(\cons(a,x),\cons(a,x))} \\ & = & \bif{p(a)}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \btrue \end{eqnarray*}$ as needed.

_test_dropWhile_suffix :: (List t, Equal a, Equal (t a))
=> t a -> Test ((a -> Bool) -> t a -> Bool)
_test_dropWhile_suffix _ =
testName "suffix(dropWhile(p)(x),x) == true" $\p x -> eq (suffix (dropWhile p x) x) true Like $$\take$$ and $$\drop$$, $$\takeWhile$$ and $$\dropWhile$$ give a kind of $$\cat$$-factorization. Let $$A$$ be a set and $$p : A \rightarrow \bool$$. For all $$x \in \lists{A}$$ we have $x = \cat(\takeWhile(p)(x),\dropWhile(p)(x)).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \cat(\takeWhile(p)(\nil),\dropWhile(p)(\nil)) \\ & = & \cat(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \nil \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \cat(\takeWhile(p)(\cons(a,x)),\dropWhile(p)(\cons(a,x))) \\ & = & \cat(\bif{p(a)}{\cons(a,\takeWhile(p)(x))}{\nil},\bif{p(a)}{\dropWhile(x)}{\cons(a,x)}) \\ & = & \bif{p(a)}{\cat(\cons(a,\takeWhile(p)(x)),\dropWhile(p)(x))}{\cat(\nil,\cons(a,x))} \\ & = & \bif{p(a)}{\cons(a,\cat(\takeWhile(p)(x)),\dropWhile(p)(x))}{\cons(a,x)} \\ & = & \bif{p(a)}{\cons(a,x)}{\cons(a,x)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \cons(a,x) \end{eqnarray*}$ as needed. _test_takeWhile_dropWhile_cat :: (List t, Equal a, Equal (t a)) => t a -> Test ((a -> Bool) -> t a -> Bool) _test_takeWhile_dropWhile_cat _ = testName "cat(takeWhile(p)(x),dropWhile(p)(x)) == x"$
\p x -> eq (cat (takeWhile p x) (dropWhile p x)) x

## Testing

Suite:

_test_takewhile_dropwhile ::
( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t
, TypeName n, Natural n, Show n, Arbitrary n
, Equal (t a), Show (t a), Arbitrary (t a)
) => Int -> Int -> t a -> n -> IO ()
_test_takewhile_dropwhile size cases t k = do
testLabel1 "takeWhile & dropWhile" t

let args = testArgs size cases

runTest args (_test_takeWhile_nil t)
runTest args (_test_takeWhile_cons t)
runTest args (_test_takeWhile_prefix t)
runTest args (_test_takeWhile_sublist t)
runTest args (_test_takeWhile_idempotent t)
runTest args (_test_takeWhile_commutes t)

runTest args (_test_dropWhile_nil t)
runTest args (_test_dropWhile_cons t)
runTest args (_test_dropWhile_suffix t)

runTest args (_test_takeWhile_dropWhile_cat t)

Main:

main_takewhile_dropwhile :: IO ()
main_takewhile_dropwhile = do
_test_takewhile_dropwhile 20 100 (nil :: ConsList Bool)  (zero :: Unary)
_test_takewhile_dropwhile 20 100 (nil :: ConsList Unary) (zero :: Unary)