그 어느 때보 다 사람들이 사용하는 용어는 완전히 일치하지 않습니다. 모나드에 의해 영감을 받았지만 엄격하게 말하는 것은 그다지 중요한 개념이 다양합니다. “인덱싱 된 모나드”라는 용어는 이러한 개념을 특성화하는 데 사용되는 용어의 숫자 ( “모나드”및 “매개 변수화 된 모나드”(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 화살이 무엇인지 (하나의 “도미노”가 무엇인지) 말한 다음 그 위에 “계산 시퀀스”라는 적절한 개념을 구축했습니다.

인덱스 된 모든 모나드 m에 대해 “대각선 변경 없음” m i i은 모나드이지만 일반적으로m i j 으로 그렇지 않습니다. 또한 값은 색인화되지 않지만 계산은 색인화되므로 색인화 된 모나드는 다른 범주에 대해 인스턴스화 된 모나드의 일반적인 아이디어가 아닙니다.

자, Kleisli 화살의 종류를 다시보세요

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 -> *)이 아니라 *. 둘째, Kleisli 화살의 종류를 보면

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

Good Old Hoare Logic에서 와 같이 전제 조건 a 및 후 조건 으로 계산 유형을 얻습니다 b. 프로그램 논리에 대한 주장은 Curry-Howard 서신을 통과하고 Haskell 유형이되는 데 반세기 미만이 걸렸습니다. returnIx“건너 뛰기”에 대한 Hoare Logic 규칙 인 “아무것도하지 않고 유지되는 모든 사후 조건을 달성 할 수 있습니다.” 라는 유형입니다 . 해당 구성은 “;”에 대한 Hoare Logic 규칙입니다.

유형을 살펴보고 bindIx모든 수량자를 입력하여 마무리하겠습니다 .

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

이것들 forall은 반대 극성을 가지고 있습니다. 우리는 초기 상태 와 사후 조건으로 i시작할 수있는 계산을 선택합니다 . 세상은 자신이 좋아 하는 중간 상태를 선택 하지만 사후 조건이 유지 된다는 증거를 우리에게 제공해야하며 그러한 상태에서 우리는 계속 유지할 수 있습니다. 따라서 순서대로 state에서 조건 을 얻을 수 있습니다 . “이후”상태에 대한 그립을 해제함으로써 예측할 수없는 계산을 모델링 할 수 있습니다 .iajbbbi

모두 IxMonad와 MonadIx유용합니다. 두 모델 모두 상태 변화, 예측 가능 및 예측 불가능과 관련하여 상호 작용 계산의 유효성을 모델링합니다. 예측 가능성은 얻을 수있을 때 가치가 있지만 예측 불가능 성은 때때로 삶의 사실입니다. 바라건대,이 답변은 인덱스 모나드가 무엇인지에 대한 일부 표시를 제공하여 유용하기 시작하는시기와 중지되는시기를 모두 예측합니다.

답변

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

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)

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

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

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 _