31

好的，假设你有类型

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) fband extract (Dual da) = da $ return id，但我不知道如何定义duplicateor extend。

这甚至可能吗？如果不是，那么没有什么证明（是否有一个特定的 Monadm可以证明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，我认为。

4

1 回答 1

5

是的，事实上任何函子都会以这种方式产生一个独特的共单子，除非 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) 是由_所有可能的纤维 ∀rF(r)->r 索引的 a 的余积，即

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

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

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

请注意，如此构造的单子/单子通常不是原始单子/单子的对偶。例如让 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# RealWorld这意味着仅从类型论来看，相应的覆盖是_由所有s索引的唯一规范覆盖空间。您是否可以（或应该）拒绝这可能是一个哲学问题，而不是一个技术问题。

  • MonadPlus m => Dual m a是无效的

    是的，但请注意，如果 F(a)=0 则 W(a)=1 并且它不是共单胞（因为否则该共单将暗示类型 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
于 2016-12-24T06:16:55.423 回答