Hit! You sunk my Adjunction!
Today we'll be looking into Kmett's | |
[adjunctions](http://hackage.haskell.org/package/adjunctions) library, | |
particularly the meat of the library in Data.Functor.Adjunction. | |
This post is a literate haskell file, which means you can load it right up in | |
ghci and play around with it! Like any good haskell file we need half a dozen | |
language pragmas and imports before we get started. | |
> {-# language DeriveFunctor #-} | |
> {-# language TypeFamilies #-} | |
> {-# language MultiParamTypeClasses #-} | |
> {-# language InstanceSigs #-} | |
> {-# language FlexibleContexts #-} | |
> module Battleship where | |
> import Data.Functor (void) | |
> import Data.Functor.Adjunction | |
> import Data.Functor.Rep | |
> import Data.Distributive | |
> import Control.Arrow ((&&&)) | |
I've been struggling to understand this library for a little while | |
now and have been poking at it from different angles trying to gain | |
some intuition. My previous post on [Zippers using Representable and | |
Cofree](http://chrispenner.ca/posts/representable-cofree-zippers) | |
is part of that adventure so I'd suggest you read that first if you haven't yet. | |
Like most higher-level mathematic concepts Adjunctions themselves are just | |
an abstract collection of types and shapes that fit together in a certain | |
way. This means that they have little practical meaning on their own, | |
but provide a useful set of tools to us if we happen to notice that some | |
problem we're working on matches their shape. The first time I dug into | |
adjunctions I went straight to the typeclass to check out which requirements | |
and methods it had. Here are the signatures straight from the source code in | |
Data.Functor.Adjunction | |
```haskell | |
class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where | |
unit :: a -> u (f a) | |
counit :: f (u a) -> a | |
leftAdjunct :: (f a -> b) -> a -> u b | |
rightAdjunct :: (a -> u b) -> f a -> b | |
``` | |
Hrmm... not the most illuminating. Unfortunately there's not much in | |
the way of documentation to help us out, but that's because the type signatures | |
pretty much explain how to USE adjunctions, but tragically they don't tell us | |
WHERE or HOW to use them. For this I think examples are the most useful, and | |
that's where I'll try to help out. | |
The first place to look for examples is in the 'instances' section of the type-class | |
itself, let's see what's in there: | |
```haskell | |
Adjunction Identity Identity | |
Adjunction ((,) e) ((->) e) | |
Adjunction f g => Adjunction (IdentityT f) (IdentityT g) | |
Adjunction f u => Adjunction (Free f) (Cofree u) | |
Adjunction w m => Adjunction (EnvT e w) (ReaderT e m) | |
Adjunction m w => Adjunction (WriterT s m) (TracedT s w) | |
(Adjunction f g, Adjunction f' g') => Adjunction (Compose f' f) (Compose g g') | |
(Adjunction f g, Adjunction f' g') => Adjunction (Sum f f') (Product g g') | |
``` | |
Hrmm, still not the most helpful, most of these instances depend on some | |
underlying functor ALREADY having an adjunction so those won't tell us how to | |
implement one. I see one for `Adjunction Identity Identity`, but something | |
tells me that's not going to provide much depth either. Let's | |
dive into the one remaining example: `Adjunction ((,) e) ((->) e)` | |
This one looks a little funny if you're not used to type sigs for functions and | |
tuples, but it gets a lot easier to read if we substitute it into the typeclass | |
methods. To specialize for the tuple/function adjunction we'll replace every | |
`f a` with `(e, a)` and each `u a` with `e -> a`: | |
> -- Tuple/Function adjunction specializations: | |
> tfUnit :: a -> (e -> (e, a)) | |
> tfCounit :: (e, (e -> a)) -> a | |
> tfLeftAdjunct, tfLeftAdjunct' :: ((e, a) -> b) -> a -> (e -> b) | |
> tfRightAdjunct, tfRightAdjunct' :: (a -> (e -> b)) -> (e, a) -> b | |
Hrmm, okay! That's a bit confusing but it's something we can work with. Let's | |
try to implement the functions! We'll implement our specialized versions so as | |
not to collide with the existing instance. | |
Unit and Counit are good starting points for understanding an adjunction. The | |
minimal definition of an adjunction is (unit AND counit) OR (leftAdjunct AND | |
rightAdjunct). That lets us know that unit and counit can themselves represent | |
the entire adjunction (i.e. leftAdjunct and rightAdjunct can be implemented in | |
terms of unit and counit; or vice versa). | |
Starting with `unit` we see from the type `a -> (e -> (e, a))` that we need to | |
take an arbitrary 'a' and embed it into a function which returns a tuple of the | |
same type as the function. Well, there's pretty much only one way I can think | |
to make this work! | |
> tfUnit a = \e -> (e, a) | |
Solid! We just converted the type signature into an implementation. | |
One down, three to go. This may not provide much insight, but don't worry we'll | |
get there yet. Next is counit which essentially does the opposite, exactly one | |
implementation seems clear to me: `(e, (e -> a)) -> a` | |
> tfCounit (e, eToA) = eToA e | |
If we stop here for a minute we can notice a few things, we built this | |
adjunction out of two functors, `(e, a)` and `e -> a`. These functors have a | |
unique relationship to one another in that they both hold *pieces* of the whole | |
picture, the tuple has an 'e' but doesn't know what to do with it, while `e -> | |
a` knows what to do with an 'e' but doesn't have one to work with! Only when we | |
pair the functors together do we have the full story! | |
The next thing to notice is that these functors are only readily useful when | |
nested in a specific ordering, we can write a counit which takes `(e, (e -> a)) | |
-> a`, BUT if we tried to put the function on the outside instead: `(e -> (e, | |
a)) -> a`; we have no way to get our 'a' out without having more information | |
since the 'e' is now hidden inside! This non-symmetric relationship shows us | |
that the nesting of functors matters. This is why we refer to the functors in | |
an adjunction as either `left adjoint` or `right adjoint`; (`f` and `u` respectively). | |
In our case `(e,)` is left adjoint and `(e ->)` is right adjoint. This is | |
probably still a bit confusing and that's okay! Try to hold on until we get to | |
start playing Battleship and I promise we'll have a more concrete example! One | |
more thing first, let's see how leftAdjunct and rightAdjunct play out for our | |
tuple/function adjunction. | |
Here's a refresher of the types: | |
```haskell | |
tfLeftAdjunct :: ((e, a) -> b) -> a -> (e -> b) | |
tfRightAdjunct :: (a -> (e -> b)) -> (e, a) -> b | |
``` | |
Now that we've written 'unit' and 'counit' we can implement these other functions | |
in terms of those. I'll provide two implementations here; one using unit/counit and | |
one without. | |
> tfLeftAdjunct f = fmap f . tfUnit | |
> tfRightAdjunct f = tfCounit . fmap f | |
> tfLeftAdjunct' eaToB a = \e -> eaToB (e, a) | |
> tfRightAdjunct' aToEToB (e, a) = aToEToB a e | |
We can see from the first set of implementations that `leftAdjunct` somehow | |
'lifts' a function that we give it from one that operates over the left-hand | |
functor into a result within the right-hand functor. | |
Similarly `rightAdjunct` takes a function which results in a value in left-hand | |
functor, and when given an argument embedded in the left-hand functor gives us | |
the result. The first set of implementations know nothing about the functors in | |
specific, which shows that if we write unit and counit we can let the default | |
implementations take over for the rest. | |
If you're keen you'll notice that this adjunction represents the curry and | |
uncurry functions! Can you see it? | |
```haskell | |
tfLeftAdjunct :: ((e, a) -> b) -> a -> (e -> b) | |
curry :: ((a, b) -> c) -> a -> b -> c | |
tfRightAdjunct :: (a -> (e -> b)) -> (e, a) -> b | |
uncurry :: (a -> b -> c) -> (a, b) -> c | |
``` | |
I haven't gotten to a point where I can prove it yet, but I believe all adjunctions | |
are actually isomorphic to this curry/uncurry adjunction! Maybe someone reading can | |
help me out with the proof. | |
Again, it's fun to see this play out, but where are the practical | |
applications?? Let's play a game. It's time to see if we can match these | |
shapes and patterns to a real(ish) problem. We're going to make a mini game of | |
Battleship, an old board game where players can guess where their opponents | |
ships are hiding within a grid and see if they can hit them! We'll start by | |
setting up some data-types and some pre-requisite instances, then we'll tie it | |
all together with an Adjunction! | |
> data Row = A | B | C | |
> deriving (Show, Eq) | |
> data Column = I | II | III | |
> deriving (Show, Eq) | |
> -- I'm going to define this as a Functor type to save time later, but for now | |
> -- we'll use the alias Coord; | |
> data CoordF a = CoordF Row Column a | |
> deriving (Show, Eq, Functor) | |
> type Coord = CoordF () | |
Each cell can hold a Vessel of some kind, maybe a Ship or Submarine; | |
It's also possible for a cell to be empty. | |
> data Vessel = Ship | Sub | Sunk | Empty | |
> deriving (Show, Eq) | |
We'll start with a 3x3 board to keep it simple, each row is represented by a | |
3-tuple. We've learned by now that making our types into Functors makes them | |
more usable, so I'm going to define the board as a functor parameterized over | |
the contents of each cell. | |
> data Board a = Board | |
> (a, a, a) | |
> (a, a, a) | |
> (a, a, a) | |
> deriving (Eq, Functor) | |
I'm going to add a quick Show instance, it's not perfect but it lets us see the | |
board! | |
> instance (Show a) => Show (Board a) where | |
> show (Board top middle bottom) = | |
> " I | II | III\n" | |
> ++ "A " ++ show top ++ "\n" | |
> ++ "B " ++ show middle ++ "\n" | |
> ++ "C " ++ show bottom ++ "\n" | |
Here's a good starting position, the board is completely empty! | |
> startBoard :: Board Vessel | |
> startBoard = Board | |
> (Empty, Empty, Empty) | |
> (Empty, Empty, Empty) | |
> (Empty, Empty, Empty) | |
It's at this point we want to start making guesses using a Coord and | |
seeing what's in each position! How else are we going to sink the | |
battleship? Well, when we start talking about 'Indexing' into our board | |
(which is a functor) I think immediately of the Representable typeclass from | |
[Data.Functor.Rep](https://hackage.haskell.org/package/adjunctions-4.3/docs/Dat | |
a-Functor-Rep.html#t:Representable). Don't let the name scare you, one of the | |
things that Representable gives you is the notion of *indexing* into a functor. | |
> instance Representable Board where | |
> -- We index into our functor using Coord | |
> type Rep Board = Coord | |
> | |
> -- Given an index and a board, pull out the matching cell | |
> index (Board (a, _, _) _ _) (CoordF A I _) = a | |
> index (Board (_, a, _) _ _) (CoordF A II _) = a | |
> index (Board (_, _, a) _ _) (CoordF A III _) = a | |
> index (Board _ (a, _, _) _) (CoordF B I _) = a | |
> index (Board _ (_, a, _) _) (CoordF B II _) = a | |
> index (Board _ (_, _, a) _) (CoordF B III _) = a | |
> index (Board _ _ (a, _, _)) (CoordF C I _) = a | |
> index (Board _ _ (_, a, _)) (CoordF C II _) = a | |
> index (Board _ _ (_, _, a)) (CoordF C III _) = a | |
> | |
> -- Given a function which describes a slot, build a Board | |
> tabulate desc = Board | |
> (desc (CoordF A I ()), desc (CoordF A II ()), desc (CoordF A III ())) | |
> (desc (CoordF B I ()), desc (CoordF B II ()), desc (CoordF B III ())) | |
> (desc (CoordF C I ()), desc (CoordF C II ()), desc (CoordF C III ())) | |
If you find it easier to implement unit and counit (which we'll explore soon) you | |
can implement those and then use `indexAdjunction` and `tabulateAdjunction` provided | |
by Data.Functor.Adjunction as your implementations for your Representable instance. | |
For Representable we also have a prerequisite of Distributive from | |
[Data.Distributive](https://hackage.haskell.org/package/distributive-0.5.0.2/do | |
cs/Data-Distributive.html#t:Distributive), All Representable functors are also | |
Distributive and this library has decided to make that an explicit requirement. | |
No problem though, it turns out that since every Representable is Distributive | |
that Data.Functor.Rep has a `distributeRep` function which provides an appropriate | |
implementation for us for free! We just need to slot it in: | |
> instance Distributive Board where | |
> distribute = distributeRep | |
Phew! A lot of work there, but now we can do some cool stuff! Let's say that | |
as a player we want to build a game board with some ships on it. We now have | |
two choices, we can either define a board and put some ships on it, or define a | |
function which says what's at a given coordinate and use that to build a board. | |
Let's do both, for PEDAGOGY! | |
> myBoard1 :: Board Vessel | |
> myBoard1 = Board | |
> (Empty, Empty, Ship) | |
> (Sub, Empty, Sub) | |
> (Ship, Empty, Empty) | |
> -- Now we'll define the same board using a function | |
> define :: Coord -> Vessel | |
> define (CoordF A III _) = Ship | |
> define (CoordF B I _) = Sub | |
> define (CoordF B III _) = Sub | |
> define (CoordF C I _) = Ship | |
> -- Otherwise it's Empty! | |
> define _ = Empty | |
> -- Now we build up a board using our descriptor function. | |
> -- Notice that (myBoard1 == myBoard2) | |
> myBoard2 :: Board Vessel | |
> myBoard2 = tabulate define | |
Okay this is already pretty cool; but I *DID* promise we'd use an adjunction | |
here somewhere, but for that we need TWO functors. Remember how CoordF is | |
actually a functor hidden undernath Coord? We can use that! This functor | |
doesn't make much sense on its own, but the important bit is that it's a | |
functor which contains part of the information about our system. Remember that | |
only one of our functors needs to be Representable in an Adjunction, so we can | |
take it easy and don't need to worry about Distributive or Representable for | |
CoordF | |
Now for the good stuff; let's crack out Adjunction and see if we can write an | |
instance! | |
I'm lazy, so I'm going to rely on Representable to do the dirty work, | |
Embedding an a into a Board filled with coordinates and values | |
doesn't make a ton of sense, but the most sensible way that I can | |
think of to do that is to put the a in every slot where the Coord represents | |
the index of the cell its in. | |
> instance Adjunction CoordF Board where | |
> unit :: a -> Board (CoordF a) | |
> unit a = tabulate (\(CoordF row col ()) -> CoordF row col a) | |
Counit actually makes sense in this case! We have our two pieces of info | |
which form the parts of the adjunction; The board contains the values in ALL | |
positions and the CoordF contains info which tells us exactly WHICH position | |
we're currently interested in. | |
For counit I'm just going to use index to pull the value out of the underlying board. | |
> counit :: CoordF (Board a) -> a | |
> counit (CoordF row col board) = index board (CoordF row col ()) | |
Done! We've written our Adjunction, let's keep building to game to see how we | |
can use the system! Here're the other type sigs for our Adjunction: | |
```haskell | |
leftAdjunct :: (CoordF a -> b) -> a -> Board b | |
rightAdjunct :: (a -> Board b) -> CoordF a -> b | |
``` | |
First let's observe unit and co-unit in action! | |
`unit` Always does the naive thing, so if we pass it a Vessel it'll just | |
set the whole board to that value; note that each slot is also labelled with its index! | |
```haskell | |
λ> unit Ship :: Board (CoordF Vessel) | |
A | B | C | |
I (CoordF A I Ship,CoordF A II Ship,CoordF A III Ship) | |
II (CoordF B I Ship,CoordF B II Ship,CoordF B III Ship) | |
III (CoordF C I Ship,CoordF C II Ship,CoordF C III Ship) | |
``` | |
If we already have our game board and also have an index then counit folds down the | |
structure by choosing the index specified by the outer CoordF Functor. | |
```haskell | |
-- Remember our board: | |
λ> myBoard1 | |
A | B | C | |
I (Empty,Empty,Ship) | |
II (Sub,Empty,Sub) | |
III (Ship,Empty,Empty) | |
λ> counit . CoordF A III $ myBoard1 | |
Ship | |
``` | |
So what about leftAdjunct and rightAdjunct? Conceptually you can think of these as | |
functions which let you operate over one piece of information and the Adjunction | |
will form the other piece of information for you! For instance leftAdjunct: | |
```haskell | |
leftAdjunct :: (CoordF a -> b) -> a -> Board b | |
``` | |
lets you build a value in the right adjoint functor by specifying how to handle | |
each index, this is similar to `tabulate` from from Representable. Earlier we | |
used tabulate to generate a game board from a shoot function, we can do the same | |
thing using leftAdjunct, we could re-implement our `shoot` function from above | |
in terms of leftAdjunct: | |
> myBoard3 :: Board Vessel | |
> myBoard3 = leftAdjunct define () | |
Right adjunct works similarly, but in reverse! Given a way to create | |
a board from a solitary value we can extract a value from the board matching | |
some CoordF. Just like leftAdjunct lines up with 'tabulate', rightAdjunct lines | |
up with 'index', but with a smidge of extra functionality. | |
```haskell | |
rightAdjunct :: (a -> Board b) -> CoordF a -> b | |
``` | |
I don't have any illuminating uses of rightAdjunct for our Battleship example, | |
but you can use it to reimplement 'index' from Representable if you like! | |
> myIndex :: Board a -> CoordF () -> a | |
> myIndex board coord = rightAdjunct (const board) coord | |
Cool, now let's try and make this game a little more functional! | |
Already we've got most of the basics for a simple game of battleship, | |
earlier we defined a game board in terms of a 'firing' function, now let's | |
write a function which takes a game board and mutates it according to a player's | |
layout. | |
War has changed over the years so our version of battleship is going to be a | |
bit more interesting than the traditional version. In our case each player | |
places ships OR submarines on each square, and when firing on a square they | |
may fire either a torpedo (hits ships) OR a depth charge (hits subs). | |
This means that we need a way to check not only if a cell is occupied, but also | |
if the vessel there can be hit by the weapon which was fired! For this we'll | |
take a look at the useful but vaguely named `zapWithAdjunction` function. | |
This function has its roots in an 'Pairing' typeclass which eventually was | |
absorbed by Adjunction. The idea of a Functor Pairing is that there's a relationship | |
between the structure of the two paired functors regardless of what's inside. Sounds | |
like an adjunction right?? `zapWithAdjunction` looks like this: | |
```haskell | |
zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c | |
``` | |
or for our types: | |
```haskell | |
zapWithAdjunction :: (a -> b -> c) -> Board a -> CoordF b -> c | |
``` | |
So it pairs a Board and Coord together, but applies a function *across* the | |
values stored there. It uses the adjunction to do this, so it will automagically | |
choose the 'right' value from the Board to apply with the value from the CoordF! | |
First we need weapons! | |
> data Weapon = Torpedo | DepthCharge | |
> deriving (Show, Eq) | |
Now we can write something like this: | |
> checkHit :: Vessel -> Weapon -> Bool | |
> checkHit Ship Torpedo = True | |
> checkHit Sub DepthCharge = True | |
> checkHit _ _ = False | |
> | |
> shoot :: Board Vessel -> CoordF Weapon -> Bool | |
> shoot = zapWithAdjunction checkHit | |
And of course we can try that out! | |
```haskell | |
λ> myBoard1 | |
A | B | C | |
I (Empty,Empty,Ship) | |
II (Sub,Empty,Sub) | |
III (Ship,Empty,Empty) | |
λ> shoot myBoard1 (CoordF A III Torpedo) | |
True | |
λ> shoot myBoard1 (CoordF A III DepthCharge) | |
False | |
``` | |
It's really unique how Adjunctions let us specify our data as a functor like this! | |
Now what if we want to see what happens at each spot in the board if we hit it | |
with a Torpedo OR a DepthCharge? No problem; | |
> hitMap :: Board (Bool, Bool) | |
> hitMap = fmap (flip checkHit Torpedo &&& flip checkHit DepthCharge) myBoard1 | |
We use (&&&) from Control.Arrow which combines two functions which take the same | |
input and makes a single function which returns a tuple! | |
```haskell | |
(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c') | |
``` | |
Now we've got a `Board (Bool, Bool)`, Since the right adjoint functor (Board) is | |
distributive, flipping the the tuple to the outside is trivial: | |
> hitMap' :: (Board Bool, Board Bool) | |
> hitMap' = unzipR hitMap | |
Now we've got two Boards, showing where we could get a hit if we used a Torpedo | |
or DepthCharge respectively. | |
Most of the functions we've written are a bit contrived. Sometimes the | |
adjunction-based approach was a bit clunkier than just writing a simple | |
function to do what you needed on a Board, but I hope this provides some form | |
of intuition for adjunctions. Good luck! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment