Можете ли вы определить `Comonads` на основе` Monads`?

Хорошо, так скажем, у вас есть тип

newtype Dual f a = Dual {dual :: forall r. f(a -> r)->r}

Как оказывается, когда f является Comonad, Dual f является монадой (упражнение с потерей). Работает ли это наоборот?

Вы можете определить fmap ab (Dual da) = Dual $ \fb -> da $ fmap (. ab) fb и extract (Dual da) = da $ return id, но я не знаю, как определить duplicate или extend.

Возможно ли это? Если нет, то какого доказательства нет (существует ли конкретная Monad m, для которой вы можете доказать, что Dual m не является comonad)?

Некоторые наблюдения: Dual IO a по существу Void (и Const Void является допустимым Comonad). Dual m a для MonadPlus m - Void (просто используйте dual mzero). Dual Reader - Env. Dual Writer - Traced. Dual State Store, я думаю.

Ответ 1

Да, на самом деле любой функтор приводит к созданию уникальной comonad таким образом, если f == 0.

Пусть F - контур на Hask. Пусть

W(a) = ∀r.F(a->r)->r
W(f) = F(f∗)∗
       where g∗(h) = h∘g

Головоломка становится геометрической/комбинаторной по своей природе, как только вы осознаете следующий изоморфизм:

Теорема 1.

Предположим, что ни один из типов (∀r.r- > F (r)) (∀r.F(r) → r) пуст. Тогда существует изоморфизм типов W (a) ≃ (∀r.F(r) → r, a).

Доказательство:

class Functor f => Fibration f where
        projection   :: ∀r. f(r)->r
        some_section :: ∀r. r->f(r) -- _any_ section will work

to :: forall f a. Fibration f
      => (∀r.f(a->r) -> r)
      -> (∀r.f(r)->r, a)
to(f) = ( f . fmap const
        , f(some_section(id)))

from :: forall f a. Fibration f
        => (∀r.f(r)->r, a)
        -> (∀r.f(a->r) -> r)
from (π,η) = ev(η) . π

ev :: a -> (a->b) -> b
ev x f = f x

Заполнение сведений об этом (которое я могу отправить по запросу) потребует немного параметричности и леммы Йонеды. Когда F не является расслоением (как я определил выше), W тривиально, как вы заметили.

Назовем расслоение накрытием, если проекция является уникальной (хотя я не уверен, что это использование подходит).

Применяя теорему, вы можете видеть W (a) как копроизведение индексированного всеми возможными расслоениями ∀r.F(r) → r, т.е.

W(a) ≃ ∐a
       π::∀f.F(r)->r

Другими словами, функтор W (как предпучок на Func (Hask)) принимает расслоение и строит из него канонически тривиализованное накрывающее пространство.

В качестве примера, пусть F (a) = (Int, a, a, a). Тогда мы имеем три очевидных естественных расслоения F (a) → a. Написав копроизведение на +, следующая диаграмма вместе с вышеприведенной теоремой, должно быть, достаточно, чтобы описать comonads конкретно:

           a
           ^
           | ε
           |
         a+a+a
        ^  |  ^
     Wε |  |δ | εW
        |  v  |
(a+a+a)+(a+a+a)+(a+a+a)

Таким образом, конгрессия уникальна. Используя очевидные индексы в копроизведение, Wε отображает (i, j) в j, εW отображает (i, j) в i. Таким образом, δ должно быть единственным "диагональным" отображением, а именно δ (i) == (i, i)!

Теорема 2.

Пусть F - расслоение и ΩW - множество всех комонад с основополагающим функтором W. Тогда ΩW≃1.

(Извините, я не формализовал доказательство.)

Интересен и аналогичный комбинаторный аргумент для множества монад MW, но в этом случае МW может быть не одиночным. (Возьмем некоторую константу c и положим η: 1- > c и μ (i, j) = я + j-c.)

Заметим, что построенные монады/комонады не являются дуальными для исходных комонад/монад вообще. Например, пусть M - монада (F (a) = (Int, a), η (x) = (0, x), μ (n, (m, x)) = (n + m, x)), т.е. a Writer. Естественная проекция единственна, следовательно, по теореме W (a) ≃a, и нет возможности уважать исходную алгебру.

Обратите внимание также, что comonad тривиально является Fibration (возможно, многими разными способами), если Void, поэтому вы получили Monad из Comonad (но это не обязательно уникально!).

Несколько комментариев о ваших наблюдениях:

Dual IO a по существу Void

Насколько я знаю, в Haskell IO определено что-то вроде:
```
  -- ghc/libraries/ghc-prim/GHC/Types.hs
 newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
```
что означает только из теории типов, соответствующее покрытие является единственным каноническим накрывающим пространством, индексированным всеми State# RealWorld s. Можете ли вы (или должны) отвергнуть это, вероятно, философский, а не технический вопрос.
MonadPlus m => Dual m a - Void

Правильно, но заметим, что если F (a) = 0, то W (a) = 1, и это не комонада (так как в противном случае у канита будет подразумеваться тип W (0) → 0 ≃ 1- > 0), Это единственный случай, когда W даже не может быть тривиальной комонадой, заданной произвольным функтором.
Dual Reader есть.. Иногда эти утверждения могут быть правильными, иногда нет. Зависит от того, согласуется ли (со) алгебра с алгеброй (bi) покрытий.

Итак, я удивлен, насколько интересным является геометрический Haskell! Я думаю, что может быть очень много геометрических конструкций, подобных этому. Например, естественным обобщением этого было бы рассмотреть "каноническую тривиализацию" F- > G для некоторых ковариантных функторов F, G. Тогда группа автоморфизмов для базового пространства уже не будет тривиальной, поэтому для правильного понимания этого потребуется немного больше теории.

Наконец, здесь доказательство кода концепции. Спасибо за отличную освежающую головоломку и очень веселое Рождество; -)

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Comonad

class Functor f => Fibration f where
        x0 :: f ()
        x0 = some_section ()

        some_section :: forall r. r -> f(r)
        some_section x = fmap (const x) x0

        projection :: forall r. f(r) -> r

newtype W f a = W { un_w :: forall r. f(a->r)->r }

instance Functor f =>  Functor (W f) where
        fmap f (W c) = W $ c . fmap (. f)

instance Fibration f => Comonad (W f) where
        extract = ε
        duplicate = δ

-- The counit is determined uniquely, independently of the choice of a particular section.
ε :: forall f a. Fibration f => W f a -> a
ε (W f) = f (some_section id)

-- The comultiplication is unique too.
δ :: forall f a. Fibration f => W f a -> W f (W f a)
δ f = W $ ev(f) . un_w f . fmap const

ev :: forall a b. a -> (a->b)->b
ev x f = f x

-- An Example
data Pair a = P {p1 ::a
                ,p2 :: a
                 }
               deriving (Eq,Show)

instance Functor Pair where
        fmap f (P x y) = P (f x)  (f y)

instance Fibration Pair where
        x0 = P () ()
        projection = p1

type PairCover a = W Pair a

-- How to construct a cover (you will need unsafePerformIO if you want W IO.)
cover :: a -> W Pair a
cover x = W $ ev(x) . p1