What is an indexed monad?

Question

What is indexed monad and motivation for this monad?

I read that this helps track side effects. But signature and type documentation don't lead me anywhere.

What will be an example of how this can help track side effects (or any other valid example)?

Answer 1

As always, the terminology used by people is not entirely consistent. There are many inspired monads, but strictly speaking, not quite concepts. The term “indexed monad” is one of a number (including “monadic” and “parameterized monad” (the Atkey name for them)) of the terms used to characterize one such concept. (Another such concept, if you are interested, is Katsamata, the “parametric effect monad” indexed by a monoid, where the recoil is indexed neutrally and the connective is accumulated in its index.)

First of all, let's check the views.

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

That is, the type of "calculation" (or "action", if you prefer, but I will stick to the "calculation"), looks like

 m before after value 

where before, after :: state and value :: * . The idea is to encompass means of safe interaction with an external system that has some predictable view of the state. The type of calculation tells you what state should be before , what state will be after and (as is the case with regular monads over * ), what type of value does the calculation.

Regular bits and pieces * -wise look like a monad, and state -wise looks like a domino game.

 ireturn :: a -> miia -- returning a pure value preserves state ibind :: mija -> -- we can go from i to j and get an a, thence (a -> mjkb) -- we can go from j to k and get ab, therefore -> mikb -- we can indeed go from i to k and get ab 

The concept of “Claysley arrow” (a function that performs the calculations) generated in this way

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

and we get the composition

 icomp :: IxMonad m => (b -> mjkc) -> (a -> mijb) -> a -> mikc icomp fg = \ a -> ibind (ga) f 

and, as always, laws accurately guarantee that ireturn and icomp give us a category

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

or in the comedy fake C / Java / whatever

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

Why bother? Model the “rules” of interaction. For example, you cannot eject a DVD if it is not on the disc, and you cannot insert the DVD into the disc if it is already there. So

 data DVDDrive :: Bool -> Bool -> * -> * where -- Bool is "drive full?" DReturn :: a -> DVDDrive iia DInsert :: DVD -> -- you have a DVD DVDDrive True ka -> -- you know how to continue full DVDDrive False ka -- so you can insert from empty DEject :: (DVD -> -- once you receive a DVD DVDDrive False ka) -> -- you know how to continue empty DVDDrive True ka -- 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 = ka ibind (DInsert dvd j) k = DInsert dvd (ibind jk) ibind (DEject j) k = DEject j $ \ dvd -> ibind (j dvd) k 

With this in mind, we can define "primitive" commands

 dInsert :: DVD -> DVDDrive False True () dInsert dvd = DInsert dvd $ DReturn () dEject :: DVDrive True False DVD dEject = DEject $ \ dvd -> DReturn dvd 

from which others are assembled with ireturn and ibind . Now I can write (lending do -notation)

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

but not physically impossible

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

In addition, you can directly define one primitive command

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

and then instantiate the generic template

 data CommandIxMonad :: (state -> state -> * -> *) -> state -> state -> * -> * where CReturn :: a -> CommandIxMonad ciia (:?) :: cija -> (a -> CommandIxMonad cjkb) -> CommandIxMonad cikb instance IxMonad (CommandIxMonad c) where ireturn = CReturn ibind (CReturn a) k = ka ibind (c :? j) k = c :? \ a -> ibind (ja) k 

In fact, we said what the primitive arrows of Claysley (what is "dominoes"), and then built a suitable concept of a "sequence of calculations" over them.

Note that for each indexed monad m “diagonal without changes” mii is a monad, but in the general case mij is not. In addition, values ​​are not indexed, but calculations are indexed, so an indexed monad is not just the usual idea of ​​creating a monad for any other category.

Now look again at the type of arrow Claysley

 a -> mijb 

We know that we must be able to start i , and we predict that any continuation will start from state j . We know a lot about this system! This is not a risky operation! When we put the DVD in the drive, it comes in! The DVD drive has nothing to do with the state after each command.

But this is not so in general when interacting with the world. Sometimes you may need to give up some control and let the world do what it likes. For example, if you are a server, you can offer your client a choice, and your session state will depend on what he chooses. The operation "offer selection" on the server does not determine the resulting state, but the server must be able to perform in any case. In the above sense, this is not a "primitive command", so indexed monads are not a good tool for modeling an unpredictable scenario.

Which tool is better?

 type f :-> g = forall state. f state -> g state class MonadIx (m :: (state -> *) -> (state -> *)) where returnIx :: x :-> mx flipBindIx :: (a :-> mb) -> (ma :-> mb) -- tidier than bindIx 

Scary cookies? Not entirely for two reasons. Firstly, it is more like what a monad is, because it is a monad, but more (state → *) and not * . Two, if you look at the type of arrow Claysley,

 a :-> mb = forall state. a state -> mb state 

You get a type of computation with the precondition a and the postcondition b , as in "Good old Hoar logic." Statements in the program logic took less than half a century to cross Curry-Howard correspondence and become Haskell types. The returnIx type says: “You can achieve any postcondition that is satisfied just by doing nothing,” which is the Hoare Logic rule for “skip”. The corresponding composition is the Hoare Logic rule for ";".

Let's finish by looking at the bindIx type, putting all the quantifiers in.

 bindIx :: forall i. mai -> (forall j. aj -> mbj) -> mbi 

These forall have the opposite polarity. We choose the initial state i and the calculation, which can begin with i , with the postcondition a . The world chooses any intermediate state j he likes, but he must give us proof that the postcondition b holds, and from any such state we can go to b . So, in order, we can reach condition b from state i . Having freed our “after” state, we can model unpredictable calculations.

