Czy jest coś, co nazywa się "semi-monad" lub "counter-monad"?

Question

Studiuję Monady Haskella. Kiedy przeczytałem artykuł o Wikipedii Category theory, stwierdziłem, że sygnatura morfizmów monady wygląda całkiem jak tautologie w logice, ale musisz przekonwertować M a na ~~A, tutaj ~ jest logiczną negacją.

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction 
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B 

innych operacji jest także tautologie:

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B) 
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A 

Jest również zrozumiałe, że zgodnie z tym, że Curry-Howard korespondencja normalnych językach funkcjonalnych jest intuicyjny logika nie logika klasyczna, więc nie możemy oczekiwać Tautologia taka jak ~~A => A może mieć korespondencję.

Ale myślę o czymś innym. Dlaczego monada może odnosić się tylko do podwójnej negacji? jaka jest zgodność pojedynczej negacji? To prowadzi mnie do następującej definicji klasy:

class Nomad n where 
    rfmap :: (a -> b) -> n b -> n a 
    dneg :: a -> n (n a) 

return :: Nomad n => a -> n (n a) 
return = dneg 
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b) 
x >>= f = rfmap dneg $ rfmap (rfmap f) x 

Tu zdefiniował pojęcie o nazwie „Nomad” i obsługuje dwie operacje (zarówno związanych z aksjomatu logiki intuicyjnej logiki). Zauważ, że nazwa "rfmap" oznacza fakt, że jej podpis jest podobny do podpisu functora fmap, ale kolejność a i b jest odwrotna. Teraz mogę ponownie zdefiniować operacje Monad z nimi, zamieniając M a na n (n a).

Teraz przejdźmy do części pytania. To, że Monad jest pojęciem z teorii kategorii, zdaje się oznaczać, że mój "Nomad" jest także pojęciem teorii kategorii. Więc co to jest? To jest użyteczne? Czy istnieją jakieś dokumenty lub wyniki badań w tym temacie?

Answer 1

Podwójna negacja jest szczególności monada

data Void --no constructor because it is uninhabited 

newtype DN a = DN {runDN :: (a -> Void) -> Void} 

instance Monad DN where 
    return x = DN $ \f -> f x 
    m >>= k = DN $ \c -> runDN m (\a -> runDN (k a) c)) 

faktycznie, to jest przykładem bardziej ogólnym monady

type DN = Cont Void 
newtype Cont r a = Cont {runCont :: (a -> r) -> r} 

który jest monada za kontynuacją przejściu.

Pojęcie takie jak "monada" nie jest zdefiniowane tylko przez podpis, ale także przez niektóre prawa. Oto pytanie: jakie powinny być prawa dla twojej konstrukcji?

(a -> b) -> f b -> f a 

jest podpis metody dobrze znane kategorii teorii, kontrawariantny funktor. Podporządkowuje się zasadniczo tym samym prawom, co funktory (zachowania (ko) kompozycji i tożsamości). W rzeczywistości przeciwwskazany funktor jest dokładnie funktorem kategorii przeciwnej.Ponieważ interesuje nas "funktory haskellowe", które mają być endo-funktorykami, widzimy, że "funkator contravariant" haskella jest funktorem Hask -> Hask_Op.

Z drugiej strony, co

a -> f (f a) 

jakie prawa powinno to mieć? Mam propozycję. W teorii kategorii możliwe jest mapowanie pomiędzy Funktorami. Biorąc pod uwagę dwa funktory z F, G każdej z kategorii C do kategorii D, A naturalna transformacja z F do G jest morfizmem w D

forall a. F a -> G a 

że przestrzega pewnych praw spójność. Możesz zrobić wiele dzięki naturalnym transformacjom, w tym używając ich do zdefiniowania "kategorii funktora". Ale klasyczny żart (z powodu Mac Lane) polega na tym, że wymyślono kategorie mówiące o funktorach, funktory wymyślono, aby mówić o naturalnych przekształceniach, a naturalne transformacje wymyślono, aby mówić o dodatkach.

funktora F : D -> C a funktor G : C -> D tworzą adjunction z C do D jeśli istnieją dwie transformacja naturalna

unit : Id -> G . F 
counit : F . G -> Id 

Ta idea adjunction jest częstym sposobem rozumienia monady. Każde przyłączenie prowadzi do monady w całkowicie naturalny sposób. Oznacza to, że skoro skład tych dwóch funktorów jest endofunktorem, a ty masz coś pokrewnego do powrotu (jednostka), wszystko czego potrzebujesz to sprzężenie. Ale to proste, join to po prostu funkcja G . F . G . F -> G . F, którą otrzymujesz po prostu używając counit "w środku".

A więc z tym wszystkim, czego szukasz? Dobrze

dneg :: a -> n (n a) 

wygląda dokładnie jak unit z adjunction z kontrawariantny funktora z samym sobą. Dlatego Twój typ Nomad jest prawdopodobnie (oczywiście jeśli użyjesz go do skonstruowania monady) jest dokładnie taki sam, jak "przeciwwariantowy funktor, który jest samozłączny". Poszukiwanie samodzielnych funktorów doprowadzi cię z powrotem do Double-negation i Continuation passing ... właśnie tam zaczęliśmy!

---

EDYCJA: Prawie na pewno niektóre z powyższych strzałek są do tyłu. Jednak podstawowa idea jest słuszna. Można się dogadać siebie za pomocą poniższych cytatów:

najlepszych książek na temat teorii kategorii są prawdopodobnie

• Steve Awodey, teoria Kategoria
• Sanders Mac Lane, kategorie dla matematyk roboczej

Chociaż istnieje wiele bardziej przystępnych książek intro, w tym książka Benjamina Piercesa na temat teorii kategorii dla komputerów scie Ntists.

wideo wykłady online,

• kategorii Teoria wykłady Steve Awodey z Oregon Programming Language Summer School
• Catsters krótkich wykładów na youtube, indexed here, zwracać szczególną uwagę na filmy na adjunctions

liczba dokumentów bada kąt sprzężenia w monadzie kontynuacji, na przykład:

• Hayo Thielecke, Semantyka kontynuacja i Self-adjointness

warunki wyszukiwania "self adjoint", "kontynuacja" i "monada" są dobre. Ponadto, wielu blogerów napisało o tych problemach. Jeśli używasz google "skąd biorą się monady", otrzymujesz przydatne wyniki, takie jak this one z kawiarni kategorii n, lub this one z sigfpe. Również Sjoerd Vissche's link do czytnika Comonad.

Answer 2

To byłby samozgodny funktor kontrawariatu. rfmap dostarcza przeciwwariantową część funktora, a dneg jest jednostką i kontrapunktem przymusu.

Op r jest przykładem, który tworzy monadę kontynuacji. Zobacz moduły przeciwwskazań w http://hackage.haskell.org/package/adjunctions dla jakiegoś kodu.

Powinieneś przeczytać http://comonad.com/reader/2011/monads-from-comonads/, która jest powiązana i bardzo interesująca.