--- title: Reverse author: nbloomf date: 2017-04-24 tags: arithmetic-made-difficult, literate-haskell slug: rev --- > {-# LANGUAGE NoImplicitPrelude #-} > module Reverse > ( revcat, rev, last, _test_rev, main_rev > ) where > > import Testing > import Flip > import DisjointUnions > import Unary > import Lists > import HeadAndTail > import LeftFold > import Snoc Today we'll define a function that takes a list and reverses the order of its elements; say, to turn $(a,b,c)$ into $(c,b,a)$ and vice versa. First we define a utility as follows. :::::: definition :: []{#def-revcat} Let $A$ be a set. We define a map $\revcat : \lists{A} \times \lists{A} \rightarrow \lists{A}$ by $$\revcat = \foldl(\flip(\cons)).$$ In Haskell: > revcat :: (List t) => t a -> t a -> t a > revcat = foldl (flip cons) :::::::::::::::::::: Since $\revcat$ is defined as a $\foldl(\ast)$, it can be characterized as the unique solution to a system of functional equations. :::::: corollary ::: []{#cor-revcat-nil}[]{#cor-revcat-cons} Let $A$ be a set. Then $\revcat$ is the unique solution $f : \lists{A} \times \lists{A} \rightarrow \lists{A}$ to the following system of equations for all $a \in A$ and $x,y \in \lists{A}$. $$\left\{\begin{array}{l} f(x,\nil) = x \\ f(x,\cons(a,y)) = f(\cons(a,x),y) \end{array}\right.$$ ::: test ::::::::::: > _test_revcat_nil :: (List t, Equal (t a)) > => t a -> Test (t a -> Bool) > _test_revcat_nil z = > testName "revcat(x,nil) == x" $> \x -> > let nil' = nil withTypeOf z in > eq (revcat x nil') x > > > _test_revcat_cons :: (List t, Equal (t a)) > => t a -> Test (a -> t a -> t a -> Bool) > _test_revcat_cons _ = > testName "revcat(x,cons(a,y)) == revcat(cons(a,x),y)"$ > \a x y -> eq (revcat x (cons a y)) (revcat (cons a x) y) :::::::::::::::::::: :::::::::::::::::::: Now $\revcat$ interacts with $\snoc$. :::::: theorem ::::: []{#thm-revcat-snoc-left}[]{#thm-revcat-snoc-right} Let $A$ be a set. For all $a \in A$ and $x,y \in \lists{A}$ we have the following. 1. $\revcat(\snoc(a,x),y) = \snoc(a,\revcat(x,y))$. 2. $\revcat(x,\snoc(a,y)) = \cons(a,\revcat(x,y))$. ::: proof :::::::::: 1. We proceed by list induction on $y$. For the base case $y = \nil$, we have $$\begin{eqnarray*} & & \revcat(\snoc(a,x),\nil) \\ & \href{@rev@#cor-revcat-nil} = & \snoc(a,x) \\ & \href{@rev@#cor-revcat-nil} = & \snoc(a,\revcat(x,\nil)) \end{eqnarray*}$$ as needed. For the inductive step, suppose the equality holds for all $a$ and $x$ for some $y$, and let $b \in A$. Now we have $$\begin{eqnarray*} & & \revcat(\snoc(a,x),\cons(b,y)) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(b,\snoc(a,x)),y) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\snoc(a,x),\cons(b,y)) \\ & \hyp{\revcat(\snoc(a,x),y) = \snoc(a,\revcat(x,y))} = & \snoc(a,\revcat(x,\cons(b,y))) \end{eqnarray*}$$ as needed. 2. We proceed by list induction on $y$. For the base case $y = \nil$, we have $$\begin{eqnarray*} & & \revcat(x,\snoc(a,\nil)) \\ & \href{@snoc@#cor-snoc-nil} = & \revcat(x,\cons(a,\nil)) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(a,x),\nil) \\ & \href{@rev@#cor-revcat-nil} = & \cons(a,x) \\ & \href{@rev@#cor-revcat-nil} = & \cons(a,\revcat(x,\nil)) \end{eqnarray*}$$ as needed. For the inductive step, suppose the equality holds for all $a$ and $x$ for some $y$, and let $b \in A$. Now we have $$\begin{eqnarray*} & & \revcat(x,\snoc(a,\cons(b,y))) \\ & \href{@snoc@#cor-snoc-cons} = & \revcat(x,\cons(b,\snoc(a,y))) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(b,x),\snoc(a,y)) \\ & \href{@rev@#thm-revcat-snoc-right} = & \cons(a,\revcat(\cons(b,x),y)) \\ & \href{@rev@#cor-revcat-cons} = & \cons(a,\revcat(x,\cons(b,y))) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_revcat_snoc_left :: (List t, Equal (t a)) > => t a -> Test (a -> t a -> t a -> Bool) > _test_revcat_snoc_left _ = > testName "revcat(snoc(a,x),y) == snoc(a,revcat(x,y))" $> \a x y -> eq (revcat (snoc a x) y) (snoc a (revcat x y)) > > > _test_revcat_snoc_right :: (List t, Equal (t a)) > => t a -> Test (a -> t a -> t a -> Bool) > _test_revcat_snoc_right _ = > testName "revcat(x,snoc(a,y)) == cons(a,revcat(x,y))"$ > \a x y -> eq (revcat x (snoc a y)) (cons a (revcat x y)) :::::::::::::::::::: :::::::::::::::::::: And we define list reversal in terms of $\revcat$. :::::: definition :: []{#def-rev} Let $A$ be a set. We define $\rev : \lists{A} \rightarrow \lists{A}$ by $$\rev(x) = \revcat(\nil,x).$$ In Haskell: > rev :: (List t) => t a -> t a > rev = revcat nil :::::::::::::::::::: Now $\rev$ is essentially defined here as a left fold, but it can also be characterized as a right fold. :::::: theorem ::::: []{#thm-rev-foldr} We have $$\rev(x) = \foldr(\nil)(\snoc)(x).$$ ::: proof :::::::::: Let $\varphi$ be as defined in the definition of $\rev$. We proceed by list induction on $x$. For the base case $x = \nil$, note that $$\begin{eqnarray*} & & \foldr(\nil)(\snoc)(\nil) \\ & \href{@lists@#def-foldr-nil} = & \nil \\ & \href{@rev@#cor-revcat-nil} = & \revcat(\nil,\nil) \\ & \href{@rev@#def-rev} = & \rev(\nil) \end{eqnarray*}$$ For the inductive step, suppose the equality holds for some $x \in \lists{A}$, and let $a \in A$. Now $$\begin{eqnarray*} & & \foldr(\nil)(\snoc)(\cons(a,x)) \\ & \href{@lists@#def-foldr-cons} = & \snoc(a,\foldr(\nil)(\snoc)(x)) \\ & \href{@rev@#thm-rev-foldr} = & \snoc(a,\rev(x)) \\ & \href{@rev@#def-rev} = & \snoc(a,\revcat(\nil,x)) \\ & \href{@rev@#thm-revcat-snoc-left} = & \revcat(\snoc(a,\nil),x) \\ & \href{@snoc@#cor-snoc-nil} = & \revcat(\cons(a,\nil),x) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\nil,\cons(a,x)) \\ & \href{@rev@#def-rev} = & \rev(\cons(a,x)) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_foldr :: (List t, Equal (t a)) > => t a -> Test (t a -> Bool) > _test_rev_foldr _ = > testName "rev(x) == foldr(nil,snoc)(x)" $> \x -> eq (rev x) (foldr nil snoc x) :::::::::::::::::::: :::::::::::::::::::: Because$\rev$is equivalent to a$\foldr(\ast)(\ast)$, it can be characterized as the unique solution to a system of functional equations. :::::: corollary ::: []{#cor-rev-nil}[]{#cor-rev-cons} Let$A$be a set. Then$\rev$is the unique function$f : \lists{A} \rightarrow \lists{A}$having the property that for all$a \in A$and$x \in \lists{A}$we have $$\left\{\begin{array}{l} f(\nil) = \nil \\ f(\cons(a,x)) = \snoc(a,f(x)). \end{array}\right.$$ ::: test ::::::::::: > _test_rev_nil :: (List t, Equal (t a)) > => t a -> Test Bool > _test_rev_nil z = > testName "rev(nil) == nil"$ > let nil' = nil withTypeOf z in > eq (rev nil') nil' > > > _test_rev_cons :: (List t, Equal (t a)) > => t a -> Test (a -> t a -> Bool) > _test_rev_cons _ = > testName "rev(cons(a,x)) == snoc(a,rev(x))" $> \a x -> eq (rev (cons a x)) (snoc a (rev x)) :::::::::::::::::::: :::::::::::::::::::: Special cases: :::::: theorem ::::: Let$A$be a set. For all$a,b \in A$we have the following. 1.$\rev(\cons(a,\nil)) = \cons(a,\nil)$. 2.$\rev(\cons(a,\cons(b,\nil))) = \cons(b,\cons(a,\nil))$. ::: proof :::::::::: 1. Note that $$\begin{eqnarray*} & & \rev(\cons(a,\nil)) \\ & \href{@rev@#def-rev} = & \revcat(\nil,\cons(a,\nil)) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(a,\nil),\nil) \\ & \href{@rev@#cor-revcat-nil} = & \cons(a,\nil) \end{eqnarray*}$$ as claimed. 2. Note that $$\begin{eqnarray*} & & \rev(\cons(a,\cons(b,\nil))) \\ & \href{@rev@#def-rev} = & \revcat(\nil,\cons(a,\cons(b,\nil))) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(a,\nil),\cons(b,\nil)) \\ & \href{@rev@#cor-revcat-cons} = & \revcat(\cons(b,\cons(a,\nil)),\nil) \\ & \href{@rev@#cor-revcat-nil} = & \cons(b,\cons(a,\nil)) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_single :: (List t, Equal (t a)) > => t a -> Test (a -> Bool) > _test_rev_single z = > testName "rev(cons(a,nil)) == cons(a,nil)"$ > \a -> > let nil' = nil withTypeOf z in > eq (rev (cons a nil')) (cons a nil') > > > _test_rev_double :: (List t, Equal (t a)) > => t a -> Test (a -> a -> Bool) > _test_rev_double z = > testName "rev(cons(a,cons(b,nil))) == cons(b,cons(a,nil))" $> \a b -> > let nil' = nil withTypeOf z in > eq > (rev (cons a (cons b nil'))) > (cons b (cons a nil')) :::::::::::::::::::: :::::::::::::::::::: Now$\rev$and$\snoc$interact: :::::: theorem ::::: []{#thm-rev-snoc} Let$A$be a set. Then for all$a \in A$and$x \in \lists{A}$, we have $$\rev(\snoc(a,x)) = \cons(a,\rev(x)).$$ ::: proof :::::::::: We have $$\begin{eqnarray*} & & \rev(\snoc(a,x)) \\ & \href{@rev@#def-rev} = & \revcat(\nil,\snoc(a,x)) \\ & \href{@rev@#thm-revcat-snoc-right} = & \cons(a,\revcat(\nil,x)) \\ & \href{@rev@#def-rev} = & \cons(a,\rev(x)) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_snoc :: (List t, Equal (t a)) > => t a -> Test (a -> t a -> Bool) > _test_rev_snoc _ = > testName "rev(snoc(a,x)) == cons(a,rev(x))"$ > \a x -> eq (rev (snoc a x)) (cons a (rev x)) :::::::::::::::::::: :::::::::::::::::::: And $\rev$ is an involution. :::::: theorem ::::: []{#thm-rev-involution} Let $A$ be a set. For all $x \in \lists{A}$, we have $\rev(\rev(x)) = x$. ::: proof :::::::::: We proceed by list induction. For the base case $x = \nil$, note that $$\begin{eqnarray*} & & \rev(\rev(\nil)) \\ & \href{@rev@#cor-rev-nil} = & \rev(\nil) \\ & \href{@rev@#cor-rev-nil} = & \nil \end{eqnarray*}$$ as claimed. For the inductive step, suppose the equality holds for some $x \in \lists{A}$, and let $a \in A$. Now $$\begin{eqnarray*} & & \rev(\rev(\cons(a,x))) \\ & \href{@rev@#cor-rev-cons} = & \rev(\snoc(a,\rev(x))) \\ & \href{@rev@#thm-rev-snoc} = & \cons(a,\rev(\rev(x))) \\ & \hyp{\rev(\rev(x)) = x} = & \cons(a,x) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_involution :: (List t, Equal (t a)) > => t a -> Test (t a -> Bool) > _test_rev_involution _ = > testName "rev(rev(x)) == x" $> \x -> eq (rev (rev x)) x :::::::::::::::::::: ::::::::::::::::::::$\rev$preserves$\isnil$and$\beq$. :::::: theorem ::::: []{#thm-isnil-rev}[]{#thm-beq-rev} Let$A$be a set with$x,y \in \lists{A}$. Then we have the following. 1.$\isnil(x) = \isnil(\rev(x))$. 2.$\beq(x,y) = \beq(\rev(x),\rev(y))$. ::: proof :::::::::: 1. We consider two possibilities. If$x = \nil$, we have $$x = \nil = \rev(\nil) = \rev(x),$$ so that$\isnil(x) = \isnil(\rev(x))$as claimed. Suppose instead that$x = \cons(a,u)$for some$u$; then$x = \snoc(b,v)$for some$v$. Now we have $$\begin{eqnarray*} & & \isnil(x) \\ & \let{x = \cons(a,u)} = & \isnil(\cons(a,u)) \\ & \href{@head-tail@#thm-isnil-cons} = & \bfalse \\ & \href{@head-tail@#thm-isnil-cons} = & \isnil(\cons(b,\rev(v))) \\ & \href{@rev@#thm-rev-snoc} = & \isnil(\rev(\snoc(b,v))) \\ & \let{x = \snoc(b,v)} = & \isnil(\rev(x)) \end{eqnarray*}$$ as claimed. 2. We proceed by list induction on$x$. For the base case$x = \nil$, we have $$\begin{eqnarray*} & & \beq(x,y) \\ & \let{x = \nil} = & \beq(\nil,y) \\ & = & \isnil(y) \\ & \href{@rev@#thm-isnil-rev} = & \isnil(\rev(y)) \\ & = & \beq(\nil,\rev(y)) \\ & \href{@rev@#cor-rev-nil} = & \beq(\rev(\nil),\rev(y)) \\ & = & \beq(\rev(x),\rev(y)) \end{eqnarray*}$$ as needed. For the inductive step, suppose the equality holds for all$y$for some$x$and let$a \in A$. We consider two possibilities for$y$. If$y = \nil$, we have $$\begin{eqnarray*} & & \beq(\cons(a,x),y) \\ & \hyp{y = \nil} = & \beq(\cons(a,x),\nil) \\ & = & \isnil(\cons(a,x)) \\ & \href{@rev@#thm-isnil-rev} = & \isnil(\rev(\cons(a,x))) \\ & = & \beq(\rev(\cons(a,x)),\nil) \\ & \href{@rev@#cor-rev-nil} = & \beq(\rev(\cons(a,x)),\rev(\nil)) \\ & \hyp{y = \nil} = & \beq(\rev(\cons(a,x)),\rev(y)) \end{eqnarray*}$$ as needed. Suppose instead that$y = \cons(b,u)$. Using the inductive hypothsis, we have $$\begin{eqnarray*} & & \beq(\cons(a,x),y) \\ & \hyp{y = \cons(b,u)} = & \beq(\cons(a,x),\cons(b,u)) \\ & \href{@lists@#thm-list-eq-cons} = & \band(\beq(a,b),\beq(x,u)) \\ & \href{@rev@#thm-beq-rev} = & \band(\beq(a,b),\beq(\rev(x),\rev(u))) \\ & \href{@snoc@#thm-snoc-eq} = & \beq(\snoc(a,\rev(x)),\snoc(b,\rev(u))) \\ & = & \beq(\rev(\cons(a,x)),\snoc(b,\rev(u))) \\ & \href{@rev@#cor-rev-cons} = & \beq(\rev(\cons(a,x)),\rev(\cons(b,u))) \\ & \hyp{y = \cons(b,u)} = & \beq(\rev(\cons(a,x)),\rev(y)) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_isnil :: (List t, Equal (t a), Equal a) > => t a -> Test (t a -> Bool) > _test_rev_isnil _ = > testName "isnil(rev(x)) == isnil(x)"$ > \x -> eq (isNil (rev x)) (isNil x) > > > _test_rev_eq :: (List t, Equal (t a), Equal a) > => t a -> Test (t a -> t a -> Bool) > _test_rev_eq _ = > testName "eq(rev(x),rev(y)) == eq(x,y)" $> \x y -> eq > (eq (rev x) (rev y)) > (eq x y) :::::::::::::::::::: :::::::::::::::::::: And left fold is a reversed right fold. :::::: theorem ::::: Let$f : B \times A \rightarrow B$. Now $$\foldl(f)(e,x) = \foldr(e)(\flip(f))(\rev(x)).$$ ::: proof :::::::::: We proceed by list induction on$x$. For the base case$x = \nil$, we have $$\begin{eqnarray*} & & \foldl(f)(e,\nil) \\ & \href{@foldl@#def-foldl-nil} = & e \\ & \href{@lists@#def-foldr-nil} = & \foldr(e)(\flip(f))(\nil) \\ & \href{@rev@#cor-rev-nil} = & \foldr(e)(\flip(f))(\rev(\nil)) \end{eqnarray*}$$ as needed. For the inductive step, suppose the equality holds for all$e$for some$x$, and let$a \in A$. Now $$\begin{eqnarray*} & & \foldl(f)(e,\cons(a,x)) \\ & \href{@foldl@#def-foldl-cons} = & \foldl(f)(f(e,a),x) \\ & \hyp{\foldl(f)(w,x) = \foldr(w)(\flip(f))(\rev(x))} = & \foldr(f(e,a))(\flip(f))(\rev(x)) \\ & = & \foldr(\flip(f)(a,e))(\flip(f))(\rev(x)) \\ & = & \foldr(e)(\flip(f))(\snoc(a,\rev(x))) \\ & \href{@rev@#cor-rev-cons} = & \foldr(e)(\flip(f))(\rev(\cons(a,x))) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_rev_foldl :: (List t, Equal (t a), Equal a) > => t a -> Test ((a -> a -> a) -> a -> t a -> Bool) > _test_rev_foldl _ = > testName "foldl(phi)(e,x) == foldr(e,flip(phi))(rev(x))"$ > \phi e x -> > let psi a b = phi b a in > eq (foldl phi e x) (foldr e psi (rev x)) :::::::::::::::::::: :::::::::::::::::::: Note that $\rev$ is a nontrivial involution on $\lists{A}$ -- in particular, that means it is a bijection on $\lists{A}$ other than the identity. When this happens on a type with an induction principle, if we can show that our nontrivial bijection is actually an isomorphism, we get an alternative induction principle (almost) for free. And indeed, $\rev$ is an isomorphism taking $\cons$ to $\snoc$. :::::: theorem ::::: (Snoc Induction.) Let $A$ be a set, and let $f : \lists{A} \rightarrow B$ be a map. Suppose $C \subseteq B$ is a subset with the property that 1. $f(\nil) \in C$ 2. If $f(x) \in C$ and $a \in A$, then $f(\snoc(a,x)) \in C$. Then we have $f(x) \in C$ for all $x \in \lists{A}$. ::: proof :::::::::: This proof is analogous to that of the ordinary list induction principle. Define $T \subseteq \lists{A}$ by $$T = \{ x \in \lists{A} \mid f(x) \in C \}.$$ Note that $\nil \in T$ and if $x \in T$ and $a \in A$ then $\snoc(a,x) \in T$; that is, $(T,\nil,\snoc)$ is an $A$-iterative set. We define $\Theta : \lists{A} \rightarrow T$ to be the fold $$\Theta = \foldr(\nil)(\snoc).$$ Now $\rev : T \rightarrow \lists{A}$ is an $A$-iterative homomorphism since $$\rev(\cons(a,x)) = \snoc(a,\rev(x)).$$ Thus $\rev \circ \Theta$ is an $A$-inductive homomorphism, which by uniqueness must be the identity on $\lists{A}$. If $x \in \lists{A}$, we have $$x = \rev(\rev(x)) = \rev(\id(\rev(x))) = \rev(\rev(\Theta(\rev(x)))) = \Theta(\rev(x)) \in T,$$ so that $T = \lists{A}$ as claimed. :::::::::::::::::::: :::::::::::::::::::: We can define an analog to $\head$ in terms of $\rev$: :::::: definition :: []{#def-last} Let $A$ be a set. We define $\last : \lists{A} \rightarrow 1 + A$ by $$\last(x) = \head(\rev(x)).$$ In Haskell: > last :: (List t) => t a -> Union () a > last = head . rev :::::::::::::::::::: And $\last$ has some nice properties. :::::: theorem ::::: Let $A$ be a set. For all $a,b \in A$ and $x \in \lists{A}$ we have the following. 1. $\last(\nil) = \lft(\ast)$. 2. $\last(\cons(a,\nil)) = \rgt(a)$. 3. $\last(\cons(a,\cons(b,x))) = \last(\cons(b,x))$. ::: proof :::::::::: 1. We have $$\begin{eqnarray*} & & \last(\nil) \\ & \href{@rev@#def-last} = & \head(\rev(\nil)) \\ & \href{@rev@#cor-rev-nil} = & \head(\nil) \\ & \href{@head-tail@#thm-head-nil} = & \lft(\ast) \end{eqnarray*}$$ as claimed. 2. We have $$\begin{eqnarray*} & & \last(\cons(a,\nil)) \\ & \href{@rev@#def-last} = & \head(\rev(\cons(a,\nil))) \\ & \href{@rev@#cor-rev-cons} = & \head(\snoc(a,\rev(\nil))) \\ & \href{@rev@#cor-rev-nil} = & \head(\snoc(a,\nil)) \\ & \href{@snoc@#cor-snoc-nil} = & \head(\cons(a,\nil)) \\ & \href{@head-tail@#thm-head-cons} = & \rgt(a) \end{eqnarray*}$$ as claimed. 3. Note that $$\begin{eqnarray*} & & \last(\cons(a,\cons(b,x))) \\ & \href{@rev@#def-last} = & \head(\rev(\cons(a,\cons(b,x)))) \\ & \href{@rev@#cor-rev-cons} = & \head(\snoc(a,\rev(\cons(b,x)))) \\ & \href{@rev@#cor-rev-cons} = & \head(\snoc(a,\snoc(b,\rev(x)))) \\ & \href{@snoc@#thm-snoc-head} = & \head(\snoc(b,\rev(x))) \\ & \href{@rev@#cor-rev-cons} = & \head(\rev(\cons(b,x))) \\ & \href{@rev@#def-last} = & \last(\cons(b,x)) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _test_last_nil :: (List t, Equal (t a), Equal a) > => t a -> Test Bool > _test_last_nil l = > testName "eq(last(nil),lft(*))" $> eq (last (nil withTypeOf l)) (lft ()) > > > _test_last_one :: (List t, Equal (t a), Equal a) > => t a -> Test (a -> Bool) > _test_last_one l = > testName "eq(last(cons(a,xs)),rgt(a))"$ > \a -> eq (last (cons a (nil withTypeOf l))) (rgt a) > > > _test_cons_last :: (List t, Equal (t a), Equal a) > => t a -> Test (a -> a -> t a -> Bool) > _test_cons_last _ = > testName "eq(last(cons(a,cons(b,xs))),last(cons(b,xs)))" \$ > \a b x -> eq (last (cons a (cons b x))) (last (cons b x)) :::::::::::::::::::: :::::::::::::::::::: Testing ------- Suite: > _test_rev :: > ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a > , TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a) > ) => Int -> Int -> t a -> IO () > _test_rev size cases t = do > testLabel1 "rev" t > let args = testArgs size cases > > runTest args (_test_revcat_nil t) > runTest args (_test_revcat_cons t) > runTest args (_test_revcat_snoc_left t) > runTest args (_test_revcat_snoc_right t) > runTest args (_test_rev_foldr t) > runTest args (_test_rev_nil t) > runTest args (_test_rev_cons t) > runTest args (_test_rev_single t) > runTest args (_test_rev_double t) > runTest args (_test_rev_snoc t) > runTest args (_test_rev_involution t) > runTest args (_test_rev_isnil t) > runTest args (_test_rev_eq t) > runTest args (_test_rev_foldl t) > runTest args (_test_last_nil t) > runTest args (_test_last_one t) > runTest args (_test_cons_last t) Main: > main_rev :: IO () > main_rev = do > _test_rev 20 100 (nil :: ConsList Bool) > _test_rev 20 100 (nil :: ConsList Unary)