Flip

Posted on 2018-02-17 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 Flip (
  flip, flip2, flip3, flip4, flip5, _test_flip, main_flip
) where

import Testing
import Functions

It turns out that equational proofs are much simpler to state and verify if we define new functions in the so-called pointfree style. A pointfree function definition is one that does not refer to its arguments explicitly; for example, suppose we have two functions \(f : A \rightarrow B\) and \(g : B \rightarrow C\), and have defined a new function \(h : A \rightarrow C\) by \[h(x) = g(f(x)).\] Of course this definition is equivalent to \[h(x) = \compose(g)(f)(x).\] But now the rightmost argument, \(x\), can be omitted, leaving \[h = \compose(g)(f).\] This final statement is written in the pointfree style. We’ll see later that definitions will cooperate better with equational reasoning if they are in pointfree form. To make this work, we’ll need a stable of operators for manipulating functions, like \(\compose\) in the above example. In all cases the goal will be to move function arguments around; for instance, \(\compose\) lets us move a rightmost argument “up” one level of parentheses.

In this post we’ll define a family of operators that rearrange the arguments of a multi-argument function. The first example is \(\flip\), which flips the arguments of a two-argument function.

Let \(A\), \(B\), and \(C\) be sets. Given \(f : A \rightarrow B \rightarrow C\), we define \(\flip(f) : B \rightarrow A \rightarrow C\) by \[\flip(f)(b)(a) = f(a)(b).\]

In Haskell:

\(\flip\) is an involution.

Let \(A\), \(B\), and \(C\) be sets. For all \(f : A \rightarrow B \rightarrow C\), we have \[\flip(\flip(f)) = f.\]

Let \(a \in A\) and \(b \in B\). Then we have \[\begin{eqnarray*} & & \flip(\flip(f))(a)(b) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & \flip(f)(b)(a) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & f(a)(b) \end{eqnarray*}\] as needed.

Ostensibly, \(\flip\) acts on functions of two arguments. But since the return type of such a function can be another function, a better way to think of \(\flip\) is that it flips the first two arguments of a multi-argument function.

Let \(f : A \rightarrow B \rightarrow C \rightarrow D\). Then we have \[\flip(f)(b)(a)(c)(d) = f(a)(b)(c)(d).\]

Note that \[\begin{eqnarray*} & & \flip(f)(b)(a)(c) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & f(a)(b)(c) \end{eqnarray*}\]

Okay- what about more general permutations of function arguments? Let’s start with flipping the second and third.

Let \(A\), \(B\), \(C\), and \(D\) be sets. Given \(f : A \rightarrow B \rightarrow C \rightarrow D\), we define \(\flipB(f) : A \rightarrow C \rightarrow B \rightarrow D\) by \[\flipB = \compose(\flip).\]

In Haskell:

Now \(\flipB\) permutes function arguments.

Let \(f : A \rightarrow B \rightarrow C \rightarrow D\). Then \[\flipB(f)(a)(c)(b) = f(a)(b)(c).\]

We have \[\begin{eqnarray*} & & \flipB(f)(a)(c)(b) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip2} = & \compose(\flip)(f)(a)(c)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \flip(f(a))(c)(b) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & f(a)(b)(c) \end{eqnarray*}\] as claimed.

And we can flip the third and fourth arguments.

Let \(A\), \(B\), \(C\), \(D\), and \(E\) be sets. We define \[\flipC : (A \rightarrow B \rightarrow C \rightarrow D \rightarrow E) \rightarrow A \rightarrow B \rightarrow D \rightarrow C \rightarrow E\] by \[\flipC = \compose(\compose(\flip)).\]

In Haskell:

\(\flipC\) does the thing:

Let \(f : A \rightarrow B \rightarrow C \rightarrow D \rightarrow E\). Then \[\flipC(f)(a)(b)(d)(c) = f(a)(b)(c)(d).\]

