Jak zawsze, terminologia używana przez ludzi nie jest do końca spójna. Istnieje wiele różnych pojęć inspirowanych przez monady, ale ściśle mówiąc nie do końca. Termin „monada indeksowana” jest jednym z wielu terminów (w tym „monadish” i „monada sparametryzowana” (ich nazwa Atkey)) używanych do scharakteryzowania jednego z takich pojęć. (Innym takim pojęciem, jeśli jesteś zainteresowany, jest "monada efektu parametrycznego" Katsumaty, indeksowana przez monoid, gdzie zwrot jest indeksowany neutralnie, a bind gromadzi się w jego indeksie.)
Przede wszystkim sprawdźmy rodzaje.
IxMonad (m :: state -> state -> * -> *)
Oznacza to, że typ „obliczenia” (lub „akcji”, jeśli wolisz, ale pozostanę przy „obliczeniu”) wygląda tak
m before after value
gdzie before, after :: state
i value :: *
. Chodzi o to, aby uchwycić sposoby bezpiecznej interakcji z zewnętrznym systemem, który ma pewne przewidywalne pojęcie stanu. Typ obliczenia mówi ci, jaki musi być stan, w którym będzie before
działać, jaki będzie stan, w którym będzie after
działać i (podobnie jak w przypadku zwykłych monad *
), jakiego typu value
obliczenia generują.
Zwykłe bity i kawałki są *
-wspomagane jak monada i state
-wspomagane jak gra w domino.
ireturn :: a -> m i i a -- returning a pure value preserves state
ibind :: m i j a -> -- we can go from i to j and get an a, thence
(a -> m j k b) -- we can go from j to k and get a b, therefore
-> m i k b -- we can indeed go from i to k and get a b
Powstaje w ten sposób pojęcie „strzały Kleisliego” (funkcja, która daje obliczenia)
a -> m i j b -- values a in, b out; state transition i to j
i otrzymujemy kompozycję
icomp :: IxMonad m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
icomp f g = \ a -> ibind (g a) f
i, jak zawsze, prawo dokładnie to zapewnia ireturn
i icomp
nadaje nam kategorię
ireturn `icomp` g = g
f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)
lub w komedii fałszywy C / Java / cokolwiek,
g(); skip = g()
skip; f() = f()
{g(); h()}; f() = h(); {g(); f()}
Po co się męczyć? Modelowanie „reguł” interakcji. Na przykład nie możesz wysunąć płyty DVD, jeśli nie ma jej w napędzie, i nie możesz włożyć płyty DVD do napędu, jeśli jest już na niej. Więc
data DVDDrive :: Bool -> Bool -> * -> * where -- Bool is "drive full?"
DReturn :: a -> DVDDrive i i a
DInsert :: DVD -> -- you have a DVD
DVDDrive True k a -> -- you know how to continue full
DVDDrive False k a -- so you can insert from empty
DEject :: (DVD -> -- once you receive a DVD
DVDDrive False k a) -> -- you know how to continue empty
DVDDrive True k a -- so you can eject when full
instance IxMonad DVDDrive where -- put these methods where they need to go
ireturn = DReturn -- so this goes somewhere else
ibind (DReturn a) k = k a
ibind (DInsert dvd j) k = DInsert dvd (ibind j k)
ibind (DEject j) k = DEject j $ \ dvd -> ibind (j dvd) k
Mając to na miejscu, możemy zdefiniować polecenia „prymitywne”
dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()
dEject :: DVDrive True False DVD
dEject = DEject $ \ dvd -> DReturn dvd
z których inne są montowane z ireturn
i ibind
. Teraz mogę pisać (zapożyczenie - do
przypis)
discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dvd' <- dEject; dInsert dvd ; ireturn dvd'
ale nie fizycznie niemożliwe
discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dInsert dvd; dEject -- ouch!
Alternatywnie, można bezpośrednio zdefiniować swoje prymitywne polecenia
data DVDCommand :: Bool -> Bool -> * -> * where
InsertC :: DVD -> DVDCommand False True ()
EjectC :: DVDCommand True False DVD
a następnie utwórz wystąpienie szablonu ogólnego
data CommandIxMonad :: (state -> state -> * -> *) ->
state -> state -> * -> * where
CReturn :: a -> CommandIxMonad c i i a
(:?) :: c i j a -> (a -> CommandIxMonad c j k b) ->
CommandIxMonad c i k b
instance IxMonad (CommandIxMonad c) where
ireturn = CReturn
ibind (CReturn a) k = k a
ibind (c :? j) k = c :? \ a -> ibind (j a) k
W efekcie powiedzieliśmy, czym są prymitywne strzały Kleisliego (czym jest jedno „domino”), a następnie zbudowaliśmy nad nimi odpowiednie pojęcie „sekwencji obliczeniowej”.
Zauważ, że dla każdej indeksowanej monady m
„przekątna bez zmian” m i i
to monada, ale ogólnie rzecz biorąc,m i j
nie jest. Co więcej, wartości nie są indeksowane, ale obliczenia są indeksowane, więc indeksowana monada to nie tylko zwykła idea monady, której instancje są tworzone dla innej kategorii.
Teraz spójrz ponownie na rodzaj strzały Kleisli
a -> m i j b
Wiemy, że musimy być w stanie, i
aby rozpocząć, i przewidujemy, że jakakolwiek kontynuacja zacznie się od stanu j
. O tym systemie wiemy dużo! To nie jest ryzykowna operacja! Kiedy włożymy DVD do napędu, wchodzi! Napęd DVD nie ma nic do powiedzenia o stanie po każdym poleceniu.
Ale generalnie nie jest to prawdą podczas interakcji ze światem. Czasami możesz chcieć oddać trochę kontroli i pozwolić światu robić, co mu się podoba. Na przykład, jeśli jesteś serwerem, możesz zaoferować klientowi wybór, a stan Twojej sesji będzie zależał od tego, co wybierze. Operacja „wybór oferty” serwera nie określa wynikowego stanu, ale serwer i tak powinien być w stanie kontynuować. Nie jest to „prymitywne polecenie” w powyższym sensie, więc indeksowane monady nie są tak dobrym narzędziem do modelowania nieprzewidywalnego scenariusza.
Jakie jest lepsze narzędzie?
type f :-> g = forall state. f state -> g state
class MonadIx (m :: (state -> *) -> (state -> *)) where
returnIx :: x :-> m x
flipBindIx :: (a :-> m b) -> (m a :-> m b) -- tidier than bindIx
Straszne ciastka? Niezupełnie, z dwóch powodów. Po pierwsze, bardziej przypomina to, czym jest monada, ponieważ jest monadą, ale (state -> *)
raczej ponad niż *
. Po drugie, jeśli spojrzysz na rodzaj strzały Kleisli,
a :-> m b = forall state. a state -> m b state
otrzymujesz typ obliczeń z warunkiem wstępnym a
i warunkiem końcowym b
, tak jak w Good Old Hoare Logic. Twierdzenia w logice programu zajęły mniej więcej pół wieku, zanim przekroczyły korespondencję Curry-Howard i stały się typem Haskella. Typ returnIx
mówi „możesz osiągnąć dowolny warunek końcowy, który jest zachowany, po prostu nic nie robiąc”, co jest regułą Hoare Logic dla „pomiń”. Odpowiednia kompozycja to reguła Hoare Logic dla „;”.
Na koniec przyjrzyjmy się typowi bindIx
, umieszczając wszystkie kwantyfikatory.
bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i
Te forall
mają przeciwną polaryzację. Wybieramy stan początkowy i
i obliczenia, od których można zacząć i
, z warunkiem końcowym a
. Świat wybiera dowolny stan pośredni, j
jaki mu się podoba, ale musi dać nam dowód, że warunek końcowy b
zachowuje, a każdy taki stan możemy b
utrzymać. Tak więc w kolejności możemy uzyskać warunek b
ze stanu i
. Uwalniając uchwyt na stanach „po”, możemy modelować nieprzewidywalne obliczenia.
Obie IxMonad
i MonadIx
są przydatne. Oba modele trafności obliczeń interaktywnych w odniesieniu do zmieniającego się stanu, odpowiednio przewidywalnego i nieprzewidywalnego. Przewidywalność jest cenna, kiedy można ją zdobyć, ale nieprzewidywalność jest czasami faktem. Miejmy nadzieję, że ta odpowiedź daje pewne wskazówki, czym są indeksowane monady, przewidując zarówno kiedy zaczną być przydatne, jak i kiedy przestaną.
True
/False
wartości jako argumenty typu doDVDDrive
? Czy to jakieś rozszerzenie, czy też wartości logiczne faktycznie tu wpisują?