Are all differentiable types Monads
Asked Answered
B

2

19

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.

Booking answered 3/12, 2014 at 21:35 Comment(0)
R
5

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

Rabbin answered 4/12, 2014 at 15:46 Comment(3)
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.Shakitashako
@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?Booking
@DanBurton We can make a Monad instance for something opposite, see my new answer.Booking
B
3

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
Booking answered 11/12, 2014 at 21:2 Comment(2)
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.Booking
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.Shakitashako

© 2022 - 2024 — McMap. All rights reserved.