# Snoc

Posted on 2018-01-05 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module Snoc (
snoc, _test_snoc, main_snoc
) where

import Testing
import Booleans
import And
import Unary
import Lists
import LeftFold

We’ve defined a set $$\lists{A}$$ with a special element $$\nil$$, a map $$\cons : A \times \lists{A} \rightarrow \lists{A}$$, and a universal map $$\foldr(\ast)(\ast)$$. As you might guess we’ll be thinking of the elements of $$\lists{A}$$ as finite lists, and they will form a simple kind of data structure.

The $$\cons$$ function attaches a new item to the “beginning” of a list; we want an analogous function that attaches items to the “end”.

First let’s tackle adding items to the end of a list; traditionally this operator is called $$\snoc$$ as a bad pun on “reverse $$\cons$$”. Now the signature of $$\snoc$$ should be something like $\snoc : A \times \lists{A} \rightarrow \lists{A},$ and $$\foldr(e)(\varphi)$$ can be used to build a map $$\lists{A} \rightarrow \lists{A}$$, provided $$e$$ is in $$\lists{A}$$ and $$\varphi : A \times \lists{A} \rightarrow \lists{A}$$. Considering the behavior we want $$\snoc$$ to have, we define the following.

Let $$A$$ be a set. We now define a map $$\snoc : A \times \lists{A} \rightarrow \lists{A}$$ by $\snoc(a,x) = \foldr(\cons(a,\nil))(\cons)(x).$

snoc :: (List t) => a -> t a -> t a
snoc a = foldr (cons a nil) cons

Because $$\snoc$$ is defined directly as a fold, it is the unique solution to a system of functional equations.

