인덱스 된 모나드는 무엇입니까?

인덱스 된 모나드는 무엇입니까?

---

인덱스 된 모나드 는 무엇 이며이 모나드 의 동기 는 무엇입니까 ?

나는 그것이 부작용을 추적하는 데 도움이된다고 읽었습니다. 그러나 형식 서명과 문서는 나를 어디로도 인도하지 않습니다.

부작용 (또는 다른 유효한 예)을 추적하는 데 도움이 될 수있는 예는 무엇입니까?

---

그 어느 때보 다 사람들이 사용하는 용어는 완전히 일치하지 않습니다. 모나드에 의해 영감을 받았지만 엄격하게 말하는 것은 그다지 중요한 개념이 다양합니다. "인덱싱 된 모나드"라는 용어는 이러한 개념을 특성화하는 데 사용되는 용어의 숫자 ( "모나드"및 "매개 변수화 된 모나드"(Atkey의 이름) 포함) 중 하나입니다. (관심이 있다면 또 다른 개념은 모노 이드로 색인 된 Katsumata의 "파라 메트릭 효과 모나드"입니다. 여기서 return은 중립적으로 색인되고 bind는 색인에 누적됩니다.)

먼저 종류를 확인합시다.

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

즉, "계산"(또는 원하는 경우 "액션"이지만 "계산"을 고수하겠습니다)의 유형은 다음과 같습니다.

m before after value

어디 before, after :: state와 value :: *. 이 아이디어는 예측 가능한 상태 개념 을 가진 외부 시스템과 안전하게 상호 작용하는 수단을 포착하는 것입니다 . 하는 계산으로의 유형은 국가가해야 무엇을 알려줍니다 before, 그것은 실행 상태가 될 것입니다 무엇을 after그것을 실행하고 (정기적 인 모나드와 같은 *어떤 종류의) value계산이 생산의.

일반적인 비트와 조각은 *모나드와 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

이렇게 생성 된 "Kleisli 화살표"(계산을 생성하는 함수)의 개념은 다음과 같습니다.

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를 꺼낼 수없고, 이미 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

실제로, 우리는 원시 Kleisli 화살이 무엇인지 (하나의 "도미노"가 무엇인지) 말한 다음 그 위에 "계산 시퀀스"라는 적절한 개념을 구축했습니다.

Note that for every indexed monad m, the "no change diagonal" m i i is a monad, but in general, m i j is not. Moreover, values are not indexed but computations are indexed, so an indexed monad is not just the usual idea of monad instantiated for some other category.

Now, look again at the type of a Kleisli arrow

a -> m i j b

We know we must be in state i to start, and we predict that any continuation will start from state j. We know a lot about this system! This isn't a risky operation! When we put the dvd in the drive, it goes in! The dvd drive doesn't get any say in what the state is after each command.

But that's not true in general, when interacting with the world. Sometimes you might need to give away some control and let the world do what it likes. For example, if you are a server, you might offer your client a choice, and your session state will depend on what they choose. The server's "offer choice" operation does not determine the resulting state, but the server should be able to carry on anyway. It's not a "primitive command" in the above sense, so indexed monads are not such a good tool to model the unpredictable scenario.

What's a better tool?

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

Scary biscuits? Not really, for two reasons. One, it looks rather more like what a monad is, because it is a monad, but over (state -> *) rather than *. Two, if you look at the type of a Kleisli arrow,

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

you get the type of computations with a precondition a and postcondition b, just like in Good Old Hoare Logic. Assertions in program logics have taken under half a century to cross the Curry-Howard correspondence and become Haskell types. The type of returnIx says "you can achieve any postcondition which holds, 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 type of bindIx, putting all the quantifiers in.

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

These foralls have opposite polarity. We choose initial state i, and a computation which can start at i, with postcondition a. The world chooses any intermediate state j it likes, but it must give us the evidence that postcondition b holds, and from any such state, we can carry on to make b hold. So, in sequence, we can achieve condition b from state i. By releasing our grip on the "after" states, we can model unpredictable computations.

Both IxMonad and MonadIx are useful. Both model validity of interactive computations with respect to changing state, predictable and unpredictable, respectively. Predictability is valuable when you can get it, but unpredictability is sometimes a fact of life. Hopefully, then, this answer gives some indication of what indexed monads are, predicting both when they start to be useful and when they stop.

---

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

