haskell - programmers - ¿Es esta propiedad de un funtor más fuerte que una mónada?

monad traduccion

Question

Mientras pensaba cómo generalizar las mónadas, se me ocurrió la siguiente propiedad de un functor F:

inject :: (a -> F b) -> F(a -> b) 

- Lo que debería ser una transformación natural tanto en a como en b.

En ausencia de un nombre mejor, llamo al functor F enlazable si existe una inject transformación natural que se muestra arriba.

La pregunta principal es si esta propiedad ya se conoce y tiene un nombre, y cómo se relaciona con otras propiedades bien conocidas de los funtores (como, por ejemplo, aplicativo, monádico, puntiagudo, transitable, etc.)

La motivación para el nombre "enlazable" viene de la siguiente consideración: Supongamos que M es una mónada y F es un functor "enlazable". Entonces uno tiene el siguiente morfismo natural:

fbind :: M a -> (a -> F(M b)) -> F(M b)

Esto es similar al "enlace" monádico,

bind :: M a -> (a -> M b) -> M b

Salvo que el resultado esté decorado con el functor F.

La idea detrás de fbind era que una operación monádica generalizada puede producir no solo un único resultado M b, sino una F "funcional" de tales resultados. Quiero expresar la situación cuando una operación monádica produce varias "hebras de cómputo" en lugar de solo una; cada "hebra de computación" es nuevamente una computación monádica.

Tenga en cuenta que cada functor F tiene el morfismo

eject :: F(a -> b) -> a -> F b

que es contrario a "inyectar". Pero no todo funtor F tiene "inyectar".

Ejemplos de funtores que tienen "inyectar": F t = (t,t,t) o F t = c -> (t,t) donde c es un tipo constante. Los funcionales F t = c (functor constante) o F t = (c,t) no son "vinculables" (es decir, no tienen "inyectar"). El functor de continuación F t = (t -> r) -> r tampoco parece tener inject .

La existencia de "inyectar" se puede formular de una manera diferente. Considere el functor "lector" R t = c -> t donde c es un tipo constante. (Este funtor es aplicativo y monádico, pero eso no viene al caso). La propiedad "inyectar" significa entonces R (F t) -> F (R t) , en otras palabras, que R conmuta con F. Tenga en cuenta que esto no es el mismo que el requisito de que F sea transitable; eso habría sido F (R t) -> R (F t) , que siempre se cumple para cualquier functor F con respecto a R.

Hasta ahora, pude demostrar que "inyectar" implica "fbind" para cualquier mónada M.

Además, demostré que cada functor F que tiene "inyectar" también tendrá estas propiedades adicionales:

• es puntiagudo

point :: t -> F t

• Si F es "unible" y es aplicativo, entonces F es también una mónada.

• si F y G son "enlazables", entonces también lo es el functor de pares F * G (pero no F + G)

• si F es "vinculable" y A es cualquier profunctor, entonces el (pro) functor G t = A t -> F t es vinculable

• El functor de identidad es vinculable.

Preguntas abiertas:

• ¿Es la propiedad de ser "vinculable" equivalente a algunas otras propiedades bien conocidas, o es una propiedad nueva de un functor que generalmente no se considera?

• ¿Existen otras propiedades del functor "F" que se derivan de la existencia de "inyectar"?

• ¿Necesitamos leyes para "inyectar", sería útil? Por ejemplo, podríamos requerir que R (F t) sea isomorfo a F (R t) en una o ambas direcciones.

Answer 1

Para mejorar un poco la terminología, propongo llamar a estos funtores "rígidos" en lugar de "vinculables". La motivación para decir "rígido" se explicará a continuación.

Un functor f se llama rígido si tiene el método de inject como se muestra. Tenga en cuenta que cada functor tiene el método de eject .

class (Functor f) => Rigid f where
  inject :: (a -> f b) -> f(a -> b)

  eject :: f(a -> b) -> a -> f b
  eject fab x = fmap (/ab -> ab x) fab

La ley de "no degeneración" debe contener:

eject . inject = id

Un funtor rígido siempre es puntiagudo:

instance (Rigid f) => Pointed f where
  point :: t -> f t
  point x = fmap (const x) (inject id)

Si un funtor rígido es aplicativo, entonces es automáticamente monádico:

instance (Rigid f, Applicative f) => Monad f where
  bind :: f a -> (a -> f b) -> f b
  bind fa afb = (inject afb) <*> fa

La propiedad de ser rígido no es comparable (ni más débil ni más fuerte) que la de ser monádico: si un funtor es rígido, no parece seguir que es automáticamente monádico (aunque no conozco contraejemplos específicos para este caso). ). Si un funtor es monádico, no se sigue que sea rígido (hay contraejemplos).

Los contraejemplos básicos de los funtores monádicos que no son rígidos son Maybe y List . Estos son los funtores que tienen más de un constructor: como regla, tales funtores no son rígidos.

