Are all differentiable types Monads

Question

Given a differentiable type, we know that its Zipper is a Comonad. In response to this, Dan Burton asked, "If derivation makes a comonad, does that mean that integration makes a monad? Or is that nonsense?". I'd like to give this question a specific meaning. If a type is differentiable, is it necessarily a monad? One formulation of the question would be to ask, given the following definitions

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)

can we write functions with signatures similar to

return :: (Diff t) => a -> t a
(>>=) :: (Diff t) => t a -> (a -> t b) -> t b

obeying the Monad laws.

In the answers to the linked questions, there were two successful approaches to a similar problem of deriving Comonad instances for the Zipper. The first approach was to expand the Diff class to include the dual of >>= and use partial differentiation. The second approach was to require that the type be twice or infinitely differentiable.

Sjoerd Visscher · Accepted Answer · 2014-12-04T16:43:40.617

5

No. The void functor data V a is differentiable, but return cannot be implemented for it.

edited Dec 04 '14 at 16:43

answered Dec 04 '14 at 15:46

Sjoerd Visscher

11,840
2
47
59

So, this demonstrates that "being differentiable" does not guarantee that something can also be "the result of integration". It soundly answers Cirdec's question, but doesn't particularly answer mine. (I'm not asking for an answer, just noting.) The derivative of zero is zero, but the indefinite integral of zero is not necessarily zero. It's an arbitrary constant. – Dan Burton Dec 11 '14 at 18:55
@DanBurton If you think of the `Zipper` holding a `D t` as being the derivative, `D t` being the derivative of `t` lead to a `Comonad` instance for `Zipper t`. Integration is the inverse of differentiation, so `t` is the/an integral of `D t`. Having a derivative is the same as being an integral. That's why I phrased the question the way I did: Does `t` being the/an integral of `D t` lead to a `Monad` instance for a `t`? – Cirdec Dec 11 '14 at 19:30
@DanBurton We can make a `Monad` instance for something opposite, see my new answer. – Cirdec Dec 11 '14 at 21:16

score 3 · Answer 2 · edited May 23 '17 at 12:19

We can unsurprising derive a Monad for something similar if we reverse absolutely everything. Our previous statement and new statements are below. I'm not entirely sure that the class defined below is actually integration, so I won't refer to it explicitly as such.

if D  t is the derivative of t then the product of D  t and the identity is a Comonad
if D' t is the ???        of t then the sum     of D' t and the identity is a Monad

First we'll define the opposite of a Zipper, an Unzipper. Instead of a product it will be a sum.

data Zipper   t a = Zipper { diff :: D  t a  ,  here :: a }
data Unzipper t a =          Unzip  (D' t a) |  There   a

An Unzipper is a Functor as long as D' t is a Functor.

instance (Functor (D' t)) => Functor (Unzipper t) where
    fmap f (There x) = There (f x)
    fmap f (Unzip u) = Unzip (fmap f u)

If we recall the class Diff

class (Functor t, Functor (D t)) => Diff t where
    type D t :: * -> *
    up :: Zipper t a -> t a
    down :: t a -> t (Zipper t a)

the class of things opposite to it, Diff', is the same but with every instance of Zipper replaced with Unzipper and the order of the -> arrows flipped.

class (Functor t, Functor (D' t)) => Diff' t where
    type D' t :: * -> *
    up' :: t a -> Unzipper t a
    down' :: t (Unzipper t a) -> t a

If we use my solution to the previous problem

around :: (Diff t, Diff (D t)) => Zipper t a -> Zipper t (Zipper t a)
around z@(Zipper d h) = Zipper ctx z
    where
        ctx = fmap (\z' -> Zipper (up z') (here z')) (down d)

we can define the inverse of that function, which will be join for the Monad.

inside :: (Diff' t, Diff' (D' t)) => Unzipper t (Unzipper t a) -> Unzipper t a
inside (There x) = x
inside (Unzip u) = Unzip . down' . fmap f $ u
    where
        f (There u') = There u'
        f (Unzip u') = up' u'

This allows us to write a Monad instance for the Unzipper.

instance (Diff' t, Diff' (D' t)) => Monad (Unzipper t) where
    return = There
    -- join = inside
    x >>= f = inside . fmap f $ x

This instance is in the same vein as the Comonad instance for the Zipper.

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where
    extract   = here
    duplicate = around

I am now curious if there's a free `Diff'` `FD f` for any `Functor` `f` such that `Unzipper (FD f)` is the free monad, `Free f`. — Cirdec, Dec 11 '14 at 21:27
D' (FD f) a = f (UnZipper (FD f) a). up' is easy, but I'm not sure about down'. It seems like `f` would have to be a monad to merge the layers. Note that `up' . down'` appears to be equivalent to `wrap`. — Dan Burton, Dec 17 '14 at 10:49

Are all differentiable types Monads

2 Answers2

Linked