Können Sie `Comonads` basierend auf` Monaden` definieren?

Question

Okay, also lassen Sie uns sagen, dass Sie die Art haben

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

Wie sich herausstellt, wenn f ein Comonad ist, Dual f ist eine Monade (Spaß Übung). Funktioniert es umgekehrt?

Sie können fmap ab (Dual da) = Dual $ \fb -> da $ fmap (. ab) fb und extract (Dual da) = da $ return id definieren, aber ich weiß nicht, wie man duplicate oder extend definiert.

Ist das überhaupt möglich? Wenn nicht, was der Beweis gibt es nicht (gibt es eine bestimmte Monad m für die Sie Dual m beweisen können, ist keine comonad)?

Einige Beobachtungen: Dual IO a im Wesentlichen Void ist (und Const Void ist eine gültige Comonad). Dual m a für MonadPlus mistVoid (verwenden Sie einfach dual mzero). Dual Reader ist Env. Dual Writer ist Traced. Dual State ist Store, denke ich.

Answer 1

Ja, in der Tat erzeugt jeder Funktor auf diese Weise eine eindeutige comonad, es sei denn f == 0.

Sei F ein Endofunktor auf Hask. Lassen

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

Das Puzzle wird geometrisch/Kombinatorik in der Natur, wenn Sie den folgenden Isomorphismus realisieren:

Satz 1.

Angenommen, weder die Typen (∀rr-> F (r)) (∀rF (r) -> r) ist leer. Dann gibt es einen Isomorphismus der Typen W (a) ≃ (∀r.F (r) -> r, a).

Beweis:

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 

die Details dieses Auffüllen wird (was ich auf Anfrage veröffentlichen können) ein bisschen Parametrizität und Yoneda Lemma benötigen. Wenn F keine Fibration ist (wie ich oben definiert habe), ist W trivial, wie Sie beobachtet haben.

Nennen wir eine Fibration eine Deckung, wenn die Projektion einzigartig ist (obwohl ich nicht sicher bin, ob diese Verwendung geeignet ist). > R, dh

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

Mit anderen Worten, die Funktors W (-

Zugegeben den Satz, können Sie W (a) als Co-Produkt von a indiziert wird von _alle möglich Faserungen ∀rF (r) sehen als Vorwort auf Func (Hask) nimmt eine Fibration und konstruiert daraus einen kanonisch trivialisierten Bedeckungsraum.

Als Beispiel sei F (a) = (Int, a, a, a). Dann haben wir drei offensichtliche natürliche Fibrationen F (a) -> a. Das Schreiben der coproduct von +, das folgende Diagramm zusammen mit dem obigen Satz sollte hoffentlich genug sein, um die comonads konkret zu beschreiben:

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

So ist die counit einzigartig ist.Unter Verwendung von offensichtlichen Indizes in dem Koprodukt bildet Ws Karten (i, j) mit j, & epsi; W-Karten (i, j) mit i ab. Also muss δ die eindeutige "diagonale" Karte sein, nämlich δ (i) == (i, i)!

Satz 2.

Sei F eine Fibration und sei ΩW die Menge aller Komonaden mit dem darunter liegenden Funktor W. Dann ΩW≃1.

(Leider habe ich den Beweis nicht formalisierte.)

Ein analoges kombinatorisches Argument für den Satz von Monaden uW zu interessant wäre, aber in diesem Fall uW kann kein Singleton sein. (Nehmen eine Konstante c und η eingestellt: 1-> c und μ (i, j) = i + jc).

anzumerken, dass die Monaden/comonads so konstruiert ist nicht duals die zu dem ursprünglichen comonads/Monaden Im Algemeinen. Zum Beispiel sei M eine Monade (F (a) = (Int, a), η (x) = (0, x), μ (n, (m, x)) = (n + m, x)) , dh eine Writer. Die natürliche Projektion ist daher einzigartig durch den Satz W (a) ≃a, und es gibt keine Möglichkeit, die ursprüngliche Algebra zu respektieren.

Beachten Sie auch, dass eine comonad trivialerweise eine Fibration ist (auf viele verschiedene Arten), es sei denn Void, weshalb Sie eine Monad von einem Comonad bekommen haben (aber das ist nicht unbedingt einzigartig!).

Einige Kommentare über Ihre Beobachtungen:

• Dual IO a ist im Wesentlichen Void

  Soweit ich weiß, in Haskell IO definiert ist so etwas wie:

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

  , die von der Einrichtung die Typentheorie allein die entsprechende Bedeckung ist der einzigartige kanonische Bedeckungsraum, der von allen State# RealWorld s indexiert wird. Ob Sie dies ablehnen können (oder sollten), ist wahrscheinlich eher eine philosophische als eine technische Frage.

• MonadPlus m => Dual m a ist Void

  Richtig, aber beachten Sie, dass, wenn F (a) = 0, dann ist W (a) = 1 und es ist kein comonad (weil sonst der counit den Typ W bedeuten würde (0) -> 0 ≃ 1-> 0). Dies ist der einzige Fall, in dem W nicht einmal eine triviale Komonad mit einem beliebigen Funktor sein kann.

• Dual Reader ist .. Diese Aussagen werden manchmal richtig sein, manchmal nicht. Hängt davon ab, ob die (Co-) Algebra von Interesse mit der (Bi-) Algebra von Überdeckungen übereinstimmt.

Ich bin überrascht Wie interessant geometrische Haskell wirklich ist! Ich denke, dass es sehr viele ähnliche geometrische Konstruktionen geben kann. Eine natürliche Verallgemeinerung wäre zum Beispiel die "kanonische Trivialisierung" von F → G für einige kovariante Funktoren F, G. Dann wäre die Automorphismengruppe für den Basisraum nicht mehr trivial, also wäre etwas mehr Theorie erforderlich, um dies richtig zu verstehen.

Schließlich ist hier ein Beweis des Konzeptcodes. Danke für ein tolles erfrischend Puzzle, und hat ein sehr frohes Weihnachten ;-)

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