We have \[\begin{eqnarray*} & & \flipC(f)(a)(b)(d)(c) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip3} = & \compose(\compose(\flip))(f)(a)(b)(d)(c) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\flip)(f(a))(b)(d)(c) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \flip(f(a)(b))(d)(c) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & f(a)(b)(c)(d) \end{eqnarray*}\] as claimed.

We’ll look at two more examples, to see the pattern emerging.

We define \(\flipD : (A \rightarrow B \rightarrow C \rightarrow D \rightarrow E \rightarrow F) \rightarrow A \rightarrow B \rightarrow C \rightarrow E \rightarrow D \rightarrow F\) by \[\flipD = \compose(\compose(\compose(\flip))).\]

In Haskell:

And:

Let \(f : A \rightarrow B \rightarrow C \rightarrow D \rightarrow E \rightarrow F\). Then \[\flipD(f)(a)(b)(c)(e)(d) = f(a)(b)(c)(d)(e).\]

We have \[\begin{eqnarray*} & & \flipD(f)(a)(b)(c)(e)(d) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip4} = & \compose(\compose(\compose(\flip)))(f)(a)(b)(c)(e)(d) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\compose(\flip))(f(a))(b)(c)(e)(d) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\flip)(f(a)(b))(c)(e)(d) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \flip(f(a)(b)(c))(e)(d) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & f(a)(b)(c)(d)(e) \end{eqnarray*}\] as claimed.

One more.

We define \[\flipE : (A \rightarrow B \rightarrow C \rightarrow D \rightarrow E \rightarrow F \rightarrow G) \rightarrow A \rightarrow B \rightarrow C \rightarrow D \rightarrow F \rightarrow E \rightarrow G\] by \[\flipE = \compose(\compose(\compose(\compose(\flip)))).\]

In Haskell:

And:

Let \(w : A \rightarrow B \rightarrow C \rightarrow D \rightarrow E \rightarrow F \rightarrow G\). Then \[\flipE(w)(a)(b)(c)(d)(f)(e) = w(a)(b)(c)(d)(e)(f).\]

We have \[\begin{eqnarray*} & & \flipE(w)(a)(b)(c)(d)(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip5} = & \compose(\compose(\compose(\compose(\flip))))(w)(a)(b)(c)(d)(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\compose(\compose(\flip)))(w(a))(b)(c)(d)(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\compose(\flip))(w(a)(b))(c)(d)(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(\flip)(w(a)(b)(c))(d)(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \flip(w(a)(b)(c)(d))(f)(e) \\ & \href{/posts/arithmetic-made-difficult/Flip.html#def-flip} = & w(a)(b)(c)(d)(e)(f) \end{eqnarray*}\] as claimed.

Well that’s neat. This pattern continues, and we can define an operator that flips the \(n\)th and \((n+1)\)th argument, for any \(n\), using just \(\compose\) and \(\flip\). And it turns out that this is enough to generate arbitrary permutations of the arguments of any function, by composing the flip operators in the right order. We won’t prove this in full generality here (not yet, anyway).

Testing

Suite:

_test_flip ::
  ( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a
  , Equal b, Show b, Arbitrary b, CoArbitrary b, TypeName b
  , Equal c, Show c, Arbitrary c, CoArbitrary c, TypeName c
  , Equal d, Show d, Arbitrary d, CoArbitrary d, TypeName d
  , Equal e, Show e, Arbitrary e, CoArbitrary e, TypeName e
  , Equal f, Show f, Arbitrary f, CoArbitrary f, TypeName f
  , Equal g, Show g, Arbitrary g, CoArbitrary g, TypeName g
  ) => Int -> Int -> a -> b -> c -> d -> e -> f -> g -> IO ()

_test_flip size cases a b c d e f g = do
  testLabel0 "flip"
  let args = testArgs size cases

  runTest args (_test_flip_involution a b c)
  runTest args (_test_flip_3 a b c d)
  runTest args (_test_flip2 a b c d)
  runTest args (_test_flip3 a b c d e)
  runTest args (_test_flip4 a b c d e f)
  runTest args (_test_flip5 a b c d e f g)

Main:

main_flip :: IO ()
main_flip = do
  _test_flip 1 1 () () () () () () ()