你能根据`Monads`来定义`Comonads`吗？

Question

好吧,让我们说你有类型

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

事实证明,什么时候f是Comonad,Dual f是Monad(有趣的运动).它是否相反？

您可以定义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,我想.

Answer 1

是的，事实上任何函子都会以这种方式产生一个独特的共子，除非 f==0。

令 F 成为 Hask 上的一个内函子。让

W(a) = ?r.F(a->r)->r
W(f) = F(f?)?
       where g?(h) = h?g

一旦你意识到以下同构，这个谜题本质上就变成了几何/组合：

定理 1。

假设类型 (?rr->F(r)) (?rF(r)->r) 都不是空的。那么存在类型 W(a) 的同构吗？(?rF(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) 视为由 _all 可能的纤维化 ?rF(r)->r 索引的 a 的联积，即

W(a) ? ?a
       ?::?f.F(r)->r

换句话说，函子 W（作为 Func(Hask) 上的 presheaf）接受颤动并从中构造一个规范化的平凡化覆盖空间。

例如，设 F(a)=(Int,a,a,a)。然后我们有三个明显的自然纤维 F(a)->a。用+写出余积，下图连同上述定理应该足以具体描述共生：

           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 是一个 Fibration，令 ?W 是所有带有基础函子 W 的共子的集合。然后?W?1。

（对不起，我没有正式证明。）

一组 monad 的类似组合论证 ?W 也很有趣，但在这种情况下 ?W 可能不是单例。（取一些常数 c 并设置 ?:1->c 和 ?(i,j)=i+jc。）

请注意，这样构造的 monads/comonads 通常不是原始 comonads/monads 的对偶。例如让 M 是一个单子 (F(a)=(Int,a), ?(x) = (0,x), ?(n,(m,x)) = (n+m,x)),即一个Writer。自然投影是唯一的，因此根据定理 W(a)?a，没有办法尊重原始代数。

还请注意，comonad 是一个微不足道的 Fibration（可能有许多不同的方式），除非Void，这就是为什么您从 Comonad 获得了一个 Monad（但这不一定是唯一的！）。

关于您的观察的一些评论：

• Dual IO a 基本上是空的

  据我所知，在 Haskell IO 中定义如下：

    -- ghc/libraries/ghc-prim/GHC/Types.hs
   newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
  

  这意味着仅从类型理论来看，相应的覆盖是_由所有State# RealWorlds索引的唯一规范覆盖空间。您是否可以（或应该）拒绝这可能是一个哲学问题，而不是一个技术问题。

• MonadPlus m => Dual m a 是空的

  是的，但请注意，如果 F(a)=0 则 W(a)=1 并且它不是共子（因为否则 counit 将暗示类型 W(0)->0 ? 1->0）。这是 W 甚至不能是给定任意函子的平凡共子的唯一情况。

• Dual Reader是.. 这些陈述有时是正确的，有时则不是。取决于感兴趣的（共）代数是否与覆盖的（双）代数一致。

所以我很惊讶几何 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