El problema con la implementación de inject para Maybe es que inject debe transformar una función de tipo a -> Maybe b en Maybe(a -> b) mientras que Maybe tiene dos constructores. Una función de tipo a -> Maybe b podría devolver diferentes constructores para diferentes valores de a . Sin embargo, se supone que debemos construir un valor de tipo Maybe(a -> b) . Si para algunos la función dada produce Nothing , no tenemos una b por lo que no podemos producir una función total a->b . Por lo tanto, no podemos devolver Just(a->b) ; estamos obligados a devolver Nothing mientras la función dada produzca Nothing incluso para un valor de a . Pero no podemos verificar que una función dada de tipo a -> Maybe b produce Just(...) para todos los valores de a . Por lo tanto estamos obligados a devolver Nothing en todos los casos. Esto no cumplirá con la ley de la no degeneración.

Por lo tanto, podemos implementar inject si ft es un contenedor de "forma fija" (que tiene un solo constructor). De ahí el nombre de "rígido".

Otra explicación de por qué la rigidez es más restrictiva que la monadicidad es considerar la expresión definida naturalmente.

(inject id) :: f(f a -> a) 

donde id :: fa -> fa . Esto muestra que podemos tener un f-algebra fa -> a para cualquier tipo a , siempre que esté dentro de f . No es cierto que cualquier mónada tenga un álgebra; por ejemplo, las diversas mónadas "futuras", así como la mónada IO describen cálculos del tipo fa que no nos permiten extraer valores del tipo a ; no deberíamos poder tener un método del tipo fa -> a incluso si Envuelto dentro de un f -contenedor. Esto demuestra que las mónadas "futuras" y la mónada IO no son rígidas.

Una propiedad que es estrictamente más fuerte que la rigidez es la distributividad de uno de los paquetes de E. Kmett. Un functor f es distributivo si podemos intercambiar el orden como en p (ft) -> f (pt) para cualquier functor p . La rigidez es lo mismo que poder intercambiar la orden solo con respecto al functor "lector" rt = a -> t . Por lo tanto, todos los functores distributivos son rígidos.

Todos los functores distributivos son necesariamente representables, lo que significa que son equivalentes al functor "lector" c -> t con algún tipo fijo c . Sin embargo, no todos los funtores rígidos son representables. Un ejemplo es el functor g definido por

type g t = (t -> r) -> t

El functor g no es equivalente a c -> t con un tipo fijo c .

Otros ejemplos de funtores rígidos que no son representables (es decir, no son "distributivos") son funtores de la forma at -> ft donde a es cualquier contrafunctor f es un funtor rígido. Además, el producto cartesiano y la composición de dos funtores rígidos también son rígidos. De esta manera, podemos producir muchos ejemplos de funtores rígidos dentro de la clase de functors exponencial-polinomial.

Mi respuesta a ¿Cuál es el caso general de la función de promoción de QuickCheck? También enumera las construcciones de funtores rígidos.

Finalmente, encontré dos casos de uso para funtores rígidos.

El primer caso de uso fue la motivación original para considerar los funtores rígidos: nos gustaría devolver varios resultados monádicos a la vez. Si m es una mónada y queremos tener fbind como se muestra en la pregunta, necesitamos que f sea ​​rígido. Entonces podemos implementar fbind como

fbind :: m a -> (a -> f (m b)) -> f (m b)
fbind ma afmb = fmap (bind ma) (inject afmb)

Podemos usar fbind para realizar operaciones monádicas que devuelven más de un resultado monádico (o, más en general, un funcionamiento rígido de resultados monádicos), para cualquier mónada m .

El segundo caso de uso surge de la siguiente consideración. Supongamos que tenemos un programa p :: a que utiliza internamente una función f :: b -> c . Ahora, notamos que la función f es muy lenta, y nos gustaría refactorizar el programa reemplazando f con un "futuro" o "tarea" monádica, o generalmente con una flecha de Kleisli f'' :: b -> mc para algunos mónada m . Nosotros, por supuesto, esperamos que el programa p se vuelva monádico: p'' :: ma . Nuestra tarea es refactorizar p en p'' .

La refactorización se realiza en dos pasos: primero, refactorizamos el programa p para que la función f sea ​​explícitamente un argumento de p . Supongamos que esto se ha hecho, de modo que ahora tenemos p = qf donde

q :: (b -> c) -> a

Segundo, reemplazamos f por f'' . Ahora asumimos que q y f'' se dan. Nos gustaría construir el nuevo programa q'' del tipo.

q'' :: (b -> m c) -> m a

de modo que p'' = q'' f'' . La pregunta es si podemos definir un combinador general que refactorice q en q'' ,

refactor :: ((b -> c) -> a) -> (b -> m c) -> m a

Resulta que el refactor se puede construir si m es un funtor rígido. Al tratar de implementar refactor , encontramos esencialmente el mismo problema que cuando intentamos implementar inject para Maybe : tenemos una función f'' :: b -> mc que podría devolver diferentes efectos monádicos mc para diferentes b , pero se nos exige para construir ma , que debe representar el mismo efecto monádico para todos b . Esto no puede funcionar, por ejemplo, si m es una mónada con más de un constructor.

Si m es rígido (y no es necesario que m sea ​​una mónada), podemos implementar refactor :

refactor bca bmc = fmap bca (inject bmc)

Si m no es rígido, no podemos refactorizar programas arbitrarios. Hasta ahora hemos visto que la mónada de continuación es rígida, pero las mónadas de "futuro" y la mónada IO no son rígidas. Esto demuestra una vez más que la rigidez es, en cierto sentido, una propiedad más fuerte que la monadicidad.