haskell - 你能根据 `Comonads` 定义 `Monads` 吗？

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 不是共单胞)？

一些观察: 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

是的，事实上任何仿函数都会以这种方式产生一个独特的共单子(monad)，除非 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 索引的 a 的余积，即

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

换句话说，仿函数 W(作为 Func(Hask) 上的预层)接受一个纤维化并从中构造一个规范的平凡覆盖空间。

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

           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 为 Fibration，令 ΩW 为所有带有底层仿函数 W 的共单子(monad)的集合。然后 ΩW≃1。

(对不起，我没有正式证明。)

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

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

另请注意，除非 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# RealWorld索引的唯一规范覆盖空间。 s。您是否可以(或应该)拒绝这可能是一个哲学问题，而不是一个技术问题。

MonadPlus m => Dual m a是无效的

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

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