Thu 5 Jun 2008
I've had a few people ask me questions about Adjunctions since my recent post and a request for some more introductory material, so I figured I would take a couple of short posts to tie Adjunctions to some other concepts.
Representable Functors
A covariant functor is said to be representable by an object if it is naturally isomorphic to .
We can translate that into Haskell, letting play the role of with:
class Functor f => Representable f x where rep :: (x -> a) -> f a unrep :: f a -> (x -> a) {-# RULES "rep/unrep" rep . unrep = id "unrep/rep" unrep . rep = id #-}
It is trivial to show that any two representations of a given functor must be isomorphic, and that there is a natural isomorphism between any two functors with the same representation, so we could strengthen the signature of the type class above by adding a pair of functional dependencies: f -> x, x -> f, but lets work without this straightjacket for now.
Example
We can represent the anonymous reader monad with its environment.
instance Representable ((->)x) x where rep = id unrep = id
Example
We could adopt the pleasant fiction that () has a single inhabitant to avoid bringing in an empty type, but lets do this correctly. Clearly the Identity functor needs no extra information from its representation.
data Void {- you'll need EmptyDataDecls -} instance Representable Identity Void where rep f = Identity (f undefined) unrep = const . runIdentity
Adjunctions
If you recall the definition of Adjunctions over from before:
class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where unit :: a -> g (f a) counit :: f (g a) -> a leftAdjunct :: (f a -> b) -> a -> g b rightAdjunct :: (a -> g b) -> f a -> b unit = leftAdjunct id counit = rightAdjunct id leftAdjunct f = fmap f . unit rightAdjunct f = counit . fmap f
We can generate a lot of representable functors, by turning to the theorem mentioned in the Wikipedia article about the representability of a right adjoint in terms of its left adjoint wrapped around a singleton element:
Any functor with a left adjoint is represented by (FX, ηX(•)) where X = {•} is a singleton set and η is the unit of the adjunction.
Well, earlier we defined a singleton set, Void
, and can play the role of as we did above. For , we can translate the remainder quite easily:
repAdjunction :: Adjunction f g => (f Void -> a) -> g a repAdjunction f = leftAdjunct f undefined unrepAdjunction :: Adjunction f g => g a -> (f Void -> a) unrepAdjunction = rightAdjunct . const
Now, as usual the way type class inference works in Haskell requires us to reason somewhat backwards.
You'd like to say:
instance Adjunction f g => Representable g (f Void) where rep = repAdjunction; unrep = unrepAdjunction
But if you do so, you can't define any other instances for Representable
, you'll have used up the instance head, so the previous definitions couldn't be made.
On the other hand, you can create the obligation for an appropriate instance of Representable
by changing the signature of Adjunction
:
class (Representable g (f Void), Functor f) => Adjunction f g | f -> g, g -> f where ...
Then the definitions for repAdjunction
and unrepAdjunction
can be used by any would-be Adjunction
to automatically generate the corresponding Representable
instance, just like liftM
can alwyas be used to make a Haskell Monad
into a Functor
.
We can also go the other way and define an Adjunction
given a representation for the right adjoint, but I'll leave that as an exercise for the reader. (Hint: you'll probably want to weaken the signature for Adjunction to remove the fundeps, so you can test some simple cases). You may also want to take a look at the section on Adjunctions as Kan extensions portion of the earlier post.
I have since modified category-extras definition of Adjunction to require the instance for Representable motivated above.
Haddock:
[Control.Functor.Adjunction]
[Control.Functor.Representable]
June 5th, 2008 at 3:34 pm
[...] Now, we would like to do the same thing we did with Representable last time, and just require the user of the Adjunction class to provide us with more instances, something like: [...]
June 13th, 2008 at 5:33 pm
Just to let you know that this post helped my understanding of category-theoretic representability and representable functors.