haskell - ¿Puedes definir `Comonads` basado en` Monads`?

transform

Question

Bien, digamos que tienes el tipo

newtype Dual f a = Dual {dual :: forall r. f(a -> r)->r}

Resulta que cuando f es un Comonad, Dual f es una Mónada (ejercicio divertido). ¿Funciona al revés?

Puede definir fmap ab (Dual da) = Dual $ /fb -> da $ fmap (. ab) fb y extract (Dual da) = da $ return id , pero no sé cómo definir duplicate o extend .

¿Esto es posible? Si no, ¿cuál es la prueba de que no existe (hay una Mónada particular para la cual puede probar que Dual m no es una comuna)?

Algunas observaciones: Dual IO a es esencialmente Void (y Const Void es un Comonad válido). Dual ma para MonadPlus m es Void (solo use dual mzero ). Dual Reader es Env . Dual Writer . Dual State es Store , creo.

Answer 1

Sí, de hecho, cualquier functor da lugar a una combinación única de esta manera, a menos que f == 0.

Dejemos que F sea un endofunctor en Hask. Dejar

W(a) = ∀r.F(a->r)->r
W(f) = F(f∗)∗
where g∗(h) = h∘g

El rompecabezas se vuelve de naturaleza geométrica / combinatoria una vez que te das cuenta del siguiente isomorfismo:

Teorema 1.

Supongamos que ninguno de los tipos (∀rr-> F (r)) (∀rF (r) -> r) está vacío. Luego hay un isomorfismo de los tipos W (a) ≃ (∀rF (r) -> r, a).

Prueba:

class Functor f => Fibration f where
projection :: ∀r. f(r)->r
some_section :: ∀r. r->f(r) -- _any_ section will work
to :: forall f a. Fibration f
=> (∀r.f(a->r) -> r)
-> (∀r.f(r)->r, a)
to(f) = ( f . fmap const
, f(some_section(id)))
from :: forall f a. Fibration f
=> (∀r.f(r)->r, a)
-> (∀r.f(a->r) -> r)
from (π,η) = ev(η) . π
ev :: a -> (a->b) -> b
ev x f = f x

Completar los detalles de esto (que puedo publicar a petición) requerirá un poco de parametricidad y lema de Yoneda. Cuando F no es una fibración (como lo definí anteriormente), W es trivial como observaste.

Llamemos cobertura a una fibración si la proyección es única (aunque no estoy seguro de si este uso es apropiado).

Admitiendo el teorema, puede ver W (a) como el coproducto de a indexado por todas las fibraciones posibles ∀rF (r) -> r, es decir

W(a) ≃ ∐a
π::∀f.F(r)->r

En otras palabras, el functor W (como presheaf en Func (Hask)) toma una fibración y construye un espacio de cobertura canónico trivializado a partir de él.

Como ejemplo, vamos a F (a) = (Int, a, a, a). Entonces tenemos tres fibraciones naturales evidentes F (a) -> a. Al escribir el coproducto por +, el siguiente diagrama junto con el teorema anterior debería ser suficiente para describir los puntos en concreto:

 a
^
| ε
|
a+a+a
^ | ^
Wε | |δ | εW
| v |
(a+a+a)+(a+a+a)+(a+a+a)

Así que el consejo es único. Usando índices evidentes en el coproducto, los mapas Wε (i, j) a j, εW mapean (i, j) a i. Entonces δ debe ser el único mapa ''diagonal'', a saber δ (i) == (i, i)!

Teorema 2.

Sea F una fibración y sea ΩW el conjunto de todas las comillas con el functor subyacente W. Entonces ΩW≃1.

(Lo siento, no he formalizado la prueba.)

Un argumento combinatorio análogo para el conjunto de mónadas ΜW también sería interesante, pero en este caso ΜW puede no ser un singleton. (Tome alguna constante c y establezca η: 1-> c y μ (i, j) = i + jc.)

Tenga en cuenta que las mónadas / comónadas así construidas no son las duales de las comonadas / mónadas originales en general. Por ejemplo, sea M una mónada (F (a) = (Int, a), η (x) = (0, x), μ (n, (m, x)) = (n + m, x)), es decir, un Writer . La proyección natural es única, por lo tanto, según el teorema W (a) ≃a, y no hay manera de respetar el álgebra original.

Tenga en cuenta también que un Comonad es trivialmente una Fibración (posiblemente de muchas formas diferentes) a menos que sea Void , por lo que obtuvo una Monad de un Comonad (¡pero eso no es necesariamente único!).

Algunos comentarios sobre tus observaciones:

• Dual IO a es esencialmente vacío

  Por lo que sé, en Haskell IO se define algo como:

   -- ghc/libraries/ghc-prim/GHC/Types.hs
  newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

  lo que significa que solo a partir de la teoría de tipos, la cobertura correspondiente es el único espacio canónico de cobertura indexado por todos los State# RealWorld s. Si puede (o debería) rechazar esto es probablemente una cuestión filosófica, en lugar de una cuestión técnica.

• MonadPlus m => Dual ma es nulo

  Correcto, pero tenga en cuenta que si F (a) = 0, entonces W (a) = 1 y no es una coma (porque de lo contrario el país implicaría el tipo W (0) -> 0 ≃ 1-> 0). Este es el único caso en el que W ni siquiera puede ser una combinación trivial dado un funtor arbitrario.

• Dual Reader es ... Esas declaraciones serán a veces correctas, a veces no. Depende de si el (co) álgebra de interés está de acuerdo con el (bi) álgebra de coberturas.

¡Así que me sorprende lo interesante que es realmente Haskell geométrico! Supongo que puede haber muchas construcciones geométricas similares a esto. Por ejemplo, una generalización natural de esto sería considerar la "trivialización canónica" de F-> G para algunos funtores covariantes F, G. Entonces, el grupo de automorfismo para el espacio base ya no sería trivial, por lo que se requeriría un poco más de teoría para entender esto correctamente.

Finalmente, aquí hay un código de prueba de concepto. Gracias por un gran rompecabezas refrescante, y que tengan una muy feliz Navidad ;-)

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Control.Comonad
class Functor f => Fibration f where
x0 :: f ()
x0 = some_section ()
some_section :: forall r. r -> f(r)
some_section x = fmap (const x) x0
projection :: forall r. f(r) -> r
newtype W f a = W { un_w :: forall r. f(a->r)->r }
instance Functor f => Functor (W f) where
fmap f (W c) = W $ c . fmap (. f)
instance Fibration f => Comonad (W f) where
extract = ε
duplicate = δ
-- The counit is determined uniquely, independently of the choice of a particular section.
ε :: forall f a. Fibration f => W f a -> a
ε (W f) = f (some_section id)
-- The comultiplication is unique too.
δ :: forall f a. Fibration f => W f a -> W f (W f a)
δ f = W $ ev(f) . un_w f . fmap const
ev :: forall a b. a -> (a->b)->b
ev x f = f x
-- An Example
data Pair a = P {p1 ::a
,p2 :: a
}
deriving (Eq,Show)
instance Functor Pair where
fmap f (P x y) = P (f x) (f y)
instance Fibration Pair where
x0 = P () ()
projection = p1
type PairCover a = W Pair a
-- How to construct a cover (you will need unsafePerformIO if you want W IO.)
cover :: a -> W Pair a
cover x = W $ ev(x) . p1