Ini tidak melakukan checkecheck karena kelas Adjunction
hanya mewakili sebagian kecil dari adjunctions, di mana kedua functors adalah endofunctors pada Hask .
Ternyata, ini bukan kasus untuk tambahan (<-:) r -| (<-:) r
. Ada dua fungsi yang agak berbeda di sini:
f = (<-:) r
, functor dari Hask ke Op (Hask) (kategori berlawanan dari Hask, terkadang juga dilambangkan dengan Hask ^ op)
g = (<-:) r
, functor dari Op (Hask) ke Hask
Secara khusus, counit
harus menjadi transformasi alami dalam kategori Op (Hask), yang membalik panah di sekitar:
unit :: a -> g (f a)
counit :: f (g a) <-: a
Bahkan, counit
bertepatan dengan unit
dalam pertemuan ini.
Untuk menangkap ini dengan benar, kita perlu menggeneralisasi Functor
dan Adjunction
kelas sehingga kita dapat memodelkan tambahan di antara berbagai kategori:
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
Lalu kita dapatkan lagi itu Compose
adalah monad (dan comonad jika kita membalik adjuncion):
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
dan Cont
hanyalah kasus khusus dari itu:
type Cont r = Compose ((<-:) r) ((<-:) r)
Lihat juga intisari ini untuk detail lebih lanjut: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64
Saya telah membaca bahwa mengingat sepasang adjoints mereka membentuk Monad & Comonad yang unik tetapi diberi Monad dapat difaktorisasi menjadi beberapa Faktor. Apakah ada contohnya?
Faktorisasi umumnya tidak unik. Setelah Anda menggeneralisasi adjunctions seperti di atas, maka Anda setidaknya dapat M
memfaktorkan monad apa pun sebagai adjunction antara kategori Kleisli dan kategori dasarnya (dalam hal ini, 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 (=<<)
Saya tidak tahu apakah kelanjutan monad sesuai dengan tambahan antara endofunctors pada Hask.
Lihat juga artikel nCatLab tentang monad: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity
Kaitannya dengan tambahan dan keanehan
Setiap koneksi (L ⊣ R) menginduksi monad R∘L dan comonad L∘R. Secara umum ada lebih dari satu pertemuan yang memunculkan monad tertentu dengan cara ini, bahkan ada kategori tambahan untuk monad tertentu. Objek awal dalam kategori itu adalah pertemuan atas kategori Kleisli dari monad dan objek terminal adalah bahwa lebih dari kategori aljabar Eilenberg-Moore. (misalnya Borceux, vol. 2, prop. 4.2.2) Yang terakhir ini disebut monadic adjunction.