DaoFP Chapter 15 Solutions

solution

Solutions to the exercises of DaoFP, Chapter 15: DaoFP Chapter 15 Exercises. Index: Map of Content.

Solution 15.1.1

program — Exercise 15.1.1

The second identity is $\epsilon \circ L\cdot L\circ \eta ={\mathrm{id}}_L$: reading bottom-up, $L\stackrel{L\eta }{\to }LRL\stackrel{\epsilon L}{\to }L$. As a string diagram: an $L$-string that dips into a cup ($\eta$, creating $RL$ to its right) and then rises through a cap ($\epsilon$, annihilating $LR$) — a zigzag that pulls straight to the plain $L$-string. When $L$ is a Haskell endofunctor: triangle2 :: forall x. L x -> L x; triangle2 = counit . fmap unit, which must equal id (here fmap is $L$‘s, instantiating $L\circ \eta$; counit at L x is $\epsilon \circ L$).

Sources: DaoFP Exercise 15.1.1.

Solution 15.2.1

proof — Exercise 15.2.1

Replace every $T$-string by the parallel pair $LR$. Then $\eta$ is a cup and $\mu =R\epsilon L$ is a cap between the inner $R$ and $L$ of two adjacent $LR$ pairs. Left unit $\mu \circ (\eta T)$: a cup on the left of an $LR$ pair followed by the cap joining the cup’s $R$ with the pair’s $L$ — the $R$… $L$ zigzag straightens by the first triangle identity, leaving $LR=T$. Right unit: symmetric, using the second triangle identity. Associativity: three $LR$ pairs with two caps; applying the caps left-first or right-first yields the same diagram since caps on disjoint strings can slide past each other (interchange law).

Sources: DaoFP Exercise 15.2.1.

Solution 15.3.1

proof — Exercise 15.3.1

$Fa=(1+a,\mathsf{Left})$ and $U$ forgets the point, so $UFa=1+a=$ Maybe a. The unit ${\eta }_a:a\to 1+a$ is $\mathsf{Right}$ (Just); the counit at a pointed object $(b,p)$ is the point-preserving map $[p,{\mathrm{id}}_b]:1+b\to b$; whiskering gives ${\mu }_a=[\mathsf{Left},\mathrm{id}]:1+(1+a)\to 1+a$, i.e. join Nothing = Nothing; join (Just m) = m — exactly the Maybe monad. The adjunction: a point-preserving map $(1+a,\mathsf{Left})\to (b,p)$ is determined by its restriction to $a$, so $1/\mathcal{C}(Fa,(b,p))\cong \mathcal{C}(a,b)$.

Sources: DaoFP Exercise 15.3.1.