Что такое индексированная монада?
Что такое индексированная монада и мотивация к этой монаде?
Я прочитал, что это помогает отслеживать побочные эффекты. Но подпись типа и документация никуда меня не ведут.
Что может быть примером того, как это может помочь отследить побочные эффекты (или любой другой действительный пример)?
5 ответов
Как всегда, используемая людьми терминология не совсем последовательна. Есть множество вдохновленных монад, но строго говоря, не совсем понятий. Термин "индексированная монада" является одним из ряда (включая "монадская" и "параметризованная монада" (название Atkey для них)) терминов, используемых для характеристики одного такого понятия. (Другим таким понятием, если вам интересно, является "монада параметрического эффекта" Кацуматы, индексируемая моноидом, где отдача индексируется нейтрально, а связка накапливается в ее индексе.)
Прежде всего, давайте проверим виды.
IxMonad (m :: state -> state -> * -> *)
То есть тип "вычисления" (или "действие", если вы предпочитаете, но я буду придерживаться "вычисления") выглядит следующим образом
m before after value
где before, after :: state а также value :: *, Идея состоит в том, чтобы охватить средства безопасного взаимодействия с внешней системой, которая имеет некоторое предсказуемое представление о состоянии. Тип вычисления говорит вам, какое состояние должно быть before он бежит, каким будет состояние after он работает и (как с обычными монад над *) Какой тип value s вычисление производит.
Обычные кусочки * - как монада и 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 -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 "диагональ без изменений" 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 как в старом добром Hoare Logic. Утверждениям в логике программы понадобилось менее полувека, чтобы пересечь соответствие Карри-Ховарда и стать типами Хаскеля. Тип 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 полезны Обе модели достоверности интерактивных вычислений в отношении изменения состояния, предсказуемые и непредсказуемые, соответственно. Предсказуемость ценна, когда ее можно получить, но непредсказуемость иногда является фактом жизни. Надеюсь, что этот ответ дает некоторое представление о том, что такое индексированные монады, предсказывая, когда они начинают приносить пользу и когда они прекращаются.
Есть как минимум три способа определения индексированной монады, которые я знаю.
Я буду ссылаться на эти опции как на индексированные монады а-ля X, где X охватывает компьютерных ученых Боба Атки, Конора Макбрайда и Доминика Орчарда, так как я склонен думать о них. Части этих конструкций имеют гораздо более выдающуюся историю и более приятные интерпретации через теорию категорий, но я впервые узнал о них, связанных с этими именами, и стараюсь не дать этому ответу стать слишком эзотерическим.
Atkey
Стиль индексированной монады Боба Атки заключается в работе с 2 дополнительными параметрами для работы с индексом монады.
С этим вы получите определения, которые люди бросили в других ответах:
class IMonad m where
ireturn :: a -> m i i a
ibind :: m i j a -> (a -> m j k b) -> m i k b
Мы также можем определить индексированные комонады а-ля Atkey. Я на самом деле получаю много пробега из тех, кто в lens кодовая база.
McBride
Следующей формой индексированной монады является определение Конора Макбрайда из его статьи "Стрелы возмутительного счастья Клейсли". Вместо этого он использует один параметр для индекса. Это делает определение индексированной монады довольно умной формой.
Если мы определим естественное преобразование, используя параметричность следующим образом
type a ~> b = forall i. a i -> b i
тогда мы можем записать определение Макбрайда как
class IMonad m where
ireturn :: a ~> m a
ibind :: (a ~> m b) -> (m a ~> m b)
Это выглядит совсем не так, как у Атки, но больше похоже на нормальную монаду, а не на монаду (m :: * -> *) мы строим это на (m :: (k -> *) -> (k -> *),
Интересно, что вы на самом деле можете восстановить стиль индексируемой монады из McBride, используя умный тип данных, который McBride в своем неповторимом стиле выбирает для чтения как "at key".
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 может вернуть вас так же, как Атки ibind, Вам необходимо обойти эти (:=) структуры данных, но они восстанавливают всю мощь представления Atkey.
С другой стороны, презентация Atkey недостаточно сильна, чтобы восстановить все варианты использования McBride. Сила была строго получена.
Еще одна приятная вещь - то, что индексируемая монада McBride - это явно монада, это просто монада в другой категории функторов. Работает над эндофункторами в категории функторов из (k -> *) в (k -> *) а не категория функторов из * в *,
Интересное упражнение - выяснить, как выполнить преобразование McBride в Atkey для индексированных комонад. Я лично использую тип данных "At" для конструкции "at key" в статье МакБрайда. Я на самом деле подошел к Бобу Атки на 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
В качестве другого примера, предположим, что вы хотите ограниченную монаду ввода-вывода, которая не разрешает доступ к файлу. Вы можете использовать, например,
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потому что только тогда функция работает правильно - и без предоставления такого свидетеля программа не скомпилируется.
В качестве другого примера, учитывая достаточную настойчивость и поддержку компилятора для выбранного вами языка, вы можете закодировать, что функция предполагает, что определенный список отсортирован.
Индексированные монады позволяют кодировать некоторые из систем зависимых типов, чтобы более точно управлять побочными эффектами.