Все дифференцируемые типы Monads

Учитывая дифференцируемый тип, мы знаем, что его Zipper является Comonad. В ответ на это Дэн Бертон спросил: "Если вывод делает comonad, значит ли это, что интеграция делает монаду? Или это глупость?". Я хотел бы задать этот вопрос конкретному значению. Если тип дифференцируемый, обязательно ли это монада? Одна формулировка вопроса заключалась бы в том, чтобы спросить, учитывая следующие определения

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)

можем ли мы писать функции с сигнатурами, аналогичными

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

подчиняясь законы Монады.

В ответах на связанные вопросы были два успешных подхода к аналогичной проблеме получения экземпляров Comonad для Zipper. Первый подход заключался в расширении класса Diff, чтобы включить двойное значение >>= и использовать частичное дифференцирование. Второй подход заключался в требовании, чтобы тип был дважды или бесконечно дифференцируемым.

Ответы

Ответ 1

Нет. Функтор void data V a является дифференцируемым, но return не может быть реализован для него.

Ответ 2

Мы можем неудивительно получить Monad для чего-то подобного, если мы полностью отменим все. Ниже приведено наше предыдущее выражение и новые заявления. Я не совсем уверен, что класс, определенный ниже, фактически является интеграцией, поэтому я не буду ссылаться на него явно как таковой.

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

Сначала определим противоположность Zipper, a Unzipper. Вместо продукта это будет сумма.

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

An Unzipper является Functor, если D' t является Functor.

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

Если вспомнить класс 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)

класс вещей, противоположных ему, Diff', тот же, но с заменой каждого экземпляра Zipper на Unzipper и порядок стрелок ->.

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

Если мы используем мое решение для предыдущей проблемы

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

мы можем определить обратную для этой функции, которая будет join для 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'

Это позволяет нам написать экземпляр Monad для Unzipper.

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

Этот экземпляр находится в том же духе, что и экземпляр Comonad для Zipper.

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