Let $$A$$ be a set. Then $$\snoc$$ is the unique function $$f : A \times \lists{A} \rightarrow \lists{A}$$ with the property that for all $$a,b \in A$$ and $$x \in \lists{A}$$ we have $\left\{ \begin{array}{ll} f(a,\nil) = \cons(a,\nil) \\ f(a,\cons(b,x)) = \cons(b,f(a,x)). \end{array} \right.$

_test_snoc_nil :: (List t, Equal (t a))
=> t a -> Test (a -> Bool)
_test_snoc_nil z =
testName "snoc(a,nil) == cons(a,nil)" $\a -> let nil' = nil withTypeOf z in eq (snoc a nil') (cons a nil') _test_snoc_cons :: (List t, Equal (t a)) => t a -> Test (a -> a -> t a -> Bool) _test_snoc_cons _ = testName "snoc(a,cons(b,x)) == cons(b,snoc(a,x))"$
\a b x -> eq (snoc a (cons b x)) (cons b (snoc a x))

Now $$\snoc$$ interacts with $$\foldr(\ast)(\ast)$$.

Let $$A$$ and $$B$$ be sets with $$e \in B$$ and $$\varphi : A \times B \rightarrow B$$. Then for all $$a \in A$$ and $$x \in \lists{A}$$ we have $\foldr(e)(\varphi)(\snoc(a,x)) = \foldr(\varphi(a,e))(\varphi)(x).$

We proceed by list induction. For the base case $$x = \nil$$, note that $\begin{eqnarray*} & & \foldr(e)(\varphi)(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldr(e)(\varphi)(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varphi(a,e) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(\varphi(a,e))(\varphi)(\nil) \end{eqnarray*}$ as claimed. Suppose now that the equality holds for some $$x \in \lists{A}$$. Now $\begin{eqnarray*} & & \foldr(e)(\varphi)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldr(e)(\varphi)(\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(b,\foldr(e)(\varphi)(\snoc(a,x))) \\ & \hyp{\foldr(e)(\varphi)(\snoc(a,x)) = \foldr(\varphi(a,e))(\varphi)(x)} = & \varphi(b,\foldr(\varphi(a,e))(\varphi)(x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(\varphi(a,e))(\varphi)(\cons(b,x)) \end{eqnarray*}$ as needed.

We can perform case analysis on lists with $$\snoc$$.

Let $$A$$ be a set and let $$x \in \lists{A}$$. Then either $$x = \nil$$ or $$x = \snoc(a,w)$$ for some $$w \in \lists{A}$$ and $$a \in A$$.

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, the conclusion holds trivially. For the inductive step, suppose the conclusion holds for some $$x$$ and let $$a \in A$$. Now $$\cons(a,x) \neq \nil$$. We have two cases for $$x$$; if $$x = \nil$$, then $\cons(a,x) = \cons(a,\nil) = \snoc(a,\nil)$ as needed. Suppose instead that $$x \neq \nil$$; by the inductive hypothesis we have $$x = \snoc(b,w)$$ for some $$b \in A$$ and $$w \in \lists{A}$$. Then we have $\begin{eqnarray*} & & \cons(a,x) \\ & \hyp{x = \snoc(b,w)} = & \cons(a,\snoc(b,w)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(b,\cons(a,w)) \end{eqnarray*}$ as claimed.

Also, $$\snoc$$ interacts with $$\beq$$.

Let $$A$$ be a set with $$a,b \in A$$ and $$x,y \in \lists{A}$$. Then $\beq(\snoc(a,x),\snoc(b,y)) = \band(\beq(a,b),\beq(x,y)).$

We proceed by list induction on $$x$$. For the base case, set $$x = \nil$$. We consider two possibilities for $$y$$. If $$y = \nil$$, we have $\begin{eqnarray*} & & \beq(\snoc(a,\nil),\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\snoc(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,b),\beq(\nil,\nil)) \end{eqnarray*}$ as needed. If $$y = \cons(c,u)$$, we have $\begin{eqnarray*} & & \beq(\snoc(a,\nil),\snoc(b,y)) \\ & \let{y = \cons(c,u)} = & \beq(\snoc(a,\nil),\snoc(b,\cons(c,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \beq(\snoc(a,\nil),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \beq(\cons(a,\nil),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,c),\beq(\nil,\snoc(b,u))) \\ & = & \band(\beq(a,c),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \band(\beq(a,b),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-nil} = & \band(\beq(a,b),\beq(\nil,\cons(c,u))) \\ & \let{y = \cons(c,u)} = & \band(\beq(a,b),\beq(\nil,y)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$a$$, $$b$$, and $$y$$ for some $$x$$ and let $$d \in A$$. We again consider two possibilities for $$y$$. If $$y = \nil$$, we have $\begin{eqnarray*} & & \beq(\snoc(a,\cons(d,x)),\snoc(b,y)) \\ & = & \beq(\snoc(a,\cons(d,x)),\snoc(b,\nil)) \\ & = & \beq(\cons(d,\snoc(a,x)),\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(d,b),\beq(\snoc(a,x),\nil)) \\ & = & \band(\beq(d,b),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \band(\beq(a,b),\bfalse) \\ & = & \band(\beq(a,b),\beq(\cons(d,x),\nil)) \\ & = & \band(\beq(a,b),\beq(\cons(d,x),y)) \end{eqnarray*}$ as needed. Suppose instead that $$y = \cons(c,u)$$. Using the inductive hypothesis, we have $\begin{eqnarray*} & & \beq(\snoc(a,\cons(d,x)),\snoc(b,y)) \\ & \hyp{y = \cons(c,u)} = & \beq(\snoc(a,\cons(d,x)),\snoc(b,\cons(c,u))) \\ & = & \beq(\cons(d,\snoc(a,x)),\snoc(b,\cons(c,u))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \beq(\cons(d,\snoc(a,x)),\cons(c,\snoc(b,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(d,c),\beq(\snoc(a,x),\snoc(b,u))) \\ & \hyp{\beq(\snoc(a,x),\snoc(b,u)) = \band(\beq(a,b),\beq(x,u))} = & \band(\beq(d,c),\band(\beq(a,b),\beq(x,u))) \\ & = & \band(\band(\beq(d,c),\beq(a,b)),\beq(x,u)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(\band(\beq(a,b),\beq(d,c)),\beq(x,u)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-associative} = & \band(\beq(a,b),\band(\beq(d,c),\beq(x,u))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#thm-list-eq-cons} = & \band(\beq(a,b),\beq(\cons(d,x),\cons(c,u))) \\ & \let{y = \cons(c,u)} = & \band(\beq(a,b),\beq(\cons(d,x),y)) \end{eqnarray*}$ as needed.

_test_snoc_eq :: (List t, Equal (t a), Equal a)
=> t a -> Test (a -> a -> t a -> t a -> Bool)
_test_snoc_eq _ =
testName "eq(snoc(a,x),snoc(b,y)) iff and(eq(a,b),eq(x,y))" $\a b x y -> eq (eq (snoc a x) (snoc b y)) (and (eq a b) (eq x y)) Now $$\foldl(\ast)$$ interacts with $$\snoc$$. We have $\foldl(\varphi)(e,\snoc(a,x)) = \varphi(\foldl(\varphi)(e,x),a).$ We proceed by list induction on $$x$$. For the base case we have $\begin{eqnarray*} & & \foldl(\varphi)(e,\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldl(\varphi)(e,\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\varphi)(\varphi(e,a),\nil) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \varphi(e,a) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \varphi(\foldl(\varphi)(e,\nil),a) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$e$$ and $$a$$ for some $$x$$, and let $$b \in A$$. Then we have $\begin{eqnarray*} & & \foldl(\varphi)(e,\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldl(\varphi)(e,\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\varphi)(\varphi(e,b),\snoc(a,x)) \\ & \hyp{\foldl(\varphi)(c,\snoc(a,x)) = \varphi(\foldl(\varphi)(c,x),a)} = & \varphi(\foldl(\varphi)(\varphi(e,b),x),a) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \varphi(\foldl(\varphi)(e,\cons(b,x)),a) \end{eqnarray*}$ as needed. _test_snoc_foldl :: (List t, Equal (t a), Equal a) => t a -> Test ((a -> a -> a) -> a -> a -> t a -> Bool) _test_snoc_foldl _ = testName "foldl(phi)(e,snoc(a,x)) == phi(foldl(phi)(e,x),a)"$
\phi e a x -> eq
(foldl phi e (snoc a x))
(phi (foldl phi e x) a)

And $$\snoc$$ is not $$\nil$$.

We have $\isnil(\snoc(a,x)) = \bfalse.$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \isnil(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \isnil(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$a$$ for some $$x$$, and let $$b \in A$$; we have $\begin{eqnarray*} & & \isnil(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \isnil(\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \end{eqnarray*}$ as needed.

_test_snoc_isnil :: (List t, Equal (t a), Equal a)
=> t a -> Test (a -> t a -> Bool)
_test_snoc_isnil _ =
testName "eq(isnil(snoc(a,x)),false)" $\a x -> eq (isNil (snoc a x)) false Many interesting list functions can be implemented in terms of either $$\foldr(\ast)(\ast)$$ or $$\foldl(\ast)$$, and depending on the function, one may be preferable over the other. A useful question to ask is this: under what circumstances is a given right fold equivalent to a left fold? The next result provides a sufficient condition. Let $$A$$ and $$B$$ be sets, and suppose $$\varphi : A \times B \rightarrow B$$ has the property that $\varphi(a,\varphi(b,e)) = \varphi(b,\varphi(a,e))$ for all $$a,b \in A$$ and $$e \in B$$. Letting $$\psi : B \times A \rightarrow B$$ be given by $$\psi(b,a) = \varphi(a,b)$$, we have the following. 1. $$\foldl(\psi)(e,\snoc(a,x)) = \foldl(\psi)(e,\cons(a,x))$$. 2. $$\foldr(e)(\varphi)(x) = \foldl(\psi)(e,x)$$. 1. We proceed by list induction on $$x$$. For the base case $$x = \nil$$ we have $\begin{eqnarray*} & & \foldl(\psi)(e)(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \foldl(\psi)(e)(\snoc(a,\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$e$$ and $$a$$ for some $$x$$ and let $$b \in A$$. Now $\begin{eqnarray*} & & \foldl(\psi)(e,\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \foldl(\psi)(e,\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(e,b),\snoc(a,x)) \\ & \hyp{\foldl(\psi)(w)(\cons(a,x)) = \foldl(\psi)(w)(\snoc(a,x))} = & \foldl(\psi)(\psi(e,b),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(\psi(e,b),a),x) \\ & = & \foldl(\psi)(\varphi(a,\varphi(b,e)),x) \\ & = & \foldl(\psi)(\varphi(b,\varphi(a,e)),x) \\ & = & \foldl(\psi)(\psi(\psi(e,a),b),x) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(\psi(e,a),\cons(b,x)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-cons} = & \foldl(\psi)(e,\cons(a,\cons(b,x))) \end{eqnarray*}$ as needed. 2. We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \foldr(e)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & e \\ & = & \foldl(\psi)(e,\nil) \end{eqnarray*}$ as needed. If $$x = \cons(a,\nil)$$, we have $\begin{eqnarray*} & & \foldr(e)(\varphi)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \varphi(a,\foldr(e)(\varphi)(x)) \\ & = & \varphi(a,\foldl(\psi)(e,x)) \\ & = & \psi(\foldl(\psi)(e,x),a) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-foldl} = & \foldl(\psi)(e,\snoc(a,x)) \\ & = & \foldl(\psi)(e,\cons(a,x)) \end{eqnarray*}$ as needed. $$\snoc$$ interacts with $$\head$$. Let $$A$$ be a set. For all $$a,b \in A$$ and $$x \in \lists{A}$$ we have $\head(\snoc(a,\snoc(b,x))) = \head(\snoc(b,x)).$ We consider two possibilities for $$x$$. If $$x = \nil$$, we have $\begin{eqnarray*} & & \head(\snoc(a,\snoc(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \head(\snoc(a,\cons(b,\nil))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\cons(b,\snoc(a,\nil))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(b) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \head(\cons(b,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \head(\snoc(b,\nil)) \end{eqnarray*}$ and if $$x = \cons(c,y)$$ we have $\begin{eqnarray*} & & \head(\snoc(a,\snoc(b,x))) \\ & \let{x = \cons(c,y)} = & \head(\snoc(a,\snoc(b,\cons(c,y)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\snoc(a,\cons(c,\snoc(b,y)))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\cons(c,\snoc(a,\snoc(b,y)))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(c) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \head(\cons(c,\snoc(b,y))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \head(\snoc(b,\cons(c,y))) \\ & \let{x = \cons(c,y)} = & \head(\snoc(b,x)) \end{eqnarray*}$ as needed. _test_snoc_head :: (List t, Equal (t a), Equal a) => t a -> Test (a -> a -> t a -> Bool) _test_snoc_head _ = testName "eq(head(snoc(a,snoc(b,xs))),head(snoc(b,xs)))"$
\a b x -> eq (head (snoc a (snoc b x))) (head (snoc b x))

## Testing

Suite:

_test_snoc ::
( 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_snoc size cases t = do
testLabel1 "snoc" t

let args = testArgs size cases

runTest args (_test_snoc_nil t)
runTest args (_test_snoc_cons t)
runTest args (_test_snoc_eq t)
runTest args (_test_snoc_foldl t)
runTest args (_test_snoc_isnil t)
runTest args (_test_snoc_head t)

Main:

main_snoc :: IO ()
main_snoc = do
_test_snoc 20 100 (nil :: ConsList Bool)
_test_snoc 20 100 (nil :: ConsList Unary)