Что такое индексированная монада и мотивация для этой монады?
Я читал, что это помогает отслеживать побочные эффекты. Но подпись и документация типа не приводят меня никуда.
Каким будет пример того, как это может помочь отслеживать побочные эффекты (или любой другой действительный пример)?
Как всегда, используемая людьми терминология не совсем последовательна. Существует множество вдохновленных монад, но строго говоря, не совсем понятий. Термин "индексированная монада" является одним из ряда (включая "монадная" и "параметризованная монада" (имя Atkey для них)) терминов, используемых для характеристики одного такого понятия. (Еще одно такое понятие, если вам интересно, это Кацамата, "монада параметрического эффекта", индексируемая моноидом, где отдача индексируется нейтрально, а связка накапливается в ее индексе.)
Прежде всего, давайте проверим виды.
IxMonad (m :: state -> state -> * -> *)
То есть тип "вычисления" (или "действие", если вы предпочитаете, но я буду придерживаться "вычисления"), выглядит как
m before after value
где before, after :: state и value :: *. Идея состоит в том, чтобы охватить средства безопасного взаимодействия с внешней системой, которая имеет некоторое предсказуемое представление о состоянии. Тип вычисления сообщает вам, какое состояние должно быть before, какое состояние будет after и (как в случае с обычными монадами над *), какой тип value производит вычисление.
Обычные биты и кусочки * -wise похожи на монаду, а state -wise похоже на игру в домино.
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()
{g(); h()}; 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 -notation)
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 "диагональ без изменений" mii является монадой, но в общем случае mij - нет. Кроме того, значения не индексируются, а вычисления индексируются, поэтому индексированная монада - это не просто обычная идея создания монады для какой-либо другой категории.
Теперь посмотрите еще раз на тип стрелки Клейсли
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 говорит: "Вы можете достичь любого постусловия, которое выполняется, просто ничего не делая", что является правилом Hoare Logic для "skip". Соответствующая композиция является правилом Hoare Logic для ";".
Давайте закончим, посмотрев на тип bindIx, поместив все квантификаторы в.
bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i
Эти forall имеют противоположную полярность. Мы выбираем начальное состояние i и вычисление, которое может начинаться с i, с постусловием a. Мир выбирает любое промежуточное состояние j ему нравится, но он должен дать нам доказательство того, что постусловие b выполняется, и из любого такого состояния мы можем перейти к b. Итак, по порядку мы можем достичь условия b из состояния i. Освободив наше состояние "после", мы можем моделировать непредсказуемые вычисления.
И IxMonad и MonadIx полезны. Обе модели валидности интерактивных вычислений относительно изменяющегося состояния, предсказуемые и непредсказуемые, соответственно. Предсказуемость ценна, когда ее можно получить, но непредсказуемость иногда является фактом жизни. Надеемся, что тогда этот ответ дает некоторое представление о том, что такое индексированные монады, предсказывая, когда они начинают приносить пользу и когда они прекращаются.
Существует как минимум три способа определить индексированную монаду, которую я знаю.
Я буду ссылаться на эти параметры как индексированные монады à la X, где X пробегает по компьютерам ученых Боба Атки, Конора Макбрайда и Доминика Орчард, так как я склонен думать о них. Части этих конструкций имеют гораздо более прославленную историю и более приятные интерпретации через теорию категорий, но я впервые узнал о них, связанных с этими именами, и я пытаюсь сохранить этот ответ слишком эзотерическим.
В стиле индексированной монады Боба Айтта работает с двумя дополнительными параметрами, чтобы иметь дело с индексом монады.
С этим вы получаете определения, которые люди бросали в других ответах:
class IMonad m where
ireturn :: a -> m i i a
ibind :: m i j a -> (a -> m j k b) -> m i k b
Мы также можем определить индексированные комонады à la Atkey. Я действительно получаю много пробега из тех в lens codebase.
Следующая форма проиндексированной монады - это определение Конор Макбрайд из его статьи "Клейсли стрелы изгоняющей удачи" . Вместо этого он использует единственный параметр для индекса. Это означает, что индексированное определение монады имеет довольно умную форму.
Если мы определяем естественное преобразование с использованием параметричности следующим образом:
type a ~> b = forall i. a i -> b i
тогда мы можем записать определение McBride как
class IMonad m where
ireturn :: a ~> m a
ibind :: (a ~> m b) -> (m a ~> m b)
Это выглядит совсем не так, как у Атки, но он больше похож на обычную Монаду, вместо того, чтобы строить монаду на (m :: * -> *), мы строим ее на (m :: (k -> *) -> (k -> *).
Интересно, что вы действительно можете восстановить стиль Atkey с индексированной монадой из McBride, используя умный тип данных, который Макбрайд в своем неподражаемом стиле предпочитает говорить, что вы должны читать как "на ключ".
data (:=) :: a i j where
V :: a -> (a := i) i
Теперь вы можете решить, что
ireturn :: IMonad m => (a := j) ~> m (a := j)
который расширяется до
ireturn :: IMonad m => (a := j) i -> m (a := j) i
может быть вызван только при j = i, а затем тщательное чтение ibind может вернуть вас так же, как Atkey ibind. Вам необходимо передать эти (: =) структуры данных, но они восстанавливают силу презентации Atkey.
С другой стороны, презентация Atkey недостаточно сильна для восстановления всех видов использования версии McBride. Власть была строго достигнута.
Еще одна приятная вещь - то, что индексированная монада Макбрайда - это монада, это просто монада на другой категории функторов. Он работает над endofunctors в категории функторов от (k -> *) до (k -> *), а не от категории функторов от * до *.
Веселое упражнение выясняет, как сделать преобразование McBride в Atkey для индексированных comonads. Я лично использую тип данных "At" для построения "на ключ" в бумаге Макбрайда. Я фактически подошел к Бобу Атке на ICFP 2013 и упомянул, что я повернул его наизнанку, превратив его в "Пальто". Он казался явно обеспокоенным. Линия разыгралась лучше в моей голове. =)
Наконец, третий заявитель с наименее часто упоминаемым именем "проиндексированной монады" принадлежит Доминик Орчард, где вместо этого он использует моноидный уровень типа, чтобы разбить индексы. Вместо того, чтобы просматривать детали конструкции, я просто свяжусь с этим разговором:
Как простой сценарий, предположим, что у вас есть государственная монада. Тип состояния сложный, но все эти состояния могут быть разделены на два набора: красные и синие состояния. Некоторые операции в этой монаде имеют смысл только в том случае, если текущее состояние является синим. Среди них некоторые будут сохранять состояние синим (blueToBlue), а другие будут красным (blueToRed). В обычной монаде мы могли бы написать
blueToRed :: State S ()
blueToBlue :: State S ()
foo :: State S ()
foo = do blueToRed
blueToBlue
вызывает ошибку времени выполнения, поскольку второе действие ожидает синее состояние. Мы хотели бы предотвратить это статически. Указанная монада выполняет эту цель:
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
Ошибка типа запускается, потому что второй индекс blueToRed (Red) отличается от первого индекса blueToBlue (Blue).
В качестве другого примера, с индексированными монадами вы можете разрешить государственной монаде изменять тип для своего состояния, например. вы могли бы
data State old new a = State (old -> (new, a))
Вы можете использовать приведенное выше, чтобы создать состояние, которое представляет собой статически типизированный гетерогенный стек. Операции будут иметь тип
push :: a -> State old (a,old) ()
pop :: State (a,new) new a
В качестве другого примера предположим, что вы хотите ограничить IO монаду, которая не разрешить доступ к файлам. Вы можете использовать, например,
openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _
Таким образом, действие, имеющее тип IO ... NoAccess (), статически гарантируется без доступа к файлу. Вместо этого действие типа IO ... FilesAccessed () может обращаться к файлам. Наличие индексированной монады означает, что вам не нужно создавать отдельный тип для ограниченного ввода-вывода, что потребует дублирования каждой не связанной с файлом функции в обоих типах ввода-вывода.
Индексированная монада не является определенной монадой, например, государственной монадой, а своего рода обобщением концепции монады с дополнительными параметрами типа.
В то время как "стандартное" монадическое значение имеет тип Monad m => m a, значение в индексированной монаде будет IndexedMonad m => m i j a, где i и j являются индексами, так что i является типом индекса в начало монадического вычисления и j в конце вычисления. В некотором смысле вы можете думать о i как о типе типа ввода и j в качестве типа вывода.
Используя State в качестве примера, вычисление с учетом состояния State s a поддерживает состояние типа s на протяжении всего вычисления и возвращает результат типа a. Индексированная версия IndexedState i j a - это вычисление с состоянием, в котором состояние может изменяться на другой тип во время вычисления. Начальное состояние имеет тип i и состояние, а конец вычисления имеет тип j.
Использование индексированной монады над нормальной монадой редко необходимо, но в некоторых случаях ее можно использовать для кодирования более строгих статических гарантий.
Возможно, важно посмотреть, как индексирование используется в зависимых типах (например, в agda). Это может объяснить, как помогает индексация в целом, а затем перевести этот опыт на монады.
Индексирование позволяет устанавливать отношения между конкретными экземплярами типов. Затем вы можете рассуждать о некоторых значениях, чтобы установить, поддерживает ли это соотношение.
Например (в agda) вы можете указать, что некоторые натуральные числа связаны с _<_, и тип указывает, какие номера они есть. Затем вы можете потребовать, чтобы некоторым функциям был предоставлен свидетель, что m < n, потому что только тогда функция работает правильно - и без предоставления такого свидетеля программа не будет компилироваться.
В качестве другого примера, учитывая достаточную настойчивость и поддержку компилятора для выбранного вами языка, вы можете кодировать, что функция предполагает, что определенный список отсортирован.
Индексированные монады позволяют кодировать некоторые из систем зависимых типов, чтобы более точно управлять побочными эффектами.