haskell - religion - principio de leibniz

Son todos los tipos diferenciables de las mónadas.

Question

Dado un tipo diferenciable , sabemos que su Zipper es un Comonad . En respuesta a esto, Dan Burton preguntó: "Si la derivación hace una coma, ¿significa eso que la integración hace una mónada? ¿O es una tontería?". Me gustaría darle a esta pregunta un significado específico. Si un tipo es diferenciable, ¿es necesariamente una mónada? Una formulación de la pregunta sería preguntar, dadas las siguientes definiciones

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)

¿Podemos escribir funciones con firmas similares a

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

obedeciendo las leyes de la mónada .

En las respuestas a las preguntas vinculadas, hubo dos enfoques exitosos para un problema similar de derivar instancias de Comonad para la Zipper . El primer enfoque fue expandir la clase Diff para incluir el dual de >>= y usar la diferenciación parcial . El segundo enfoque era exigir que el tipo fuera dos o infinitamente diferenciable .

Answer 1

No podemos unsurprising derivar una Monad para algo similar si revertimos absolutamente todo. Nuestra declaración anterior y nuevas declaraciones se encuentran a continuación. No estoy completamente seguro de que la clase definida a continuación sea realmente integración, por lo que no me referiré explícitamente como tal.

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

Primero definiremos lo opuesto a una Zipper , una Unzipper . En lugar de un producto será una suma.

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

Un Unzipper es un Functor mientras D'' t sea ​​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)

Si recordamos la clase 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)

La clase de cosas opuestas a ella, Diff'' , es la misma pero con cada instancia de Zipper reemplazada con Unzipper y el orden de las flechas -> invertidas.

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

Si utilizamos mi solución al problema anterior.

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)

Podemos definir el inverso de esa función, que se join para la 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''

Esto nos permite escribir una instancia de Unzipper para Unzipper .

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

Esta instancia está en la misma línea que la instancia de Comonad para la Zipper .

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

Answer 2

No. Los data V a funtor void data V a son diferenciables, pero el return no se puede implementar para ellos.