I'll refer to these options as indexed monads à la X, where X ranges over the computer scientists Bob Atkey, Conor McBride and Dominic Orchard, as that is how I tend to think of them. Parts of these constructions have a much longer more illustrious history and nicer interpretations through category theory, but I first learned of them associated with these names, and I'm trying to keep this answer from getting too esoteric.

Atkey

Bob Atkey's style of indexed monad is to work with 2 extra parameters to deal with the index of the monad.

With that you get the definitions folks have tossed around in other answers:

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

We can also define indexed comonads à la Atkey as well. I actually get a lot of mileage out of those in the lens codebase.

McBride

The next form of indexed monad is Conor McBride's definition from his paper "Kleisli Arrows of Outrageous Fortune". He instead uses a single parameter for the index. This makes the indexed monad definition have a rather clever shape.

If we define a natural transformation using parametricity as follows

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

then we can write down McBride's definition as

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

This feels quite different than Atkey's, but it feels more like a normal Monad, instead of building a monad on (m :: * -> *), we build it on (m :: (k -> *) -> (k -> *).

Interestingly you can actually recover Atkey's style of indexed monad from McBride's by using a clever data type, which McBride in his inimitable style chooses to say you should read as "at key".

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

Now you can work out that

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

which expands to

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

can only be invoked when j = i, and then a careful reading of ibind can get you back the same as Atkey's ibind. You need to pass around these (:=) data structures, but they recover the power of the Atkey presentation.

On the other hand, the Atkey presentation isn't strong enough to recover all uses of McBride's version. Power has been strictly gained.

Another nice thing is that McBride's indexed monad is clearly a monad, it is just a monad on a different functor category. It works over endofunctors on the category of functors from (k -> *) to (k -> *) rather than the category of functors from * to *.

A fun exercise is figuring out how to do the McBride to Atkey conversion for indexed comonads. I personally use a data type 'At' for the "at key" construction in McBride's paper. I actually walked up to Bob Atkey at ICFP 2013 and mentioned that I'd turned him inside out at made him into a "Coat". He seemed visibly disturbed. The line played out better in my head. =)

Orchard

Finally, a third far-less-commonly-referenced claimant to the name of "indexed monad" is due to Dominic Orchard, where he instead uses a type level monoid to smash together indices. Rather than go through the details of the construction, I'll simply link to this talk:

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

---

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

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

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

triggering a runtime error since the second action expects a blue state. We would like to prevent this statically. Indexed 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 index of blueToRed (Red) differs from the first index of blueToBlue (Blue).

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

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

You could use the above to build a state which is a statically-typed heterogeneous stack. Operations would have type

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

As another example, suppose you want a restricted IO monad which does not allow file access. You could use e.g.

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

In this way, an action having type IO ... NoAccess () is statically guaranteed to be file-access-free. Instead, an action of type IO ... FilesAccessed () can access files. Having an indexed monad would mean you don't have to build a separate type for the restricted IO, which would require to duplicate every non-file-related function in both IO types.

---

An indexed monad isn't a specific monad like, for example, the state monad but a sort of generalization of the monad concept with extra type parameters.

Whereas a "standard" monadic value has the type Monad m => m a a value in an indexed monad would be IndexedMonad m => m i j a where i and j are index types so that i is the type of the index at the beginning of the monadic computation and j at the end of the computation. In a way, you can think of i as a sort of input type and j as the output type.

Using State as an example, a stateful computation State s a maintains a state of type s throughout the computation and returns a result of type a. An indexed version, IndexedState i j a, is a stateful computation where the state can change to a different type during the computation. The initial state has the type i and state and the end of the computation has the type j.

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

---

It may be important to take a look how indexing is used in dependent types (eg in agda). This can explain how indexing helps in general, then translate this experience to monads.

Indexing permits to establish relationships between particular instances of types. Then you can reason about some values to establish whether that relationship holds.

For example (in agda) you can specify that some natural numbers are related with _<_, and the type tells which numbers they are. Then you can require that some function is given a witness that m < n, because only then the function works correctly - and without providing such witness the program will not compile.

As another example, given enough perseverance and compiler support for your chosen language, you could encode that the function assumes that a certain list is sorted.

Indexed monads permit to encode some of what dependent type systems do, to manage side effects more precisely.

참고URL : https://stackoverflow.com/questions/28690448/what-is-indexed-monad