[解決済み] インデックス付きモナドとは？

質問

この質問は インデックス付きモナド とこのモナドの動機は何ですか？

私はそれが副作用を追跡するのに役立つと読んだことがあります。しかし、型署名とドキュメントは私をどこにも導きません。

副作用を追跡するのに役立つ例（または他の有効な例）は何でしょうか？

どのように解決するのですか？

これまでと同様、人々が使用する用語は完全に一致しているわけではありません。モナドに触発されたものの、厳密にはそうではない、さまざまな概念があります。インデックス付きモナドという用語は、そのような概念を特徴づけるために使われるいくつかの用語（モナディッシュやパラメータ付きモナド（アッキーの名前）を含む）のうちのひとつです（もうひとつのそのような概念は、もしアッキーがそのような概念を持っているのであれば、そのような用語です）。(もし興味があるなら、勝俣の "parametric effect monad" は、モノイドによってインデックスされ、return が中立的にインデックスされ、bind がそのインデックスに蓄積されるような概念です)。

まず、種類を確認しましょう。

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

つまり、"computation" (あるいは "action" でもいいですが、ここでは "computation" にします) の型は、次のようになります。

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()
{h(); g()}; f() = h(); {g(); f()}

なぜ悩むのか？相互作用のルール(quot;rule")をモデル化するためです。たとえば、ドライブに 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

これで、"primitive" コマンドを定義することができます。

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

事実上、私たちは原始的なクライスリー矢印が何であるか（1つの"ドミノ"は何か）を述べ、次にそれらの上に"計算順序"の適切な概念を構築しました。

すべてのインデックス付きモナド m には、"no change diagonal" があります。 m i i はモナドですが、一般には m i j はそうではない。さらに、値はインデックスされませんが、計算はインデックスされます。したがって、インデックス付きモナドは、何か他のカテゴリのためにインスタンス化されたモナドの通常の考えだけではありません。

さて、もう一度クライスリー矢印の型を見てみましょう。

a -> m i j b

私たちは状態でなければならないことを知っています i から始まることが分かっており、継続は状態 j . 私たちはこのシステムについて多くのことを知っています! これは危険な操作ではありません dvdをドライブに入れたら、そのまま入ってしまうのです! 各コマンドの後の状態について、dvd ドライブは何も言いません。

しかし、世界と対話するとき、一般的にはそうではありません。時には、コントロールを放棄して、世界に好きなようにさせる必要があるかもしれません。たとえば、あなたがサーバーの場合、クライアントに選択肢を提供し、あなたのセッションの状態はクライアントが何を選択するかに依存します。サーバーの "offer choice" 操作は結果の状態を決定しませんが、サーバーはとにかく続けることができるはずです。これは上記の意味での "プリミティブコマンド" ではないので、インデックス付きモナドはモデル化するのにそれほど良いツールではありません。 予測不可能 というシナリオがあります。

より良いツールは？

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

怖いビスケット？そうでもありません。理由は2つあります。1つは、モナドとは何かということです。 は はモナドですが、その上に (state -> *) よりも * . 2、クライスリーの矢印の型を見てみると。

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

で計算の種類を取得し 前提条件 a とポストコンディション b というように、古き良きHoare Logicのようなものです。プログラムロジックのアサーションは、半世紀弱の間に、Curry-Howard対応を越えて、Haskellの型になった。の型は returnIx の型は "何もしないだけで成立する任意の後件を達成できる" と言っており、これは "skip" に対する Hoare Logic のルールである。対応する構成は";"に対する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 . after"状態のグリップを解放することで、以下のようにモデル化することができます。 予測不可能な 計算をモデル化することができます。

どちらも IxMonad と MonadIx は有用である。両方とも、それぞれ予測可能、予測不可能という状態の変化に関する対話型計算の妥当性をモデル化しています。予測可能は得られると価値がありますが、予測不可能は時に事実です。うまくいけば、この回答はインデックス付きモナドが何であるか、いつ有用になり始めるか、いつ有用でなくなるかの両方を予測する、何らかの示唆を与えてくれます。