Both IxMonad and MonadIx are useful. Both models of the validity of interactive computing relative to a changing state, predictable and unpredictable, respectively. Predictability is valuable when it can be obtained, but unpredictability is sometimes a fact of life. We hope that then this answer gives some idea of ​​what indexed monads are, predicting when they begin to be useful and when they stop.

Answer 2

There are at least three ways to define the indexed monad that I know.

I will refer to these parameters as indexed monads à la X, where X runs through the computers of the scientists Bob Atka, Conor McBride and Dominic Orchard, since I tend to think about them. Parts of these constructions have a much more illustrious history and more pleasant interpretations through category theory, but I first learned about them associated with these names, and I'm trying to keep this answer too esoteric.

Atkey

In the style of the indexed monad, Bob Aitta works with two additional parameters to deal with the monad index.

With this, you get definitions that people threw in other answers:

 class IMonad m where ireturn :: a -> miia ibind :: mija -> (a -> mjkb) -> mikb 

We can also define indexed comonads à la Atkey. I really get a lot of mileage from those in the lens codebase .

Mcbride

The next form of indexed monad is the definition of Conor McBride from his article, “Clays of Arrows of Exorcising Luck . ” Instead, it uses a single parameter for the index. This means that the indexed definition of a monad has a pretty clever form.

If we define a natural transformation using parametricity as follows:

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

then we can write the definition of McBride as

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

This does not look like Atka’s, but it looks more like a regular Monad, instead of building a monad on (m :: * -> *) , we build it on (m :: (k -> *) -> (k -> *) .

Interestingly, you can indeed restore the Atkey style with the indexed monad from McBride using the smart data type that McBride prefers to say in his inimitable style that you should read as a key.

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

Now you can decide what

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

which expands to

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

can only be called with j = i, and then a thorough reading of ibind can bring you back just like Atkey ibind . You need to pass these (: =) data structures, but they restore the power of the Atkey presentation.

Atkey’s presentation, on the other hand, isn’t strong enough to restore all uses of the McBride version. Power was strictly achieved.

Another nice thing is that the McBride indexed monad is a monad, it's just a monad on a different category of functors. He works on endofunctors in the functor category from (k -> *) to (k -> *) , and not from the functor category from * to * .

A fun exercise is figuring out how to convert McBride to Atkey for indexed comonads. I personally use the "At" data type to build a "key" in McBride's paper. I actually went up to Bob Atka at the ICFP 2013 and mentioned that I turned it inside out, turning it into a Coat. He seemed clearly worried. The line played out better in my head. =)

Orchard

Finally, the third applicant with the least frequently mentioned name of the “indexed monad” is Dominic Orchard, where instead he uses the monoid type level to partition indexes. Instead of looking at the details of the design, I will simply contact this conversation:

http://www.cl.cam.ac.uk/~dao29/ixmonad/ixmonad-fita14.pdf

Answer 3

As a simple scenario, suppose you have a state monad. The type of state is complex, but all these states can be divided into two sets: red and blue states. Some operations in this monad only make sense if the current state is blue. Among them, some will keep the state blue ( blueToBlue ), while others will be red ( blueToRed ). In a regular monad, we could write

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

causes a runtime error because the second action expects a blue state. We would like to prevent it statically. The specified monad fulfills this goal:

 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 

A type error is triggered because the second blueToRed ( Red ) index is different from the first blueToBlue ( Blue ) index.

As another example, with indexed monads, you can allow the state monad to change the type for its state, for example. could you

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

You can use the above to create a state that is a statically typed heterogeneous stack. Operations will be of type

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

As another example, suppose you want to restrict the IO monad, which does not allow access to files. You can use for example

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

Thus, an action of type IO ... NoAccess () is statically guaranteed without access to the file. Instead, an action like IO ... FilesAccessed () can access files. Having an indexed monad means that you don’t need to create a separate type for limited I / O, which will require duplication of each non-file related function in both types of I / O.

Answer 4

An indexed monad is not a specific monad, for example, a state monad, but a kind of generalization of the concept of a monad with additional type parameters.

While the “standard” monadic value is of type Monad m => ma , the value in the indexed monad is IndexedMonad m => mija , where i and j are indices, so i is the index type at the beginning of the monadic calculation and j at the end of the calculation . In a sense, you can think of i as an input type type and j as an output type.

Using State as an example, state-based calculation State sa maintains a state of type s throughout the calculation and returns a result of type a . An indexed version of IndexedState ija is a IndexedState ija computation in which the state can change to a different type during computation. The initial state is of type i and state, and the end of the calculation is of type j .

Using an indexed monad over a normal monad is rarely necessary, but in some cases it can be used to encode more stringent static guarantees.

Answer 5

It may be important to see how indexing is used in dependent types (e.g., agda). This may explain how indexing in general helps, and then transfer this experience to monads.

Indexing allows you to establish relationships between specific type instances. You can then reason about some of the meanings to determine if this relationship is consistent.

For example (in agda) you can indicate that some positive integers are associated with _<_ , and the type indicates what numbers they are. Then you can demand that some functions be provided with a witness that m < n , because only then the function works correctly - and without providing such a witness, the program will not compile.

As another example, given sufficient persistence and compiler support for your chosen language, you can encode that a function assumes a specific list is sorted.

Indexed monads allow you to encode some of the dependent type systems in order to more accurately control side effects.