Co to jest monada indeksowana i motywacja do tej monady?

Czytałem, że pomaga to śledzić skutki uboczne. Ale podpis typu i dokumentacja nie prowadzą mnie do niczego.

Jaki byłby przykład tego, jak może pomóc śledzenie skutków ubocznych (lub jakikolwiek inny ważny przykład)?

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 :: statei 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 beforedziałać, jaki będzie stan, w którym będzie afterdziałać i (podobnie jak w przypadku zwykłych monad *), jakiego typu valueobliczenia 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 ireturni icompnadaje 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 ireturni ibind. Teraz mogę pisać (zapożyczenie - doprzypis)

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 ito 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, iaby 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 returnIxmó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 forallmają przeciwną polaryzację. Wybieramy stan początkowy ii obliczenia, od których można zacząć i, z warunkiem końcowym a. Świat wybiera dowolny stan pośredni, jjaki mu się podoba, ale musi dać nam dowód, że warunek końcowy bzachowuje, a każdy taki stan możemy butrzymać. Tak więc w kolejności możemy uzyskać warunek bze stanu i. Uwalniając uchwyt na stanach „po”, możemy modelować nieprzewidywalne obliczenia.

Obie IxMonadi MonadIxsą 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ą.

Znam co najmniej trzy sposoby zdefiniowania indeksowanej monady.

Nazywam te opcje indeksowanymi monadami à la X , gdzie X obejmuje informatyków Boba Atkeya, Conora McBride'a i Dominica Orcharda, bo tak o nich myślę. Części tych konstrukcji mają znacznie dłuższą, bardziej znamienitą historię i ładniejsze interpretacje dzięki teorii kategorii, ale najpierw dowiedziałem się o nich, które są związane z tymi nazwami, i staram się, aby ta odpowiedź nie stała się zbyt ezoteryczna.

Atkey

Styl monady indeksowanej Boba Atkey'a polega na pracy z dwoma dodatkowymi parametrami, aby poradzić sobie z indeksem monady.

Dzięki temu otrzymujesz definicje, które ludzie podrzucali w innych odpowiedziach:

class IMonad m where
  ireturn  ::  a -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

Możemy również zdefiniować indeksowane comonady à la Atkey. W rzeczywistości mam dużo kilometrów z tych w bazie lenskodu .

McBride

Następną formą indeksowanej monady jest definicja Conora McBride'a z jego artykułu „Kleisli Arrows of Outrageous Fortune” . Zamiast tego używa pojedynczego parametru dla indeksu. To sprawia, że ​​indeksowana definicja monady ma dość sprytny kształt.

Jeśli zdefiniujemy naturalną transformację za pomocą parametryczności w następujący sposób

type a ~> b = forall i. a i -> b i 

wtedy możemy zapisać definicję McBride'a jako

class IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b) -> (m a ~> m b)

To wydaje się zupełnie inne niż Atkey'a, ale bardziej przypomina normalną monadę, zamiast budować monadę (m :: * -> *), budujemy ją na(m :: (k -> *) -> (k -> *) .

Co ciekawe, możesz faktycznie odzyskać styl indeksowanej monady Atkeya z McBride's używając sprytnego typu danych, który McBride w swoim niepowtarzalnym stylu decyduje się czytać jako „kluczowy”.

data (:=) :: a i j where
   V :: a -> (a := i) i

Teraz możesz to rozpracować

ireturn :: IMonad m => (a := j) ~> m (a := j)

który rozszerza się do

ireturn :: IMonad m => (a := j) i -> m (a := j) i

można wywołać tylko wtedy, gdy j = i, a uważne przeczytanie ibindmoże przywrócić to samo, co Atkeyibind . Musisz ominąć te (: =) struktury danych, ale odzyskują one moc prezentacji Atkey.

Z drugiej strony prezentacja Atkey nie jest wystarczająco mocna, aby odzyskać wszystkie zastosowania wersji McBride. Moc została zdobyta ściśle.

Kolejną fajną rzeczą jest to, że indeksowana monada McBride'a jest wyraźnie monadą, jest po prostu monadą z innej kategorii funktorów. Działa nad endofunkcjami na kategorii funktorów od (k -> *)do, (k -> *)a nie na kategorii funktorów od *do* .

Zabawne ćwiczenie polega na ustaleniu, jak wykonać konwersję McBride na Atkey dla indeksowanych comonad . Osobiście używam typu danych „At” do konstrukcji „at key” w artykule McBride'a. Właściwie to podszedłem do Boba Atkeya na ICFP 2013 i wspomniałem, że odwróciłem go na lewą stronę i zrobiłem z niego „płaszcz”. Wydawał się wyraźnie zaniepokojony. W mojej głowie grała się lepiej. =)

sad owocowy

