Differenza tra monadi liberi e punti fissi dei funtori?

Question

Stavo leggendo http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html dove un albero sintassi astratto è derivato come la monade libera di un functor che rappresenta un insieme di istruzioni. Ho notato che la monad gratuita Free non è molto diversa dall'operatore del fixpoint sui funtori Fix.

L'articolo utilizza le operazioni monad e la sintassi do per creare questi AST (punti fissi) in modo conciso. Mi chiedo se questo è l'unico vantaggio dall'istanza monad gratuita? Ci sono altre interessanti applicazioni che abilita?

Answer 1

(NB questo combina un po 'da entrambi mio e @ commenti di Gabriel sopra.)

E' possibile per ogni abitante del punto Fix ed di un Functor essere infinita, cioè let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...)))) è l'solo abitante Fix Identity. Free differisce immediatamente da Fix in quanto garantisce almeno finito abitante di Free f. Infatti, se Fix f ha abitanti infiniti allora lo Free f ha infiniti abitanti finiti.

Un altro effetto collaterale immediato di questa sconfinatezza è che Functor f => Fix f non è più un Functor. Avremmo bisogno di implementare fmap :: Functor f => (a -> b) -> (f a -> f b), ma Fix ha "riempito tutti i buchi" in f a che conteneva il a, quindi non abbiamo più alcun a s per applicare la nostra funzione fmap a.

Questo è importante per la creazione di Monad s perché vorremmo implementare return :: a -> Free f a e hanno, per esempio, questa legge tenere fmap f . return = return . f, ma non ha nemmeno senso in un Functor f => Fix f.

Quindi, come fa Free "correggere" questi punti deboli Fix punto? "Aumenta" il nostro functor di base con il costruttore Pure. Pertanto, per tutti gli Functor f, Pure :: a -> Free f a. Questo è il nostro abitante del tipo garantito-to-be-finito. Inoltre, ci dà immediatamente una definizione ben fatta di return.

return = Pure 

Così si potrebbe pensare a questa aggiunta come tirando fuori "albero" potenzialmente infinito di annidate Functor s create da Fix e mescolando in un certo numero di "viventi" gemme, rappresentati da Pure. Creiamo nuovi boccioli usando return che potrebbe essere interpretato come una promessa di "tornare" al bocciolo in seguito e aggiungere più calcoli. In effetti, questo è esattamente ciò che fa flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b). Data una funzione di "continuazione" f :: a -> Free f b che può essere applicata ai tipi a, riconsegniamo il nostro albero restituendo a ogni Pure a e sostituendolo con la continuazione calcolata come f a. Questo ci permette di "crescere" il nostro albero.

---

Ora, Free è chiaramente più generale di Fix. Per guidare questa casa, è possibile vedere qualsiasi tipo Functor f => Fix f come sottotipo del corrispondente Free f a! Basta scegliere dove abbiamo data Void = Void Void (cioè, un tipo che non può essere costruito, è il tipo vuoto, non ha istanze).

Per renderlo più chiaro, siamo in grado di rompere i nostri Fix 'D Functor s con break :: Fix f -> Free f a e quindi provare a invertire con affix :: Free f Void -> Fix f.

break (Fix f) = Free (fmap break f) 
affix (Free f) = Fix (fmap affix f) 

Nota prima che affix non ha bisogno di gestire il caso Pure x perché in questo caso x :: Void e, quindi, non può davvero essere lì, così Pure x è assurdo e ci limiteremo a ignorarlo.

Si noti inoltre che tipo di ritorno break s' è un po' sottile, in quanto il tipo a appare solo nel tipo di ritorno, Free f a, in modo tale che è completamente inaccessibile a qualsiasi utente di break. "Completamente inaccessibile" e "non può essere istanziato" ci danno il primo suggerimento che, nonostante i tipi, affix e break sono inversi, ma possiamo solo dimostrarlo.

(break . affix) (Free f) 
===          [definition of affix] 
break (Fix (fmap affix f)) 
===          [definition of break] 
Free (fmap break (fmap affix f)) 
===          [definition of (.)] 
Free ((fmap break . fmap affix) f) 
===          [functor coherence laws] 
Free (fmap (break . affix) f) 

che dovrebbe mostrare (co-induttivo, o semplicemente intuitivamente, forse) che (break . affix) è un'identità. L'altra direzione passa in modo completamente identico.

Quindi, si spera che questo mostri che Free f è più grande di Fix f per tutti Functor f.

---

Quindi perché usare mai Fix? Bene, a volte si desidera solo le proprietà di Free f Void a causa di alcuni effetti collaterali della stratificazione di f s. In questo caso, chiamandolo Fix f è più chiaro che non dovremmo provare a (>>=) o fmap per il tipo. Inoltre, poiché Fix è solo un newtype potrebbe essere più facile per il compilatore "compilare" i livelli di Fix in quanto svolge comunque solo un ruolo semantico.

---

• Nota: possiamo più formalmente parlare di come Void e forall a. a sono tipi isomorfi al fine di vedere più chiaramente come i tipi di affix e break sono armoniosi. Ad esempio, abbiamo absurd :: Void -> a come absurd (Void v) = absurd v e unabsurd :: (forall a. a) -> Void come unabsurd a = a. Ma questi diventano un po 'sciocchi.

Answer 2

C'è una connessione profonda e 'semplice'.

È una conseguenza di adjoint functor theorem, i margini di sinistra conservano gli oggetti iniziali: L 0 ≅ 0.

Categoricamente, Free f è un funtore da una categoria alle sue algebre F (Free f viene lasciato associato a un functor smemorato andando nell'altro senso "round).Lavorare in Hask nostro algebra iniziale è Void

Free f Void ≅ 0 

e l'algebra iniziale nella categoria di F-algebre è Fix f: Free f Void ≅ Fix f

import Data.Void 
import Control.Monad.Free 

free2fix :: Functor f => Free f Void -> Fix f 
free2fix (Pure void) = absurd void 
free2fix (Free body) = Fix (free2fix <$> body) 

fixToFree :: Functor f => Fix f -> Free f Void 
fixToFree (Fix body) = Free (fixToFree <$> body) 

Allo stesso modo, gli aggiunti a destra (Cofree f, un funtore da Hask alla categoria di F- co algebre) conserva gli oggetti finali: R 1 ≅ 1.

In Hask questo è unità: () e l'oggetto finale di F- co algebre è anche Fix f (coincidono nel Hask) in modo da ottenere: Cofree f() ≅ Fix f

import Control.Comonad.Cofree 

cofree2fix :: Functor f => Cofree f() -> Fix f 
cofree2fix (() :< body) = Fix (cofree2fix <$> body) 

fixToCofree :: Functor f => Fix f -> Cofree f() 
fixToCofree (Fix body) =() :< (fixToCofree <$> body) 

---

Guarda come sono simili le definizioni!

newtype Fix f 
    = Fix (f (Fix f)) 

Fix f è Free f senza variabili.

data Free f a 
    = Pure a 
    | Free (f (Free f a)) 

Fix f è Cofree f con valori fittizi.

data Cofree f a 
    = a <: f (Cofree f a)