¿Cómo factorizar la mónada de continuación en adjuntos izquierdo y derecho?

11

Como State mónada se puede factorizar en Producto (Izquierda - Functor) y Lector (Derecha - Representable).

  1. ¿Hay alguna manera de factorizar la Mónada de Continuación? El siguiente código es mi intento, que no escribirá cheque
-- To form a -> (a -> k) -> k
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, InstanceSigs, TypeSynonymInstances #-}
type (<-:) o i = i -> o
-- I Dont think we can have Functor & Representable for this type synonym

class Isomorphism a b where
   from :: a -> b
   to :: b -> a

instance Adjunction ((<-:) e) ((<-:) e) where
   unit :: a -> (a -> e) -> e
   unit a handler = handler a

   counit :: (a -> e) -> e -> a
   counit f e = undefined -- If we have a constraint on Isomorphism a e then we can implement this

  1. ¿Existe una lista de adjuntos de izquierda y derechos que forman mónadas?

  2. He leído que, dados un par de adjuntos, forman una mónada y una comonad únicas, pero, dada una mónada, se puede factorizar en múltiples factores. ¿Hay algún ejemplo de esto?

haskell monads continuations category-theory comonad Pawan Kumar
fuente

Respuestas:

11

Esto no marca la verificación porque la clase Adjunctionsolo representa un pequeño subconjunto de adjuntos, donde ambos functores son endofunctores en Hask .

Resulta que este no es el caso para el adjunto (<-:) r -| (<-:) r. Aquí hay dos functores sutilmente diferentes:

  • f = (<-:) r, el functor de Hask a Op (Hask) (la categoría opuesta de Hask, a veces también denotada Hask ^ op)
  • g = (<-:) r, el functor de Op (Hask) a Hask

En particular, counitdebería ser una transformación natural en la categoría Op (Hask), que mueve las flechas:

unit   :: a -> g (f a)
counit :: f (g a) <-: a

De hecho, counitcoincide con uniteste adjunto.

Para capturar esto correctamente, necesitamos generalizar las clases Functory Adjunctionpara poder modelar adjuntos entre diferentes categorías:

class Exofunctor c d f where
  exomap :: c a b -> d (f a) (f b)

class
  (Exofunctor d c f, Exofunctor c d g) =>
  Adjunction
    (c :: k -> k -> Type)
    (d :: h -> h -> Type)
    (f :: h -> k)
    (g :: k -> h) where
  unit :: d a (g (f a))
  counit :: c (f (g a)) a

Luego obtenemos nuevamente que Composees una mónada (y una comonad si volteamos el adjunto):

newtype Compose f g a = Compose { unCompose :: f (g a) }
adjReturn :: forall c f g a. Adjunction c (->) f g => a -> Compose g f a
adjReturn = Compose . unit @_ @_ @c @(->)

adjJoin :: forall c f g a. Adjunction c (->) f g => Compose g f (Compose g f a) -> Compose g f a
adjJoin = Compose . exomap (counit @_ @_ @c @(->)) . (exomap . exomap @(->) @c) unCompose . unCompose

y Contes simplemente un caso especial de eso:

type Cont r = Compose ((<-:) r) ((<-:) r)

Consulte también este resumen para obtener más detalles: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

He leído que, dado un par de adjuntos, forman una mónada y una comonad únicas, pero si se le da una mónada, se puede factorizar en múltiples factores. ¿Hay algún ejemplo de esto?

La factorización generalmente no es única. Una vez que haya generalizado los adjuntos como se mencionó anteriormente, puede al menos factorizar cualquier mónada Mcomo un adjunto entre su categoría Kleisli y su categoría base (en este caso, Hask).

Every monad M defines an adjunction
  F -| G
where

F : (->) -> Kleisli M
  : Type -> Type                -- Types are the objects of both categories (->) and Kleisli m.
                                -- The left adjoint F maps each object to itself.
  : (a -> b) -> (a -> M b)      -- The morphism mapping uses return.

G : Kleisli M -> (->)
  : Type -> Type                -- The right adjoint G maps each object a to m a
  : (a -> M b) -> (M a -> M b)  -- This is (=<<)

No sé si la mónada de continuación corresponde a un complemento entre endofunctores en Hask.

Consulte también el artículo de nCatLab sobre mónadas: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

Relación con adjunciones y monadicidad.

Cada adjunto (L ⊣ R) induce una mónada R∘L y una comonad L∘R. En general, hay más de un complemento que da lugar a una mónada determinada de esta manera, de hecho, hay una categoría de adjuntos para una mónada determinada. El objeto inicial en esa categoría es el complemento sobre la categoría Kleisli de la mónada y el objeto terminal es sobre la categoría de álgebras de Eilenberg-Moore. (por ejemplo, Borceux, vol. 2, prop. 4.2.2) Este último se llama adjunto monádico.

Li-yao Xia
fuente