Ogni monade gratis su un ??? il functor produce una comonade?

Question

In "this answer in" Può una monade essere una comonad? " vediamo che

Ogni CofreeComonad su un Alternative functor produce un Monade.

Quale sarebbe il doppio a questo? Esiste una classe di funtori che rendono automaticamente una monade libera su di loro una comonade?

Answer 1

Ebbene sì, è possibile dualizzare la costruzione, ma l'unico membro della classe risultante è il funtore vuoto, la cui monade libera (la monade dell'identità) è effettivamente anche una comonade. Non molto eccitante.

La struttura a cui si fa riferimento in realtà ha bisogno di poco, quindi abbandoniamo il bagaglio di Hask e lavoriamo nella seguente generalità. Diamo

• (C, ⊗, 1) essere una categoria monoidale

• F: C -> C un funtore monoid valori, cioè, ci sono le mappe 1 -> FX e FX ⊗ FX -> FX che sono naturali in X, e unital ed associative

Definire TX = X ⊗ F (TX). Si assuma questa definizione ricorsiva ha un senso in qualche modo e siamo in grado di fare le definizioni ricorsive su T. Poi possiamo fare T in una monade con le seguenti mappe di struttura:

• unità data dal

  X = X ⊗ 1 
      -> X ⊗ F(TX)   [unit map of F] 
       = TX 
  

• join data da

  T(TX) = TX ⊗ F(TTX) 
       = X ⊗ F(TX) ⊗ F(TTX) 
      -> X ⊗ F(TX) ⊗ F(TX) [join recursively under F] 
      -> X ⊗ F(TX)   [multiplication of F] 
       = TX 
  

Quando ⊗ è il prodotto cartesiano, questa costruzione è il m struttura onad sulla comonad libera su un funtore alternativo a cui ti riferisci. In effetti, la parte Applicativa della struttura alternativa è irrilevante. Sono necessari solo i metodi di classe di Alternativa stessa (più Functor): un funtore con valori monoide. Elemento-saggio, le fasi che compongono aderire come sopra descritto sono in

(x :< xs) :< xss -> (x :< xs, xss) 
        -> (x, xs, xss) 
        -> (x, xs, fmap join xss) 
        -> (x, xs <|> fmap join xss) 
        -> x :< (xs <|> fmap join xss) 

e questo è facilmente visibile (impostando k = id) a concordare con

(a :< m) >>= k = case k a of 
        b :< n -> b :< (n <|> fmap (>>= k) m) 

Poiché la nostra struttura iniziale era talmente minima , è facilmente dualizzato. Quindi cerchiamo (C, ⊗, 1) continuerà ad essere una categoria monoidale ma ora assumere

• G: C -> C un funtore comonoid valori, cioè, ci sono le mappe GX -> 1 e GX -> GX ⊗ GX che sono naturali in X, e counital e coassociative

Quindi possiamo definire UX = X ⊗ G (UX) (nuovamente supponendo che questo rende in qualche modo senso) e doppi costruzioni dotare U con la struttura una comonade. Questa è in un certo senso la vera risposta qui, ma per rispondere alla tua domanda specifica dovremmo considerare cosa succede per alcune scelte concrete di ⊗.

In primo luogo, ⊗ è ancora il prodotto cartesiano. Quindi ogni funtore G è valutato in modo univoco in un modo unico (le forze di conteggio GX -> GX x GX sono le diagonali). Quindi, per qualsiasi functor G, otteniamo un risultato UX = X x G (UX). In realtà questo si rivela solo il solito cofree comonad su una costruzione di functor (che giustifica la parte "cofree comonad" del tuo slogan, quando F è monovalore possiamo impostare G = F e G è automaticamente a valore comoide, e quindi T e U hanno lo stesso functor sottostante).

Dually se ⊗ è il coprodotto ⨿ allora qualsiasi G che è comonoidal valori per ⨿ è anche monoidale valori per ⨿ in modo unico, così UX = X ⨿ G (UX) è anche la monade libera su G come oltre ad essere una comonade.

Ma in Hask l'oggetto unità per ⨿ è il tipo vuoto 0, e il conteggio di G deve avere tipo GX -> 0, che è possibile solo quando GX = 0 per tutto X (questo è vero in qualsiasi categoria chiusa cartesiana). Quindi, non ci sono esempi interessanti di questa costruzione in Hask. Questa mancanza di simmetria è un tipico fenomeno di categorie che assomigliano a Set.