你能基于Monads来定义`Comonads`吗？ [英] Can you define `Comonads` based on `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 。

这甚至可能吗？如果没有，那么证明什么没有（有没有一个特定的Monad m ，你可以证明 Dual m 是不是一个comonad）？

一些观察：
双重IO a 本质上是 Void （和 Const Void 是一个有效的 Comonad ）。
Dual ma MonadPlus m 无效（只需使用 dual mzero ）。
双读卡器是 Env 。
Dual Writer 是追踪。
双重状态是 Store ，我想。

解决方案

是的，实际上任何函数都会以这种方式产生一个独特的comonad，除非f == 0。让F成为哈斯克的一位管理者。令b
$ b

  W（a）=∀rF（a-> r） - > r 
 W（f ）= F（f *）* 
其中g *（h）=h∘g
  

一旦你意识到以下的同构性，这个难题就会变成几何/组合的：

定理1.

假设两种类型（∀rr - > F（r））（∀rF（r） - > r）为空。然后有一个同构类型W（a）≃（rrF（r） - > r，a）。

证明：

  class Functor f =>振动f其中
投影::∀r。 f（r） - > r 
 some_section ::∀r。 r-> f（r） -  _any_部分将工作
 
到:: forall f a。振动f 
 => （∀r.f（a-> r） - > r）
  - > （∀rf（r） - > r，a）
到（f）=（f。fmap const 
，f（some_section（id）））
 
 from： ：forall f a。振动f 
 => （∀r.f（r） - > r，a）
  - > （∈r.f（a→r）→r）
从（π，η）= ev（η）。 π
 
 ev :: a  - > （a-> b） - > b 
 ev xf = fx 
  

填写详细信息请求）需要
a位参数和Yoneda引理。当F不是Fibration时（正如我上面定义的那样），W就像你观察到的那样微不足道。 如果投影是独一无二的，我们称之为覆盖我们不确定这种用法是否恰当）。

承认这个定理，您可以看到W（a）是所有可能的纤维索引的a副产品， r） - > r，即

  W（a）≃∐a
π::∀fF（r） - > r 
  

换句话说，函数W（作为Func（Hask）的预热）作为一个例子，假设F（a）=（Int，a，a，a）。然后我们有三个明显的天然纤维F（a） - > a。

  a $写出coproduct by +，下面的图和上面的定理应该足以描述具体的comonads： b $ b ^ 
 | ε
 | 
 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。

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

单数组MMW的类似组合参数也很有趣，但在这种情况下，MM可能不是单例。 （取一些常数c并设定η：1-> c和μ（i，j）= i + jc。）注意这样构造的monads / comonads是而不是与一般的原始连接器/ monad的对偶。例如，假设M是一个monad
（F（a）=（Int，a），η（x）=（0，x），μ（n，（m，x））=（n + m， x）），即 Writer 。自然投影是唯一的，因此由定理W（a）≃a，并且没有办法尊重原代数。

还要注意的是，一个共同体是平凡的振动（可能有许多不同的方式），除非 Void ，这就是为什么你从一个Comonad获得一个Monad（但这不一定是唯一的！）。

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

• 双IO a 本质上是空的

  
  
  

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

     -  ghc / libraries / ghc-prim / GHC / Types.hs 
   newtype IO a = IO（State＃RealWorld  - >（#State＃RealWorld，a ＃））
    

  这意味着仅从类型理论中相应的覆盖就是唯一的规范覆盖空间索引所有状态＃RealWorld s。您是否可以（或应该）拒绝这可能是一个哲学问题，而不是一个技术问题。

双ma 是Void




对，但请注意，如果F（a）= 0，那么W（a）= 1，它不是comonad（因为否则该议会暗示类型W（0） - > 0≃1-> 0）。这是唯一的情况下，W甚至不能给一个任意的函子一个微不足道的comonad。


• 双读卡器是..
  那些陈述有时是正确的，有时不是。取决于感兴趣的（共）代数是否与覆盖的（bi）代数一致。
  
  
  

  米惊讶几何Haskell真的有趣！我猜可能有很多类似这样的几何结构。例如，一个自然泛化就是考虑F-> G对于一些协变函数F，G的'规范平凡化'。然后，基空间的自同构群将不再是微不足道的，因此需要更多的理论来正确理解这一点。

  
  
  

  最后，这是一个概念代码的证明。 - ）

    { - ＃LANGUAGE RankNTypes＃ - } $ b感谢您提供一个令人耳目一新的益智游戏，并且有一个非常愉快的圣诞节; $ b { - ＃LANGUAGE ScopedTypeVariables＃ - } 
   
   import Control.Comonad 
   
   class Functor f =>振动f其中
   x0 :: f（）
   x0 = some_section（）
   
   some_section :: forall r。 r  - > f（r）
   some_section x = fmap（const x）x0 
   
  投影:: forall r。 f（r） - > r 
   
   newtype W f a = W {un_w :: forall r。 f（a-> r） - > r} 
   
  实例Functor f => Functor（W f）其中
   fmap f（W c）= W $ c。 fmap（.f）
   
   instance Fibration f => Comonad（W f）其中
   extract =ε
   duplicate =δ
   
    - 该计数是唯一确定的，与特定部分的选择无关。 
  ε:: forall f a。振动f => W f a  - > a 
  ε（W f）= f（some_section id）
   
    - 乘法也是唯一的。 
  δ:: forall f a。振动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 xf = fx 
   
    - 示例
   data Pair a = P {p1 :: a 
  ， （Eq，Show）
   
  实例Functor Pair其中
   fmap f（P xy）= P（fx）（fy）$（$ p 
   
   $ b） b 
   $ b实例Fibration Pair其中
   x0 = P（）（）
  投影= p1 
   
  类型PairCover a = W对a 
   
    - 如何构建一个封面（如果需要W IO，您将需要unsafePerformIO）。
   cover :: a  - > W配对
  覆盖x = W $ ev（x）。 p1 
    

  
  

  Okay, so let's say you have the type

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

  As it turns out, when f is a Comonad, Dual f is a Monad (fun exercise). Does it work the other way around?

  You can define fmap ab (Dual da) = Dual $ \fb -> da $ fmap (. ab) fb and extract (Dual da) = da $ return id, but I do not know how to define duplicate or extend.

  Is this even possible? If not, what the proof there is not (is there a particular Monad m for which you can prove Dual m is not a comonad)?

  Some observations: Dual IO a is essentially Void (and Const Void is a valid Comonad). Dual m a for MonadPlus m is Void (just use dual mzero). Dual Reader is Env. Dual Writer is Traced. Dual State is Store, I think.

  解决方案

  Yes, in fact any functor gives rise to a unique comonad in this way, unless f==0.

  Let F be an endofunctor on Hask. Let

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

  The puzzle becomes geometric/combinatoric in nature once you realize the following isomorphism:

  Theorem 1.

  Suppose neither of the types (∀r.r->F(r)) (∀r.F(r)->r) is empty. Then there is an isomorphism of types W(a) ≃ (∀r.F(r)->r, a).

  Proof:

  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
  

  Filling up the details of this (which I can post on request) will require a bit of parametricity and Yoneda lemma. When F is not a Fibration (as I defined above), W is trivial as you observed.

  Let us call a fibration a covering if the projection is unique (though I'm not sure if this usage is appropriate).

  Admitting the theorem, you can see W(a) as the coproduct of a's indexed by _all possible fibrations ∀r.F(r)->r, i.e.

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

  In other words, the functor W (as a presheaf on Func(Hask)) takes a fibration and constructs a canonically trivialized covering space from it.

  As an example, let F(a)=(Int,a,a,a). Then we have three evident natural fibrations F(a)->a. Writing the coproduct by +, the following diagram together with the above theorem should hopefully be enough to describe the comonads concretely:

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

  So the counit is unique. Using evident indices into the coproduct, Wε maps (i,j) to j, εW maps (i,j) to i. So δ must be the unique 'diagonal' map, namely δ(i) == (i,i)!

  Theorem 2.

  Let F be a Fibration and let ΩW be the set of all comonads with the underlying functor W. Then ΩW≃1.

  (Sorry I have not formalized the proof.)

  An analogous combinatorial argument for the set of monads ΜW would be interesting too, but in this case ΜW may not be a singleton. (Take some constant c and set η:1->c and μ(i,j)=i+j-c.)

  Note that the monads/comonads so constructed are not the duals to the original comonads/monads in general. For instance let M be a monad (F(a)=(Int,a), η(x) = (0,x), μ(n,(m,x)) = (n+m,x)), i.e. a Writer. The natural projection is unique hence by the theorem W(a)≃a, and there is no way to respect the original algebra.

  Note also that a comonad is trivially a Fibration (in possibly many different ways) unless Void, which is why you got a Monad from a Comonad (but that's not necessarily unique!).

  A few comments about your observations:

  • Dual IO a is essentially Void

    As far as I know, in Haskell IO is defined something like:

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

    which means from the type theory alone the corresponding covering is_ the unique canonical covering space indexed by all State# RealWorlds. Whether you can (or should) reject this is probably a philosophical, rather than a technical question.

  • MonadPlus m => Dual m a is Void

    Right, but do note that if F(a)=0 then W(a)=1 and it's not a comonad (because otherwise the counit would imply the type W(0)->0 ≃ 1->0). This is the only case where W can not even be a trivial comonad given an arbitrary functor.

  • Dual Reader is.. Those statements will sometimes be correct, sometimes not. Depends on whether the (co)algebra of interest agrees with the (bi)algebra of coverings.

  So I'm surprised how interestingly geometric Haskell really is! I guess there may be very many geometric constructions similar to this. For example a natural generalization of this would be to consider the 'canonical trivialization' of F->G for some covariant functors F,G. Then the automorphism group for the base space would no longer be trivial, so a bit more theory would be required to properly understand this.

  Finally, here's a proof of concept code. Thanks for a great refreshing puzzle, and have a very merry Christmas ;-)

  {-# 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
  

  这篇关于你能基于Monads来定义`Comonads`吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！