Wreszcie trzeci, znacznie rzadziej wymieniany pretendent do nazwy „indeksowana monada” to Dominic Orchard, w którym zamiast tego używa monoidu na poziomie typu, aby zmiażdżyć indeksy. Zamiast omawiać szczegóły konstrukcji, po prostu podam link do tego wystąpienia:

https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf

W prostym scenariuszu załóżmy, że masz monadę stanu. Typ stanu jest złożony i duży, ale wszystkie te stany można podzielić na dwa zestawy: stany czerwony i niebieski. Niektóre operacje w tej monadzie mają sens tylko wtedy, gdy aktualny stan jest stanem niebieskim. Wśród nich niektóre zachowają stan niebieski ( blueToBlue), podczas gdy inne staną się czerwone ( blueToRed). W zwykłej monadzie moglibyśmy pisać

blueToRed  :: State S ()
blueToBlue :: State S ()

foo :: State S ()
foo = do blueToRed
         blueToBlue

wyzwalanie błędu wykonania, ponieważ druga akcja oczekuje niebieskiego stanu. Chcielibyśmy temu zapobiec statycznie. Indeksowana monada spełnia ten cel:

data Red
data Blue

-- assume a new indexed State monad
blueToRed  :: State S Blue Red  ()
blueToBlue :: State S Blue Blue ()

foo :: State S ?? ?? ()
foo = blueToRed `ibind` \_ ->
      blueToBlue          -- type error

Wyzwalany jest błąd typu, ponieważ drugi indeks blueToRed( Red) różni się od pierwszego indeksu blueToBlue( Blue).

Jako inny przykład, z indeksowanymi monadami możesz pozwolić monadzie stanu na zmianę typu swojego stanu, np.

data State old new a = State (old -> (new, a))

Możesz użyć powyższego do zbudowania stanu, który jest stosem heterogenicznym o statycznym typie. Operacje miałyby typ

push :: a -> State old (a,old) ()
pop  :: State (a,new) new a

Jako inny przykład załóżmy, że potrzebujesz ograniczonej monady IO, która nie zezwala na dostęp do plików. Możesz użyć np

openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _

W ten sposób akcja mająca typ IO ... NoAccess ()jest statycznie gwarantowana jako wolna od dostępu do pliku. Zamiast tego akcja typu IO ... FilesAccessed ()może uzyskać dostęp do plików. Posiadanie indeksowanej monady oznaczałoby, że nie musisz budować oddzielnego typu dla ograniczonego IO, co wymagałoby zduplikowania każdej funkcji niezwiązanej z plikiem w obu typach IO.

Monada indeksowana nie jest konkretną monadą, jak na przykład monada stanu, ale rodzajem uogólnienia koncepcji monady z dodatkowymi parametrami typu.

Podczas gdy „standardowa” wartość monadyczna ma typ, Monad m => m awartość w indeksowanej monadzie byłaby IndexedMonad m => m i j agdzie ii jsą typami indeksów, tak więc ijest to typ indeksu na początku obliczeń monadycznych i jna końcu obliczenia. W pewnym sensie można myśleć o irodzaju danych wejściowych i jwyjściowych.

Na Stateprzykład obliczenie stanowe State s azachowuje stan typu sprzez cały czas trwania obliczeń i zwraca wynik typu a. Wersja indeksowana IndexedState i j ato obliczenie stanowe, w którym stan może zmienić się na inny typ podczas obliczeń. Stan początkowy ma typ ii stan, a koniec obliczenia ma typ j.

Używanie indeksowanej monady zamiast zwykłej monady jest rzadko konieczne, ale w niektórych przypadkach może być używane do kodowania bardziej rygorystycznych gwarancji statycznych.

Warto przyjrzeć się, jak indeksowanie jest używane w typach zależnych (np. W agda). To może wyjaśnić, jak ogólnie pomaga indeksowanie, a następnie przełożyć to doświadczenie na monady.

Indeksowanie umożliwia ustanowienie relacji między określonymi instancjami typów. Następnie możesz uzasadnić pewne wartości, aby ustalić, czy ta relacja jest zachowana.

Na przykład (w agda) możesz określić, że niektóre liczby naturalne są powiązane _<_, a typ określa, które to liczby. Wtedy możesz wymagać, aby jakaś funkcja była świadkiem tegom < n , ponieważ tylko wtedy funkcja działa poprawnie - i bez takiego świadka program się nie skompiluje.

Jako inny przykład, mając wystarczającą wytrwałość i obsługę kompilatora dla wybranego języka, możesz zakodować, że funkcja zakłada, że ​​określona lista jest posortowana.

Monady indeksowane pozwalają zakodować niektóre działania systemów typów zależnych, aby dokładniej zarządzać efektami ubocznymi.