6-FunctionTypes.tex

\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{5}

\chapter{Function Types}

There is another kind of composition that is at the heart of functional programming. It happens when you pass a function as an argument to another function. The outer function can then use this argument as a pluggable part of its own machinery. It lets you implement, for instance, a generic sorting algorithm that accepts an arbitrary comparison function. 

If we model functions as arrows between objects, then what does it mean to have a function as an argument? 

We need a way to objectify functions in order to define arrows that have an ``object of arrows'' as a source or as a target. A function that takes a function as an argument or returns a function is called a \emph{higher-order} function. Higher-order functions are the work-horses of functional programming.

\subsection{Elimination rule}

The defining quality of a function is that it can be applied to an argument to produce the result. We have defined function application in terms of composition:

\[
 \begin{tikzcd}
 1
 \arrow[d, "x"']
 \arrow[rd, "y"]
 \\
 a
 \arrow[r, "f"']
& b
 \end{tikzcd}
\]
Here $f$ is represented as an arrow from $a$ to $b$, but we would like to be able to replace $f$ with an element of the object of arrows or, as mathematicians call it, the exponential object $b^a$; or as we call it in programming, a function type \hask{a->b}. 

Given an element of $b^a$ and an element of $a$, function application should produce an element of $b$. In other words, given a pair of elements:
\begin{align*}
f &\colon 1 \to b^a \\
x &\colon 1 \to a
\end{align*}
it should produce an element:
\[y \colon 1 \to b \]

Keep in mind that, here, $f$ denotes an element of $b^a$. Previously, it was an arrow from $a$ to $b$.

We know that a pair of elements $(f, x)$ is equivalent to an element of the product $b^a \times a$. We can therefore define function application as a single arrow:
\[\varepsilon_{a b} \colon b^a \times a \to b\]
This way $y$, the result of the application, is defined by this commuting diagram:
\[
 \begin{tikzcd}
 1
 \arrow[d, "{(f, x)}"']
 \arrow[rd, "y"]
 \\
 b^a \times a
 \arrow[r, "\varepsilon_{a b}"']
& b
 \end{tikzcd}
\]
Function application is the \emph{elimination rule} for function type. 

When somebody gives you an element of the function object, the only thing you can do with it is to apply it to an element of the argument type using $\varepsilon$. 

\subsection{Introduction rule}
To complete the definition of the function object, we also need the introduction rule. 

First, suppose that there is a way of constructing a function object $b^a$ from some other object $c$. It means that there is an arrow
\[h \colon c \to b^a\]
We know that we can eliminate the result of $h$ using $\varepsilon_{a b}$, but we have to first multiply it by $a$. So let's first multiply $c$ by $a$ and the use functoriality to map it to $b^a \times a$. 

Functoriality lets us apply a pair of arrows to a product to get another product. Here, the pair of arrows is $(h, id_a)$ (we want to turn $c$ into $b^a$, but we're not interested in modifying $a$)
\[ c \times a \xrightarrow{h \times id_a} b^a \times a \]
We can now follow this with function application to get to $b$
\[ c \times a \xrightarrow{h \times id_a} b^a \times a \xrightarrow{\varepsilon_{a b}} b\]
This composite arrow defines a mapping we'll call $f$:
\[f \colon c \times a \to b\]
Here's the corresponding diagram

\[
 \begin{tikzcd}
 c \times a
 \arrow[d, dashed, "h \times id_a"']
 \arrow[rd, "f"]
 \\
 b^a \times a
 \arrow[r, "\varepsilon"']
& b
 \end{tikzcd}
\]
This commuting diagram tells us that, given an $h$, we can construct an $f$; but we can also demand the converse: Every mapping out, $f \colon c \times a \to b$, should uniquely define a mapping into the exponential, $h \colon c \to b^a$. 

We can use this property, this one-to-one correspondence between two sets of arrows, to define the exponential object. This is the \emph{introduction rule} for the function object $b^a$. 

We've seen that product was defined using its mapping-in property. Function application, on the other hand, is defined as a \emph{mapping out} of a product. 

\subsection{Currying}

There are several ways of looking at this definition. One is to see it as an example of currying. 

So far we've been only considering functions of one argument. This is not a real limitation, since we can always implement a function of two arguments as a (single-argument) function from a product. The $f$ in the definition of the function object is such a function:
\begin{haskell}
f :: (c, a) -> b
\end{haskell}
\hask{h} on the other hand is a function that returns a function:
\begin{haskell}
h :: c -> (a -> b)
\end{haskell}
Currying is the isomorphism between these two sets of arrows. 

This isomorphism can be represented in Haskell by a pair of (higher-order) functions. Since, in Haskell, currying works for any types, these functions are written using type variables---they are \emph{polymorphic}:
\begin{haskell}
curry   :: ((c, a) -> b)   -> (c -> (a -> b))
\end{haskell}

\begin{haskell}
uncurry :: (c -> (a -> b)) -> ((c, a) -> b)
\end{haskell}
In other words, the $h$ in the definition of the function object can be written as 
\[ h = curry\, f \]

Of course, written this way, the types of \hask{curry} and \hask{uncurry} correspond to function objects rather than arrows. This distinction is usually glossed over because there is a one-to-one correspondence between the \emph{elements} of the exponential and the \emph{arrows} that define them. This is easy to see when we replace the arbitrary object $c$ with the terminal object. We get:

\[
 \begin{tikzcd}
 1 \times a
 \arrow[d, dashed, "h \times id_a"']
 \arrow[rd, "f"]
 \\
 b^a \times a
 \arrow[r, "\varepsilon_{a b}"']
& b
 \end{tikzcd}
\]
In this case, $h$ is an element of the object $b^a$, and $f$ is an arrow from $1 \times a$ to $b$. But we know that $1 \times a$ is isomorphic to $a$ so, effectively, $f$ is an arrow from $a$ to $b$. 

Therefore, from now on, we'll call an arrow \hask{->} an arrow $\to$, without making much fuss about it. The correct incantation for this kind of phenomenon is to say that the category is self-enriched.

We can write $\varepsilon_{a b}$ as a Haskell function \hask{apply}:
\begin{haskell}
apply :: (a -> b, a) -> b
apply (f, x) = f x
\end{haskell}
but it's just a syntactic trick: function application is built into the language: \hask{f x} means \hask{f} applied to \hask{x}. Other programming languages require the arguments to a function to be enclosed in parentheses, not so in Haskell. 

Even though defining function application as a separate function may seem redundant, Haskell library does provide an infix operator \hask{$} for that purpose:
\begin{haskell}
($) :: (a -> b) -> a -> b
f $ x = f x
\end{haskell}
The trick, though, is that regular function application binds to the left, e.g., \hask{f x y} is the same as \hask{(f x) y}; but the dollar sign binds to the right, so that 
\begin{haskell}
f  $ g x
\end{haskell}
is the same as \hask{f (g x)}. In the first example, \hask{f} must be a function of (at least) two arguments; in the second, it could be a function of one argument.

In Haskell, currying is ubiquitous. A function of two arguments is almost always written as a function returning a function. Because the function arrow \hask{->} binds to the right, there is no need to parenthesize such types. For instance, the pair constructor has the signature:
\begin{haskell}
pair :: a -> b -> (a, b)
\end{haskell}
You may think of if as a function of two arguments returning a pair, or a function of one argument returning a function of one argument, \hask{b->(a, b)}. This way it's okay to partially apply such a function, the result being another function. For instance, we can define:
\begin{haskell}
pairWithTen :: a -> (Int, a)
pairWithTen = pair 10 -- partial application of pair
\end{haskell}



\subsection{Relation to lambda calculus}

Another way of looking at the definition of the function object is to interpret $c$ as the type of the environment in which $f$ is defined. In that case it's customary to call the environment $\Gamma$. The arrow is interpreted as an expression that uses the variables defined in $\Gamma$. 

Consider a simple example, the expression:
\[a x^2 + b x + c\]
You may think of it as being parameterized by a triple of real numbers $(a, b, c)$ and a variable $x$, taken to be, let's say, a complex number. The triple is an element of a product $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$. This product is the environment $\Gamma$ for our expression. 

The variable $x$ is an element of $\mathbb{C}$. The expression is an arrow from the product $\Gamma \times \mathbb{C}$ to the result type (here, also $\mathbb{C}$)
\[f \colon \Gamma \times \mathbb{C} \to \mathbb{C} \]
This is a mapping-out from a product, so we can use it to construct a function object  $\mathbb{C}^{\mathbb{C}}$ and define a mapping $h \colon \Gamma \to \mathbb{C}^{\mathbb{C}}$
\[
 \begin{tikzcd}
 \Gamma \times \mathbb{C}
 \arrow[d, dashed, "h \times id_{\mathbb{C}}"']
 \arrow[rd, "f"]
 \\
 \mathbb{C}^{\mathbb{C}} \times \mathbb{C}
 \arrow[r, "\varepsilon"']
& \mathbb{C}
 \end{tikzcd}
\]
This new mapping $h$ can be seen as a constructor of the function object. The resulting function object represents all functions from $\mathbb{C}$ to $\mathbb{C}$ that have access to the environment $\Gamma$; that is, to the triple of parameters $(a, b, c)$. 

Corresponding to our original expression $a x^2 + b x + c$ there is a particular function in $\mathbb{C}^{\mathbb{C}}$ that we write as:
\[  \lambda x . \,a x^2 + b x + c \]
or, in Haskell, with the \index{backslash}backslash replacing $\lambda$,
\begin{haskell}
\x -> a * x^2 + b * x + c
\end{haskell}

The arrow $h \colon \Gamma \to \mathbb{C}^{\mathbb{C}}$ is uniquely determined by the arrow $f$. This mapping produces a function that we call $\lambda x . f$.

In general, the defining diagram for the function object becomes:
\[
 \begin{tikzcd}
 \Gamma \times a
 \arrow[d, dashed, "{h \times id_a}"']
 \arrow[rd, "f"]
 \\
 b^a \times a
 \arrow[r, "\varepsilon"']
& b
 \end{tikzcd}
\]

The environment $\Gamma$ that provides free parameters for the expression $f$ is a product of multiple objects representing the types of the parameters (in our example, it was $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$). 

An empty environment is represented by the terminal object $1$, the unit of the product. In that case, $f$ is just an arrow $a \to b$, and $h$ simply picks an element from the function object $b^a$ that corresponds to $f$. 

It's important to keep in mind that, in general, a function object represents functions that depend on external parameters. Such functions are called \index{closure}\emph{closures}. Closures are functions that capture values from their environment.

Here's our example translated to Haskell. Corresponding to $f$ we have an expression:
\begin{haskell}
(a :+ 0) * x * x + (b :+ 0) * x + (c :+ 0)
\end{haskell}
If we use \hask{Double} to approximate $\mathbb{R}$, our environment is a product \hask{(Double, Double, Double)}. The type \hask{Complex} is parameterized by another type---here we used \hask{Double} again:
\begin{haskell}
type C = Complex Double
\end{haskell}
The conversion from \hask{Double} to \hask{C} is done by setting the imaginary part to zero, as in \hask{(a :+ 0)}. 

The corresponding arrow $h$ takes the environment and produces a closure of the type \hask{C -> C}:
\begin{haskell}
h :: (Double, Double, Double) -> (C -> C)
h (a, b, c) = \x -> (a :+ 0) * x * x + (b :+ 0) * x + (c :+ 0)
\end{haskell}

\subsection{Modus ponens}

In logic, the function object corresponds to an implication. An arrow from the terminal object to the function object is the proof of that implication. Function application $\varepsilon$ corresponds to what logicians call \emph{modus ponens}: if you have a proof of the implication $A \Rightarrow B$ and a proof of $A$ then this constitutes the proof of $B$.

\section{Sum and Product Revisited}

When functions gain the same status as elements of other types, we have the tools to directly translate diagrams into code. 

\subsection{Sum types}

Let's start with the definition of the sum.
\[
 \begin{tikzcd}
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && b
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "g"]
 \\
&a + b
\arrow[d, dashed, "h"]
\\
& c
 \end{tikzcd}
\]
We said that the pair of arrows $(f, g)$ uniquely determines the mapping $h$ out of the sum. We can write it concisely using a higher-order function:
\begin{haskell}
h = mapOut (f, g)
\end{haskell}
where:
\begin{haskell}
mapOut :: (a -> c, b -> c) -> (Either a b -> c)
mapOut (f, g) = \aorb -> case aorb of
                         Left  a -> f a
                         Right b -> g b
\end{haskell}
This function takes a pair of functions as an argument and it returns a function. 

First, we pattern-match the pair \hask{(f, g)} to extract \hask{f} and \hask{g}. Then we construct a new function using a lambda. This lambda takes an argument of the type \hask{Either a b}, which we call \hask{aorb}, and does the case analysis on it. If it was constructed using \hask{Left}, we apply \hask{f} to its contents, otherwise we apply \hask{g}. 

Note that the function we are returning is a closure. It captures \hask{f} and \hask{g} from its environment. 

The function we have implemented closely follows the diagram, but it's not written in the usual Haskell style. Haskell programmers prefer to curry functions of multiple arguments. Also, if possible, they prefer to eliminate lambdas. 

Here's the version of the same function taken from the Haskell standard library, where it goes under the name (lower-case) \hask{either}:
\begin{haskell}
either :: (a -> c) -> (b -> c) -> Either a b -> c
either f _ (Left x)     =  f x
either _ g (Right y)    =  g y
\end{haskell}

The other direction of the bijection, from $h$ to the pair $(f, g)$, also follows the arrows of the diagram.
\begin{haskell}
unEither :: (Either a b -> c) -> (a -> c, b -> c)
unEither h = (h . Left, h . Right)
\end{haskell}


\subsection{Product types}

Product types are dually defined by their mapping-in property.
\[
 \begin{tikzcd}
 & c
\arrow[d, dashed, "h"]
 \arrow[ddl, bend right, "f"']
 \arrow[ddr, bend left, "g"]
\\
&a \times b
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
\\
a && b
 \end{tikzcd}
\]
Here's the direct Haskell reading of this diagram
\begin{haskell}
mapIn :: (c -> a, c -> b) -> (c -> (a, b))
mapIn (f, g) = \c -> (f c, g c)
\end{haskell}
And this is the stylized version written in Haskell style as an infix operator \hask{&&&}
\begin{haskell}
(&&&) :: (c -> a) -> (c -> b) -> (c -> (a, b))
(f &&& g) c = (f c, g c)
\end{haskell}
The other direction of the bijection is given by:
\begin{haskell}
fork :: (c -> (a, b)) -> (c -> a, c -> b)
fork h = (fst . h, snd . h)
\end{haskell}
which also closely follows the reading of the diagram.

\subsection{Functoriality revisited}

Both sum and product are functorial, which means that we can apply functions to their contents. We are ready to translate those diagrams into code. 

This is the functoriality of the sum type:

\[
 \begin{tikzcd}
 a
 \arrow[d, "f"]
 \arrow[dr,  bend left, "\text{Left}"']
  && b
 \arrow[d, "g"]
 \arrow[dl, bend right, "\text{Right}"]
 \\
 a'
 \arrow[rd, "\text{Left}"']
&a + b
\arrow[d, dashed, "h"]
& b'
\arrow[ld, "\text{Right}"]
\\
& a' + b'
 \end{tikzcd}
\]
Reading this diagram we can immediately write $h$ using \hask{either}:
\begin{haskell}
h f g = either (Left . f) (Right . g)
\end{haskell}
Or we could expand it and call it \hask{bimap}:
\begin{haskell}
bimap :: (a -> a') -> (b -> b') -> Either a b -> Either a' b'
bimap f g (Left  a) = Left  (f a)
bimap f g (Right b) = Right (g b)
\end{haskell}
Similarly for the product type:
\[
 \begin{tikzcd}
 & a \times b
\arrow[d, dashed, "h"]
 \arrow[dl,  "\text{fst}"']
 \arrow[dr,   "\text{snd}"]
\\
a
\arrow[d, "f"']
&a' \times b'
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
& b
\arrow[d, "g"]
\\
a' && b'
 \end{tikzcd}
\]
$h$ can be written as:
\begin{haskell}
h f g = (f . fst) &&& (g . snd)
\end{haskell}
Or it could be expanded to
\begin{haskell}
bimap :: (a -> a') -> (b -> b') -> (a, b) -> (a', b')
bimap f g (a, b) = (f a, g b)
\end{haskell}
In both cases we call this higher-order function \hask{bimap} since, in Haskell, both the sum and the product are instances of a more general class called \hask{Bifunctor}.

\section{Functoriality of the Function Type}

The function type, or the exponential, is also functorial, but with a twist. We are interested in a mapping from $b^a$ to $b'^{a'}$, where the primed objects are related to the non-primed ones through some arrows---to be determined. 

The exponential is defined by its mapping-in property, so if we're looking for
\[k \colon b^a \to b'^{a'} \]
we should draw the diagram that has $k$ as a mapping into $b'^{a'}$. We get this diagram from the original definition by substituting $b^a$ for $c$ and primed objects for the non-primed ones:

\[
 \begin{tikzcd}
 b^a \times a'
 \arrow[d, dashed, "k \times id_a"']
 \arrow[rd, "g"]
 \\
 b'^{a'} \times a'
 \arrow[r, "\varepsilon"']
& b'
 \end{tikzcd}
\]
The question is: can we find an arrow $g$ to complete this diagram? 
\[g \colon b^a \times a' \to b'\]
If we find such a $g$, it will uniquely define our $k$.

The way to think about this problem is to consider how we would implement $g$. It takes the product $b^a \times a'$ as its argument. Think of it as a pair: an element of the function object from $a$ to $b$ and an element of $a'$. The only thing we can do with the function object is to apply it to something. But $b^a$ requires an argument of type $a$, and all we have at our disposal is $a'$. We can't do anything unless somebody gives us an arrow $a' \to a$. This arrow applied to $a'$ will generate the argument for $b^a$. However, the result of the application is of type $b$, and $g$ is supposed to produce a $b'$. Again, we'll need an arrow $b \to b'$ to complete our assignment. 

This may sound complicated, but the bottom line is that we require two arrows between the primed and non-primed objects. The twist is that the first arrow goes from $a'$ to $a$, which feels backward from the usual functoriality considerations. In order to map $b^a$ to $b'^{a'}$ we need a pair of arrows:
\begin{align*}
f &\colon a' \to a \\
g &\colon b \to b' 
\end{align*}

This is somewhat easier to explain in Haskell. Our goal is to implement a function \hask{a' -> b'}, given a function \hask{h :: a -> b}. 

This new function takes an argument of the type \hask{a'} so, before we can pass it to \hask{h}, we need to convert \hask{a'} to \hask{a}. That's why we need a function \hask{f :: a' -> a}. 

Since \hask{h} produces a \hask{b}, and we want to return a \hask{b'}, we need another function \hask{g :: b -> b'}. All this fits nicely into one higher-order function:
\begin{haskell}
dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b')
dimap f g h = g . h . f
\end{haskell}
Similar to \hask{bimap} being an interface to the typeclass \hask{Bifunctor}, \hask{dimap} is a member of the typeclass \hask{Profunctor}.

\section{Bicartesian Closed Categories}

A category in which both the product and the exponential are defined for any pair of objects, and which has a terminal object, is called \emph{cartesian closed}. The idea is that hom-sets are not something alien to the category in question: the category is ``closed'' under the operation of forming hom-sets.

If the category also has sums (coproducts) and the initial object, it's called \emph{bicartesian closed}. 

This is the minimum structure for modeling programming languages. 

Data types constructed using these operations are called \emph{algebraic data types}. We have addition, multiplication, and exponentiation (but not subtraction or division) of types; with all the familiar laws we know from high-school algebra. They are satisfied up to isomorphism. There is one more algebraic law that we haven't discussed yet.

\subsection{Distributivity}

Multiplication of numbers distributes over addition. Should we expect the same in a bicartesian closed category?
\[b \times a + c \times a \cong (b + c) \times a\]

The left to right mapping is easy to construct, since it's simultaneously a mapping out of a sum and a mapping into a product. We can construct it by gradually decomposing it into simpler mappings. In Haskell, this means implementing a function
\begin{haskell}
dist :: Either (b, a) (c, a) -> (Either b c, a)
\end{haskell}
A mapping out of the sum on the left is given by a pair of arrows:
\begin{align*}
f &\colon b\times a \to (b + c) \times a \\
g &\colon c\times a \to (b + c) \times a 
\end{align*}
\[
 \begin{tikzcd}
 b \times a
 \arrow[dr,  bend left, "\text{Left}"]
 \arrow[ddr, bend right, "f"']
 && c \times a
 \arrow[dl, bend right, "\text{Right}"']
 \arrow[ddl, bend left, "g"]
 \\
& b \times a + c \times a
\arrow[d, dashed, "\text{dist}"]
\\
& (b + c) \times a
 \end{tikzcd}
\]

We write it in Haskell as:
\begin{haskell}
dist = either f g
  where
    f   :: (b, a) -> (Either b c, a)
    g   :: (c, a) -> (Either b c, a)
\end{haskell}
The \index{\hask{where}}\hask{where} clause is used to introduce the definitions of sub-functions.

Now we need to implement $f$ and $g$. They are mappings into the product, so each of them is equivalent to a pair of arrows. For instance, the first one is given by the pair:
\begin{align*}
f' &\colon b \times a \to (b + c) \\
f'' &\colon b \times a \to  a
\end{align*}
\[
 \begin{tikzcd}
 & b \times a
\arrow[d, dashed, "f"]
 \arrow[ddl, bend right, "f'"']
 \arrow[ddr, bend left, "f''"]
\\
& (b + c) \times a
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
\\
b + c && a
 \end{tikzcd}
\]

In Haskell:
\begin{haskell}
    f = f' &&& f''
    f'  :: (b, a) -> Either b c
    f'' :: (b, a) -> a
\end{haskell}
The first arrow can be implemented by projecting the first component $b$ and then using $\text{Left}$ to construct the sum. The second is just the projection $\text{snd}$:
\begin{align*}
 f' &= \text{Left} \circ \text{fst} \\
 f'' &= \text{snd}
\end{align*}
Similarly, we decompose $g$ into a pair $g'$ and $g''$:
\[
 \begin{tikzcd}
 & c \times a
\arrow[d, dashed, "g"]
 \arrow[ddl, bend right, "g'"']
 \arrow[ddr, bend left, "g''"]
\\
& b + c \times a
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
\\
(b + c) && a
 \end{tikzcd}
\]

Combining all these together, we get:
\begin{haskell}
dist = either f g
  where
    f   = f' &&& f''
    f'  = Left . fst
    f'' = snd
    g   = g' &&& g''
    g'  = Right . fst
    g'' = snd
\end{haskell}
These are the type signatures of the helper functions:
\begin{haskell}
    f   :: (b, a) -> (Either b c, a)
    g   :: (c, a) -> (Either b c, a)
    f'  :: (b, a) -> Either b c
    f'' :: (b, a) -> a
    g'  :: (c, a) -> Either b c
    g'' :: (c, a) -> a
\end{haskell}
They can also be inlined to produce this terse form:
\begin{haskell}
dist = either ((Left . fst) &&& snd) ((Right . fst) &&& snd)
\end{haskell}

This style of programming is called \emph{point free} because it omits the arguments (points). For readability reasons, Haskell programmers prefer a more explicit style. The above function would normally be implemented as:
\begin{haskell}
dist (Left  (b, a)) = (Left  b, a)
dist (Right (c, a)) = (Right c, a)
\end{haskell}

Notice that we have only used the definitions of sums and products. The other direction of the isomorphism requires the use of the exponential, so it's only valid in a bicartesian \emph{closed} category. This is not immediately clear from the straightforward Haskell implementation:
\begin{haskell}
undist :: (Either b c, a) -> Either (b, a) (c, a)
undist (Left b, a)  = Left (b, a)
undist (Right c, a) = Right (c, a)
\end{haskell}
but that's because currying is implicit in Haskell. 

Here's the point-free version of this function:
\begin{haskell}
undist = uncurry (either (curry Left) (curry Right))
\end{haskell}
This may not be the most readable implementation, but it underscores the fact that we need the exponential: we use both \hask{curry} and \hask{uncurry} to implement the mapping.

We'll come back to this identity later, when we are equipped with more powerful tools: adjunctions.

\begin{exercise}
Show that:
\[ 2 \times a \cong a + a \]
where $2$ is the Boolean type. Do the proof diagrammatically first, and then implement two Haskell functions witnessing the isomorphism.
\end{exercise}

\end{document}