Sono tutti tipi differenziabili Monadi

Question

Dato un differentiable type, sappiamo che its Zipper is a Comonad. In risposta a questo, Dan Burton ha chiesto: "Se la derivazione fa una comonade, vuol dire che l'integrazione fa una monade? O è una sciocchezza?". Mi piacerebbe dare a questa domanda un significato specifico. Se un tipo è differenziabile, è necessariamente una monade? Una formulazione della domanda potrebbe essere quella di chiedere, date le seguenti definizioni

data Zipper t a = Zipper { diff :: D t a, here :: a } 

deriving instance Diff t => Functor (Zipper t) 

class (Functor t, Functor (D t)) => Diff t where 
    type D t :: * -> * 
    up :: Zipper t a -> t a 
    down :: t a -> t (Zipper t a) 

possiamo scrivere funzioni con le firme simili a

return :: (Diff t) => a -> t a 
(>>=) :: (Diff t) => t a -> (a -> t b) -> t b 

obbedire alla Monad laws.

Nelle risposte alle domande collegate, c'erano due approcci di successo a un problema simile di derivazione delle istanze Comonad per lo Zipper. Il primo approccio è stato expand the Diff class to include the dual of >>= and use partial differentiation. Il secondo approccio era a require that the type be twice or infinitely differentiable.

Answer 1

No. Il subwoofer data V a è differenziabile, ma per questo non è possibile implementare return.

Answer 2

Possiamo unsurprising ricavare un Monad per qualcosa di simile se invertiamo assolutamente tutto. La nostra dichiarazione precedente e le nuove dichiarazioni sono sotto. Non sono del tutto sicuro che la classe definita di seguito sia effettivamente l'integrazione, quindi non mi riferirò esplicitamente in quanto tale.

 
if D t is the derivative of t then the product of D t and the identity is a Comonad 
if D' t is the ???  of t then the sum  of D' t and the identity is a Monad 

Prima definiremo l'opposto di un Zipper, un Unzipper. Invece di un prodotto sarà una somma.

data Zipper t a = Zipper { diff :: D t a , here :: a } 
data Unzipper t a =   Unzip (D' t a) | There a 

Un Unzipper è un Functor finché D' t è un Functor.

instance (Functor (D' t)) => Functor (Unzipper t) where 
    fmap f (There x) = There (f x) 
    fmap f (Unzip u) = Unzip (fmap f u) 

Se ricordiamo classe Diff

class (Functor t, Functor (D t)) => Diff t where 
    type D t :: * -> * 
    up :: Zipper t a -> t a 
    down :: t a -> t (Zipper t a) 

categoria delle cose opposto ad esso, Diff', è lo stesso ma con ogni istanza di Zipper sostituito con Unzipper e l'ordine delle -> frecce capovolto .

class (Functor t, Functor (D' t)) => Diff' t where 
    type D' t :: * -> * 
    up' :: t a -> Unzipper t a 
    down' :: t (Unzipper t a) -> t a 

Se usiamo la mia solution to the previous problem

around :: (Diff t, Diff (D t)) => Zipper t a -> Zipper t (Zipper t a) 
around z@(Zipper d h) = Zipper ctx z 
    where 
     ctx = fmap (\z' -> Zipper (up z') (here z')) (down d) 

si può definire l'inverso di quella funzione, che sarà join per il Monad.

inside :: (Diff' t, Diff' (D' t)) => Unzipper t (Unzipper t a) -> Unzipper t a 
inside (There x) = x 
inside (Unzip u) = Unzip . down' . fmap f $ u 
    where 
     f (There u') = There u' 
     f (Unzip u') = up' u' 

Questo ci permette di scrivere un'istanza Monad per il Unzipper.

instance (Diff' t, Diff' (D' t)) => Monad (Unzipper t) where 
    return = There 
    -- join = inside 
    x >>= f = inside . fmap f $ x 

Questa istanza è nella stessa vena come istanza Comonad per il Zipper.

instance (Diff t, Diff (D t)) => Comonad (Zipper t) where 
    extract = here 
    duplicate = around