Use cases for adjunctions in Haskell
Asked Answered
D

1

14

I have been reading up on adjunctions during the last couple of days. While I start to understand their importance from a theoretical point of view, I wonder how and why people use them in Haskell. Data.Functor.Adjunction provides an implementation and among its instances are free functor / forgetful functor and curry / uncurry. Again those are very interesting from the theoretical view point but I can't see how I would use them for more practical programming problems.

Are there examples of programming problems people solved using Data.Functor.Adjunction and why you would prefer this implementation over others?

Ditheism answered 12/6, 2019 at 9:47 Comment(3)
I could (so, so easily) be wrong, but I think Data.Functor.Adjunction exists primarily to demonstrate that the categorical idea of adjunction can be represented in Haskell.Claver
There is a use case in a made up game here: chrispenner.ca/posts/adjunction-battleship I have yet to work through this write up myself.Ditheism
Nitpick: the first instance you have linked to isn't a free/forgetful adjunction, but an adjunction between the free monad for a Hask/Hask left adjoint and the cofree comonad for the corresponding Hask/Hask right adjoint.Goines
G
6

Preliminary note: This answer is a bit speculative. Much like the question, it was built from studying Data.Functor.Adjunction.

I can think of three reasons why there aren't many use cases for the Adjunction class in the wild.

Firstly, all Hask/Hask adjunctions are ultimately some variation on the currying adjunction, so the spectrum of potential instances isn't all that large to begin with. Many of the adjunctions one might be interested on aren't Hask/Hask.

Secondly, while an Adjunction instance gives you a frankly awesome amount of other instances for free, in many cases those instances already exist somewhere else. To pick the ur-example, we might very easily implement StateT in terms of Control.Monad.Trans.Adjoint:

newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
  deriving (Functor, Applicative, Monad) via AdjointT ((,) s) ((->) s) m
  deriving MonadTrans via AdjointT ((,) s) ((->) s)
  -- There is also a straightforward, fairly general way to implement MonadState.

However, no one needs to actually do that, because there is a perfectly good StateT in transformers. That said, if you do have an Adjunction instance of your own, you might be in luck. One little thing I have thought of that might make sense (even if I haven't actually seen it out there) are the following functors:

data Dilemma a = Dilemma { fstDil :: a, sndDil a }

data ChoiceF a = Fst a | Snd a

We might write an Adjunction ChoiceF Dilemma instance, which reflects how Dilemma (ChoiceF a) is materialised version of State Bool a. Dilemma (ChoiceF a) can be thought of as a step in a decision tree: choosing one side of the Dilemma tells you, through the ChoiceF constructors, what choice is to be made next. The Adjunction instance would then give us a monad transformer for Dilemma (ChoiceF a) for free.

(Another possibility might be exploiting the Free f/Cofree u adjunction. Cofree Dilemma a is an infinite tree of outcomes, while Free ChoiceF a is a path leading to an outcome. I hazard there is some mileage to get out of that.)

Thirdly, while there are many useful functions for right adjoints in Data.Functor.Adjunction, most of the functionality they provide is also available through Representable and/or Distributive, so most places where they might be used end up sticking with the superclasses instead.

Data.Functor.Adjunction, of course, also offers useful functions for left adjoints. On the one hand, left adjoints (which are isomorphic to pairs i.e. containers that hold a single element) are probably less versatile than right adjoints (which are isomorphic to functions i.e. functors with a single shape); on the other hand, there doesn't seem to be any canonical class for left adjoints (not yet, at least), so that might lead to opportunities for actually using Data.Functor.Adjunction functions. Incidentally, Chris Penner's battleship example you suggested arguably fits the bill, as it does rely on the left adjoint and how it can be used to encode the representation of the right adjoint:

zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c
zapWithAdjunction @CoordF @Board :: (a -> b -> c) -> Board a -> CoordF b -> c

checkHit :: Vessel -> Weapon -> Bool

shoot :: Board Vessel -> CoordF Weapon -> Bool

CoordF, the left adjoint, carries coordinates for the board and a payload. zapWithAdjunction makes it possible to (quite literally, in this case), target the position while using the payload.

Goines answered 21/6, 2019 at 14:0 Comment(1)
thanks for so much insight. This is food for thoughts for me for a while.Ditheism

© 2022 - 2024 — McMap. All rights reserved.