Take and Drop

Posted on 2017-05-29 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

This page is part of a series on Arithmetic Made Difficult.

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

{-# LANGUAGE NoImplicitPrelude #-}
module TakeAndDrop
  ( take, drop, _test_take_drop, main_take_drop
  ) where

import Testing
import Functions
import Booleans
import Tuples
import DisjointUnions
import NaturalNumbers
import BailoutRecursion
import MaxAndMin
import Lists
import HeadAndTail
import Cat
import Length
import UnfoldN
import Range
import Zip
import PrefixAndSuffix
import Sublist

Today we’ll define two functions, \(\take\) and \(\drop\), that split a list at a given index. For example, \(\take(3)(x)\) should return a list consisting of the first 3 items of \(x\). The biggest question to think about is what \(\take\) should do if \(x\) doesn’t have 3 items to take – should \(\take(3)(-)\) mean take exactly 3 or take at most 3? The simplest interpretation is at most, since with exactly we’d need the return type to encode a failure case. That said, under the at most interpretation, the signature of \(\take\) will be \[\take : \nats \rightarrow {\lists{A}}^{\lists{A}}.\] Usually we’d try to define such a function with a fold, but in this case \(\unfoldN(\ast)\) does exactly what we want.

Essentially, \(\take\) and \(\drop\) compute a kind of “\(\cat\)-factorization” of a list based on index from the left. This is not the only useful such factorization; we will address two others in future posts.

Let \(A\) be a set. Define \(f : \lists{A} \rightarrow 1 + \lists{A} \times A\) by \[f(x) = \left\{ \begin{array}{ll} \lft(\ast) & \mathrm{if}\ x = \nil \\ \rgt((b,a)) & \mathrm{if}\ x = \cons(a,b). \end{array}\right.\] We then define \[\take : \nats \rightarrow {\lists{A}}^{\lists{A}}\] by \[\take(k)(x) = \unfoldN(f)(k,x).\]

In Haskell:

Since \(\take\) is defined as an \(\unfoldN(\ast)\), it can be characterized as the unique solution to a system of functional equations.

Let \(A\) be a set. \(\take\) is the unique map \(f : \nats \rightarrow {\lists{A}}^{\lists{A}}\) satisfying the following equations for all \(n \in \nats\), \(a \in A\), and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\zero,x) = \nil \\ f(\next(n),\nil) = \nil \\ f(\next(n),\cons(a,x)) = \cons(a,f(n,x)) \end{array}\right.\]

