haskell - 您可以基于 `Comonads`定义 `Monads`吗？

好吧，假设您有类型

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。

这有可能吗？如果没有，那没有什么证明(是否存在可以证明m不是共鸣的特定Monad Dual m)？

一些观察:Dual IO a本质上是Void(而Const Void是有效的Comonad)。Dual m a的MonadPlus m是Void(只需使用dual mzero)。Dual Reader是Env。Dual Writer是Traced。
我认为Dual State是Store。

最佳答案

是的，事实上，除非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不是Fibration时(如上定义)，W如您所观察到的那样微不足道。

如果投影是唯一的，让我们称振动为覆盖物(尽管我不确定这种用法是否合适)。

承认该定理，您可以看到W(a)是a的副产品，它由_all可能的纤度∀r.F(r)-> r索引，即

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

换句话说，函子W(作为Func(Hask)的预装书)采取了纤维化作用，并由此构造了一个规范的琐碎的覆盖空间。

例如，令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)

因此，counit是唯一的。使用联乘积的明显索引，Wε将(i，j)映射到j，εW将(i，j)映射到i。因此，δ必须是唯一的“对角线”图，即δ(i)==(i，i)!

定理2。

令F为一个振动，令ΩW为与底层函子W的所有共轭的集合。然后ΩW≃1。

(对不起，我尚未将证明正式化。)

一组单声道ΜW的类似组合参数也很有趣，但是在这种情况下ΜW可能不是单例。 (取一些常数c并设置η:1-> c和μ(i，j)= i + j-c。)

请注意，如此构造的单子(monad)/共母通常不是原始共母/单子(monad)的对偶。例如，让M为单子(monad)
(F(a)=(Int，a)，η(x)=(0，x)，μ(n，(m，x))=(n + m，x))，即Writer。因此，自然投影在定理W(a)≃a中是唯一的，并且没有办法尊重原始代数。

还要注意，除非Void，否则共鸣通常是Fibration(可能有许多不同的方式)，这就是为什么从Comonad获得Monad的原因(但这不一定是唯一的!)。

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

Dual IO a本质上是无效的

据我所知，Haskell IO中定义了以下内容:

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

这意味着仅从类型理论来说，相应的覆盖范围就是由所有State# RealWorld索引的唯一规范的覆盖范围。您是否可以(或应该)拒绝这可能是一个哲学问题，而不是技术问题。

MonadPlus m => Dual m a无效

是的，但请注意，如果F(a)= 0则W(a)= 1且不是共称的(因为否则，counit表示类型W(0)-> 0≃1-> 0)。这是唯一的情况，在给定任意函子的情况下，W甚至都不是平凡的共性。

Dual Reader是..
这些陈述有时是正确的，有时不是正确的。取决于感兴趣的(共)代数是否与covers的(双)代数一致。

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

关于haskell - 您可以基于 `Comonads`定义 `Monads`吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/34302616/