как всегда, терминология, которую используют люди, не совсем последовательна. Существует множество вдохновленных монадами, но, строго говоря, это не совсем понятия. Термин " индексированная монада "является одним из ряда (включая" монадиш "и" параметризованную монаду " (имя Atkey для них)) терминов, используемых для характеристики одного такого понятия. (Другое такое понятие, если вам интересно, - это "монада параметрического эффекта Кацуматы", индексированная моноидом, где возврат индексируется нейтрально и связывание накапливается в его индекс.)

прежде всего, давайте проверим видов.

IxMonad (m :: state -> state -> * -> *)

то есть, тип " вычисление "(или" действие", если вы предпочитаете, но я буду придерживаться" вычисление"), выглядит как

m before after value

здесь before, after :: state и value :: *. Идея состоит в том, чтобы захватить средства для безопасного взаимодействия с внешней системой, которая имеет некоторые предсказуемым понятие государства. Тип вычисления говорит вам, что состояние должно быть before он работает, что государство будет after он работает и (как с обычной монады над *), что типа values вычисление производит.

обычные биты и куски *-мудрый, как монада и state-мудрый, как играть в домино.

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

понятие "стрелка Клейсли" (функция, которая дает вычисление), таким образом, генерируется

a -> m i j b   -- values a in, b out; state transition i to j

и мы получаем состав

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

и, как всегда, законы точно гарантируют, что ireturn и icomp дайте нам категорию

      ireturn `icomp` g = g
      f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)

или, в комедии поддельные C / Java / что угодно,

      g(); skip = g()
      skip; f() = f()
{h(); g()}; f() = h(); {g(); f()}

зачем? Моделировать "правила" взаимодействия. Например, вы не можете извлечь dvd-диск, если его нет в приводе, и вы не можете поместить dvd-диск в привод, если он уже есть. Так что

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

С этим на месте, мы можем определить "примитивные" команды

dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()

dEject :: DVDrive True False DVD
dEject = DEject $ \ dvd -> DReturn dvd

из которого собраны другие с ireturn и ibind. Теперь я могу писать (заимствование do-нотации)

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dvd' <- dEject; dInsert dvd ; ireturn dvd'

но не физически невозможно

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dInsert dvd; dEject      -- ouch!

кроме того, можно определить примитивные команды

data DVDCommand :: Bool -> Bool -> * -> * where
  InsertC  :: DVD -> DVDCommand False True ()
  EjectC   :: DVDCommand True False DVD

и затем создать экземпляр универсального шаблона

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

фактически, мы сказали, что такое примитивные стрелки Клейсли (что такое "домино"), а затем построили над ними подходящее понятие "последовательность вычислений".

обратите внимание, что для каждой индексированной монады m, "без изменения диагонали"m i i - это монада, но в целом, m i j нет. Кроме того, значения не индексируются, но вычисления индексируются, поэтому индексированная монада-это не просто обычная идея монады, созданная для какой-либо другой категории.

теперь взгляните еще раз на тип стрелки Клейсли

a -> m i j b

мы знаем, что мы должны быть в состоянии i для начала, и мы прогнозируем, что любое продолжение будет начинаться от государства j. Мы много знаем об этой системе! Это не рискованная операция! Когда мы вставляем dvd в дисковод, он входит! Dvd-привод не получает никакого слова о том, в каком состоянии находится после каждой команды.

но это не так вообще, когда взаимодействуешь с миром. Иногда вам может потребоваться отказаться от некоторого контроля и позволить миру делать то, что ему нравится. Например, если вы являетесь сервером, вы можете предложить клиенту выбор, и ваше состояние сеанса будет зависеть от того, что они выберут. Операция сервера "выбор предложения" не выполняется определите результирующее состояние, но сервер должен быть в состоянии продолжать в любом случае. Это не "примитивная команда" в вышеуказанном смысле, поэтому индексированные монады не являются таким хорошим инструментом для моделирования непредсказуемой сценарий.

какой инструмент лучше?

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

страшные печенье? Не совсем, по двум причинам. Во-первых, это больше похоже на то, что такое монада, потому что это и монада, но над (state -> *), а не *. Во-вторых, если вы посмотрите тип стрелы Клейсли,

a :-> m b   =   forall state. a state -> m b state

вы получаете тип вычислений с условиеa и постусловия b, как в старой доброй логике Хоара. Утверждения в логике программ заняли менее полувека, чтобы пересечь переписку Карри-Говарда и стать типами Хаскелла. Тип returnIx говорит:" Вы можете достичь любого постусловия, которое выполняется, просто ничего не делая", что является правилом логики Хоара для"пропуска". Соответствие композиция-это правило логики Хоара для ";".

давайте закончим, посмотрев на тип bindIx, вводя все кванторы.

bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

эти forallS имеют противоположную полярность. Мы выбираем начальное состояние i, и вычисление, которое может начинаться с i, с постусловием a. Мир выбирает любое промежуточное состояние j его любит, но он должен дать нам доказательства того, что постусловие b держит, и от любого такого положения, мы можем снести дальше делать b удерживайте. Таким образом, в последовательности, мы можем достичь условия b государственной i. Отпустив нашу хватку на" после " состояний, мы можем моделировать непредсказуемой вычислений.

и IxMonad и MonadIx полезны. Обе модели валидности интерактивных вычислений относительно изменяющегося состояния предсказуемы и непредсказуемы соответственно. Предсказуемость ценна, когда вы можете ее получить, но непредсказуемость иногда является фактом жизни. Обнадеживающе, затем этот ответ дает некоторое представление о том, что такое индексированные монады, предсказывая, когда они начинают быть полезными и когда они останавливаются.