Como fatorar a mônada de continuação em adjuntos esquerdo e direito?

11

Como a mônada do estado pode ser fatorada em Produto (Esquerdo - Functor) e Leitor (Direito - Representável).

  1. Existe uma maneira de fatorar a Mônada de Continuação? Abaixo o código é a minha tentativa, que não digita check
-- 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 uma lista de adjuntos de esquerda e direitos que formam mônadas?

  2. Li que, dado um par de adjuntos, eles formam uma única Mônada e Comonada, mas, dada uma Mônada, ela pode ser fatorada em múltiplos fatores. Existe algum exemplo disso?

haskell monads continuations category-theory comonad Pawan Kumar
fonte

Respostas:

11

Isso não verifica tipicamente porque a classe Adjunctionrepresenta apenas um pequeno subconjunto de adjunções, em que os dois functores são endofunitores no Hask .

Como se vê, esse não é o caso da adjunção (<-:) r -| (<-:) r. Existem dois functores sutilmente diferentes aqui:

  • f = (<-:) r, o functor de Hask a Op (Hask) (a categoria oposta de Hask, às vezes também denominada Hask ^ op)
  • g = (<-:) r, o functor de Op (Hask) para Hask

Em particular, counitdeve haver uma transformação natural na categoria Op (Hask), que gira as setas:

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

De fato, counitcoincide com unitesta adjunção.

Para capturar isso corretamente, precisamos generalizar as classes Functore Adjunctionpara modelar adjuntos entre diferentes categorias:

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

Em seguida, obtemos novamente que Composeé uma mônada (e uma comonada se ativarmos a adjunção):

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

e Conté apenas um caso especial disso:

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

Consulte também esta lista para obter mais detalhes: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

Li que, dado um par de adjuntos, eles formam uma única Mônada e Comonada, mas, dada uma Mônada, ela pode ser fatorada em múltiplos fatores. Existe algum exemplo disso?

A fatoração geralmente não é única. Depois de generalizar as adjunções como acima, você pode pelo menos fatorar qualquer mônada Mcomo uma adjunção entre sua categoria Kleisli e sua categoria base (neste 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 (=<<)

Não sei se a mônada de continuação corresponde a um complemento entre os endofuncores em Hask.

Consulte também o artigo nCatLab sobre mônadas: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

Relação com adjuntos e monadicidade

Cada adjunção (L ⊣ R) induz uma mônada R∘L e uma comonad L∘R. Em geral, há mais de uma adjunção que dá origem a uma determinada mônada dessa maneira; de fato, há uma categoria de adjunções para uma determinada mônada. O objeto inicial nessa categoria é a adjunção sobre a categoria Kleisli da mônada e o objeto terminal é sobre a categoria de álgebras de Eilenberg-Moore. (por exemplo, Borceux, vol. 2, prop. 4.2.2) Este último é chamado de adjunção monádica.

Li-yao Xia
fonte