Are all differentiable types Monads

问题:

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.

回答1:

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

回答2:

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