\(\take(n)\) is a prefix.

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[\prefix(\take(k,x),x) = \btrue.\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \prefix(\take(k,x),x) \\ & \hyp{k = \zero} = & \prefix(\take(\zero,x),x) \\ & = & \prefix(\nil,x) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#cor-prefix-nil-left} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the result holds for all \(x\) for some \(k\). We now proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \prefix(\take(\next(k),\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-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 result holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \prefix(\take(\next(k),\cons(a,x)),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \prefix(\cons(a,\take(k,x)),\cons(a,x)) \\ & = & \prefix(\take(k,x),x) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-prefix} = & \btrue \end{eqnarray*}\] as needed.

\(\take(n)\) gives a sublist.

Let \(A\) be a set, with \(x \in \lists{A}\) and \(k \in \nats\). Then we have \[\sublist(\take(k,x),x) = \btrue.\]

We have \[\prefix(\take(k,x),x) = \btrue,\] so \[\infix(\take(k,x),x) = \btrue,\] so \[\sublist(\take(k,x),x) = \btrue\] as claimed.

\(\take\) has bounded length:

Let \(A\) be a set, with \(x \in \lists{A}\) and \(k \in \nats\). Then we have \[\length(\take(k,x)) = \nmin(k,\length(x)).\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \length(\take(k,x)) \\ & = & \length(\take(\zero,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-zero} = & \length(\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \zero \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-min-zero-left} = & \nmin(\zero,\length(x)) \\ & = & \nmin(k,\length(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) for some \(k\). We now proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \length(\take(\next(k),x)) \\ & = & \length(\take(\next(k),\nil)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-nil} = & \length(\nil) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \zero \\ & = & \nmin(\next(k),\zero) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \nmin(\next(k),\length(\nil)) \\ & = & \nmin(\next(k),\length(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now we have \[\begin{eqnarray*} & & \length(\take(\next(k),\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \length(\cons(a,\take(k,x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\take(k,x))) \\ & = & \next(\nmin(k,\length(x))) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-next-min-distribute} = & \nmin(\next(k),\next(\length(x))) \\ & = & \nmin(\next(k),\length(\cons(a,x))) \end{eqnarray*}\] as needed.

\(\take\) “distributes over” \(\zip\).

Let \(A\) and \(B\) be sets with \(x \in \lists{A}\), \(y \in \lists{B}\), and \(k \in \nats\). Then \[\zip(\take(k,x),\take(k,y)) = \take(k,\zip(x,y)).\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \zip(\take(k,x),\take(k,y)) \\ & = & \zip(\take(\zero,x),\take(\zero,y)) \\ & = & \zip(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \nil \\ & = & \take(\zero,\zip(x,y)) \\ & = & \take(k,\zip(x,y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) and \(y\) for some \(k\). We consider two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \zip(\take(\next(k),x),\take(\next(k),y)) \\ & = & \zip(\take(\next(k),\nil),\take(\next(k),y)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-nil} = & \zip(\nil,\take(\next(k),y)) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \nil \\ & = & \take(\next(k),\nil) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \take(\next(k),\zip(\nil,y)) \\ & = & \take(\next(k),\zip(x,y)) \end{eqnarray*}\] as needed. Suppose instead that \(x = \cons(a,u)\) for some \(u\). We now consider two possibilities for \(y\). If \(y = \nil\), we have \[\begin{eqnarray*} & & \zip(\take(\next(k),x),\take(\next(k),y)) \\ & = & \zip(\take(\next(k),x),\take(\next(k),\nil)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-nil} = & \zip(\take(\next(k),x),\nil) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#thm-zip-nil-right} = & \nil \\ & = & \take(\next(k),\nil) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#thm-zip-nil-right} = & \take(\next(k),\zip(x,\nil)) \\ & = & \take(\next(k),\zip(x,y)) \end{eqnarray*}\] as needed. Suppose instead that \(y = \cons(b,v)\). Now \[\begin{eqnarray*} & & \zip(\take(\next(k),x),\take(\next(k),y)) \\ & = & \zip(\take(\next(k),\cons(a,u)),\take(\next(k),\cons(b,v))) \\ & = & \cons((a,b),\zip(\take(k,u),\take(k,v))) \\ & = & \cons((a,b),\take(k,\zip(u,v))) \\ & = & \take(\next(k),\cons((a,b),\zip(u,v))) \\ & = & \take(\next(k),\zip(\cons(a,u),\cons(b,v))) \\ & = & \take(\next(k),\zip(x,y)) \end{eqnarray*}\] as needed.

\(\take\) interacts with \(\range\).

For all \(a,b,k \in \nats\), we have \[\take(k,\range(a,b)) = \range(a,\nmin(k,b)).\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \take(k,\range(a,b)) \\ & = & \take(\zero,\range(a,b)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-zero} = & \nil \\ & = & \range(a,\zero) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-min-zero-left} = & \range(a,\nmin(\zero,b)) \\ & = & \range(a,\nmin(k,b)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(a\) and \(b\) for some \(k\). We consider two possibilities for \(b\). If \(b = \zero\), we have \[\begin{eqnarray*} & & \take(\next(k),\range(a,b)) \\ & = & \take(\next(k),\range(a,\zero)) \\ & = & \take(\next(k),\nil) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-nil} = & \nil \\ & = & \range(a,\zero) \\ & = & \range(a,\nmin(\next(k),\zero)) \\ & = & \range(a,\nmin(\next(k),b)) \end{eqnarray*}\] as needed. If \(b = \next(m)\), we have \[\begin{eqnarray*} & & \take(\next(k),\range(a,b)) \\ & = & \take(\next(k),\range(a,\next(m))) \\ & = & \take(\next(k),\cons(a,\range(\next(a),m))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \cons(a,\take(k,\range(\next(a),m))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-range} = & \cons(a,\range(\next(a),\nmin(k,m))) \\ & = & \range(a,\next(\nmin(k,m))) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#thm-next-min-distribute} = & \range(a,\nmin(\next(k),\next(m))) \\ & = & \range(a,\nmin(\next(k),b)) \end{eqnarray*}\] as needed.

\(\take\) is idempotent.

Let \(A\) be a set. For all \(k \in \nats\) and \(x \in \lists{A}\), we have \[\take(k,\take(k,x)) = \take(k,x).\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \take(k,\take(k,x)) \\ & = & \take(\zero,\take(k,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-zero} = & \nil \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-zero} = & \take(\zero,x) \\ & = & \take(k,x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) for some \(k\). We now consider two possibilities. If \(x = \nil\), then \[\begin{eqnarray*} & & \take(\next(k),\take(\next(k),x)) \\ & = & \take(\next(k),\take(\next(k),\nil)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-nil} = & \take(\next(k),\nil) \\ & = & \take(\next(k),x) \end{eqnarray*}\] as needed. If \(x = \cons(a,u)\), we have \[\begin{eqnarray*} & & \take(\next(k),\take(\next(k),x)) \\ & = & \take(\next(k),\take(\next(k),\cons(a,u))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \take(\next(k),\cons(a,\take(k,u))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \cons(a,\take(k,\take(k,u))) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#thm-take-idempotent} = & \cons(a,\take(k,u)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-take-next-cons} = & \take(\next(k),\cons(a,u)) \\ & = & \take(\next(k),x) \end{eqnarray*}\] as needed.

Now for \(\drop\). For this function, \(\unfoldN\) doesn’t have quite the right shape; fundamentally \(\unfoldN\) “builds up” a list from the iterated images of a function, but \(\drop\) needs to “tear down” a list, with it’s natural number argument acting as a countdown. One of our other \(\nats\) recursion operators will work for this – we’ll use bailout recursion for efficiency.

Let \(A\) be a set. Define \(\beta : \nats \times A \rightarrow \bool\) by \[\beta(m,x) = \isnil(x),\] \(\psi : \nats \times \lists{A} \rightarrow \lists{A}\) by \[\psi(m,x) = x,\] and \(\omega : \nats \times \lists{A} \rightarrow \lists{A}\) by \[\omega(k,x) = \tail(x).\] We then define \(\drop : \nats \rightarrow {\lists{A}}^{\lists{A}}\) by \[\drop(k)(x) = \bailrec(\id)(\beta)(\psi)(\omega)(k,x).\]

In Haskell:

Since \(\drop\) is defined in terms of bailout recursion, it can be characterized as the unique solution of a system of functional equations.

Let \(A\) be a set. \(\drop\) is the unique map \(f : \nats \rightarrow {\lists{A}}^{\lists{A}}\) satisfying the following equations for all \(k \in \nats\), \(a \in A\), and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\zero,x) = x \\ f(\next(n),\nil) = \nil \\ f(\next(n),\cons(a,x)) = f(n,x) \end{array}\right.\]

\(\drop\) gives a \(\suffix\).

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[\suffix(\drop(k,x),x) = \btrue.\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \suffix(\drop(k,x),x) \\ & = & \suffix(\drop(\zero,x),x) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-zero} = & \suffix(x,x) \\ & \href{/posts/arithmetic-made-difficult/PrefixAndSuffix.html#thm-suffix-reflexive} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) for some \(k\). We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \suffix(\drop(\next(k),x),x) \\ & = & \suffix(\drop(\next(k),\nil),\nil) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-next-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(\drop(k,x),x) = \btrue\] and note also that \[\suffix(x,\cons(a,x)) = \btrue.\] Since \(\suffix\) is transitive, we have \[\begin{eqnarray*} & & \suffix(\drop(\next(k),\cons(a,x)),\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/TakeAndDrop.html#cor-drop-next-cons} = & \suffix(\drop(k,x),\cons(a,x)) \\ & = & \btrue \end{eqnarray*}\] as needed.

\(\take\) and \(\drop\) give a kind of \(\cat\)-factorization.

Let \(A\) be a set. For all \(x \in \lists{A}\) and \(k \in \nats\), we have \[x = \cat(\take(k,x),\drop(k,x)).\]

We proceed by induction on \(k\). For the base case \(k = \zero\), we have \[\begin{eqnarray*} & & \cat(\take(k,x),\drop(k,x)) \\ & = & \cat(\take(\zero,x),\drop(\zero,x)) \\ & = & \cat(\nil,x) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & x \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) for some \(k\). We proceed by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \cat(\take(\next(k),x),\drop(\next(k),x)) \\ & = & \cat(\take(\next(k),\nil),\drop(\next(k),\nil)) \\ & = & \cat(\nil,\nil) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \nil \\ & = & x \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \cat(\take(\next(k),\cons(a,x)),\drop(\next(k),\cons(a,x))) \\ & = & \cat(\cons(a,\take(k,x)),\drop(k,x)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cons(a,\cat(\take(k,x),\drop(k,x))) \\ & = & \cons(a,x) \end{eqnarray*}\] as needed.

Testing

Suite:

_test_take_drop ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , TypeName n, Natural n, Show n, Arbitrary n, Equal n
  , Equal (t a), Show (t a), Arbitrary (t a)
  , Equal (t b), Show (t b), Arbitrary (t b), Equal (t (Pair a b))
  , Arbitrary (t n), Show (t n), Equal (t n)
  ) => Int -> Int -> t a -> t b -> n -> IO ()
_test_take_drop size cases t u k = do
  testLabel1 "take & drop" t

  let args = testArgs size cases

  runTest args (_test_take_zero t k)
  runTest args (_test_take_next_nil t k)
  runTest args (_test_take_next_cons t k)
  runTest args (_test_take_prefix t k)
  runTest args (_test_take_sublist t k)
  runTest args (_test_take_length t k)
  runTest args (_test_take_zip t u k)
  runTest args (_test_take_range t k)
  runTest args (_test_take_idempotent t k)

  runTest args (_test_drop_zero t k)
  runTest args (_test_drop_next_nil t k)
  runTest args (_test_drop_next_cons t k)
  runTest args (_test_drop_suffix t k)

  runTest args (_test_take_drop_cat t k)

Main:

main_take_drop :: IO ()
main_take_drop = do
  _test_take_drop 50 200 (nil :: ConsList Bool)  (nil :: ConsList Bool)  (zero :: Unary)
  _test_take_drop 50 200 (nil :: ConsList Unary) (nil :: ConsList Unary) (zero :: Unary)
  _test_take_drop 50 200 (nil :: ConsList Bool)  (nil :: ConsList Unary) (zero :: Unary)
  _test_take_drop 50 200 (nil :: ConsList Unary) (nil :: ConsList Bool)  (zero :: Unary)