Можете ли вы определить `Comonads` на основе` Monads`?

Question

Итак, допустим, у вас есть тип

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

Как выясняется, когда f является комонадой, Dual f является Монада (упражнение). Работает ли это наоборот?

Вы можете определить 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

Да, на самом деле любой функтор дает уникальный comonad таким образом, если f == 0.

Позвольте F быть эндофуктором на Hask. Пусть

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

Загадка становится геометрической/комбинаторной в природе, как только вы понимаете, следующий изоморфизм:

Теоремы 1.

Пусть ни один из типов (∀rr-> F (г)) (∀rF (г) -> г) пуст. Тогда существует изоморфизм типов 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 

Заполнение детали этого (которые я могу разместить по запросу) потребует немного parametricity и Йонеды леммы. Когда F не является расслоением (как я определил выше), W тривиально, как вы заметили.

Будем называть расслоение накрытием, если проекция является уникальной (хотя я не уверен, что это использование подходит).

Допуская теорему, вы можете увидеть W (а), как копроизведением индексируется по _all возможных расслоениям ∀rF (г) -> г, т.е.

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

Другими словами, функтор W (как предпучок на Func (Hask)) принимает расслоение и строит на нем канонически тривиализованное накрывающее пространство.

В качестве примера предположим, что F (a) = (Int, a, a, a). Тогда мы имеем три очевидных естественных расслоения F (a) -> a. Запись копроизведения на +, следующая диаграмма вместе с приведенной выше теоремы следует надеяться, будет достаточно, чтобы описать comonads конкретно:

  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 - расслоение, ΩW - множество всех комонад с основополагающим функтором W. Тогда ΩW≃1.

(К сожалению, я не формализованное доказательство.)

Аналогичный комбинаторный аргумент для множества монад мкВт было бы тоже интересно, но в этом случае мкВт не может быть синглтон. (Возьмем некоторую константу с и установить п: 1-> с и М (I, J) = г + х.)

Обратите внимание, что монады/comonads сконструированы является не двойственных к оригинальным comonads/монад в целом. Например, пусть M является монадой (F (a) = (Int, a), η (x) = (0, x), μ (n, (m, x)) = (n + m, x)) , т.е. Writer. Естественная проекция единственна, следовательно, по теореме W (a) ≃a, и нет возможности уважать исходную алгебру.

Обратите внимание также, что comonad тривиально является Fibration (возможно, многими разными способами), если только Void, поэтому вы получили Monad от Comonad (но это не обязательно уникально!).

Несколько комментариев о своих наблюдениях:

• 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 (а) = 0, то W (а) = 1, и это не комонада (потому что в противном случае коединица будет означать тип W (0) -> 0 ≃ 1-> 0). Это единственный случай, когда W не может быть даже тривиальной комонадой, заданной произвольным функтором.

• Dual Reader is .. Эти утверждения иногда бывают правильными, иногда нет. Зависит от того, согласуется ли (со) алгебра с алгеброй (bi) покрытий.

Так что я удивлен, насколько интересен геометрический 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