Double negation is a particular monad
data Void --no constructor because it is uninhabited
newtype DN a = DN {runDN :: (a -> Void) -> Void}
instance Monad DN where
return x = DN $ \f -> f x
m >>= k = DN $ \c -> runDN m (\a -> runDN (k a) c))
actually, this is an example of a more general monad
type DN = Cont Void
newtype Cont r a = Cont {runCont :: (a -> r) -> r}
which is the monad for continuation passing.
A concept like "monad" is not defined just by a signature, but also by some laws. So, here is a question, what should the laws for your construction be?
(a -> b) -> f b -> f a
is the signature of a method well known to category theory, the contravariant functor. It obeys essentially the same laws as functors (preserves (co)composition and identity). Actually, a contravariant functor is exactly a functor to the oppositite category. Since we are interested in "haskell functors" which are supposed to be endo-functors, we can see that a "haskell contravariant functor" is a functor Hask -> Hask_Op
.
On the other hand, what about
a -> f (f a)
what laws should this have? I have a suggestion. In category theory, it is possible to map between Functors. Given two functors from F, G
each from category C
to category D
, a natural transformation from F
to G
is a morphism in D
forall a. F a -> G a
that obeys certain coherence laws. You can do a lot with natural transformations, including using them to define a "functor category." But, the classic joke (due to Mac Lane) is that categories were invented to talk about functors, functors were invented to talk about natural transformations, and natural transformations were invented to talk about adjunctions.
A functor F : D -> C
and a functor G : C -> D
form an adjunction from C
to D
if there exist two natural transformations
unit : Id -> G . F
counit : F . G -> Id
This idea of an adjunction is a frequent way of understanding monads. Every adjunction gives rise to a monad in a totally natural way. That is, since the composition of these two functors is an endofunctor, and you have something akin to return (the unit), all you need is the join. But that is easy, join is just a function G . F . G . F -> G . F
which you get by just using the counit "in the middle".
So, then with all this, what is it that you are looking for? Well
dneg :: a -> n (n a)
looks exactly like the unit
of the adjunction of a contravariant functor with itself. Therefore, your Nomad
type is likely (certainly if your use of it to construct a monad is correct) exactly the same as "a contravariant functor which is self adjoint." Searching for self adjoint functors will lead you back to Double-negation and Continuation passing...which is just where we started!
EDIT: Almost certainly some of the arrows above are backwards. The basic idea is right, though. You can work it out yourself using the citations below:
The best books on category theory are probably,
- Steve Awodey, Category Theory
- Sanders Mac Lane, Categories for the Working Mathematician
although numerous more approachable intro books exist including Benjamin Pierces book on Category Theory for computer scientists.
Video lectures online
- The Category Theory lectures by Steve Awodey from the Oregon Programming Language Summer School
- The Catsters short lectures on youtube, indexed here, pay particular attention to the videos on adjunctions
A number of papers explore the adjunction angle on the continuation monad, for example
- Hayo Thielecke, Continuation Semantics and Self-adjointness
The search terms "self adjoint", "continuation", and "monad" are good. Also, a number of bloggers have written about these issues. If you google "where do monads come from" you get useful results like this one from the n category cafe, or this one from sigfpe. Also Sjoerd Vissche's link to the Comonad reader.