18

さて、ライターモナドを使用すると、[通常]ある種のコンテナーにデータを書き込んで、最後にそのコンテナーを元に戻すことができます。ほとんどの実装では、「コンテナ」は実際には任意のモノイドにすることができます。

現在、「リーダー」モナドもあります。これは、あなたが思うかもしれませんが、二重の操作を提供します-ある種のコンテナから、一度に1つのアイテムを段階的に読み取ります。実際、これは通常のリーダーモナドが提供する機能ではありません。（代わりに、セミグローバル定数への簡単なアクセスを提供するだけです。）

通常のライターモナドとデュアルのモナドを実際に書くには、モノイドとデュアルのある種の構造が必要になります。

  1. この二重構造が何であるかを誰かが知っていますか？
  2. 誰かがこのモナドを書いたことがありますか？よく知られている名前はありますか？
4

3 に答える 3

32

モノイドの双対はコモノイドです。モノイドが (同形のもの) として定義されていることを思い出してください。

 class Monoid m where
    create :: () -> m
    combine :: (m,m) -> m

これらの法律で

 combine (create (),x) = x
 combine (x,create ()) = x
 combine (combine (x,y),z) = combine (x,combine (y,z))

したがって

 class Comonoid m where
    delete :: m -> ()
    split :: m -> (m,m)

いくつかの標準操作が必要です

 first :: (a -> b) -> (a,c) -> (b,c)
 second :: (c -> d) -> (a,c) -> (a,d)

 idL :: ((),x) -> x
 idR :: (x,()) -> x

 assoc :: ((x,y),z) -> (x,(y,z))

のような法律で

idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)

この型クラスが奇妙に見えるのには理由があります。インスタンスがあります

instance Comonoid m where
   split x = (x,x)
   delete x = ()

Haskell では、これが唯一のインスタンスです。reader を writer の正確な双対として再キャストできますが、comonoid のインスタンスは 1 つしかないため、標準の reader 型と同型の何かが得られます。

すべての型をコモノイドにすることで、「デカルト閉圏」の「デカルト」圏になります。「モノイド閉カテゴリ」は CCC に似ていますが、このプロパティがなく、部分構造型システムに関連しています。線形論理の魅力の 1 つは、これが示す対称性の向上です。一方、部分構造型を使用すると、より興味深いプロパティ (リソース管理などのサポート) を持つコモノイドを定義できます。実際、これにより、C++ でのコピー コンストラクターとデストラクタの役割を理解するためのフレームワークが提供されます (ただし、C++ ではポインターが存在するため、重要なプロパティは強制されません)。

編集: コモノイドからのリーダー

newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete

instance Comonoid r => Monad (Reader r) where
   return x = Reader $ \r -> forget (r,x)
   m >>= f = \r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2

ask :: Comonoid r => Reader r r
ask = Reader id

上記のコードでは、バインド後にすべての変数が 1 回だけ使用されることに注意してください (したがって、これらはすべて線形型で型付けされます)。モナドの法則の証明は自明であり、コモノイドの法則のみが機能する必要があります。したがって、Reader本当に は に双対Writerです。

于 2013-03-14T20:09:34.640 に答える
13

モノイドのデュアルがどうあるべきか完全にはわかりませんが、デュアルを何かの反対として（おそらく間違って）考えています（単にコモナドがモナドのデュアルであり、すべて同じ操作をしていることに基づいています）しかし、逆の方法です）。それを基にするのではなくmappend、mempty私はそれを基にするでしょう：

fold :: (Foldable f, Monoid m) => f m -> m

ここでfをリストに特化すると、次のようになります。

fold :: Monoid m => [m] -> m

これには、特にすべてのモノイドクラスが含まれているように見えます。

mempty == fold []
mappend x y == fold [x, y]

したがって、この異なるモノイドクラスのデュアルは次のようになると思います。

unfold :: (Comonoid m) => m -> [m]

これは、ここでハッキングで見たモノイド階乗クラスによく似ています。

したがって、これに基づいて、あなたが説明する「リーダー」モナドは供給モナドになると思います。供給モナドは事実上、値のリストの状態トランスフォーマーであるため、いつでもリストからアイテムを供給することを選択できます。この場合、リストはunfold.supplyモナドの結果になります。

私はHaskellの専門家でも、専門家の理論家でもないことを強調する必要があります。しかし、これはあなたの説明が私に考えさせたものです。

于 2013-03-14T19:21:15.913 に答える
3

供給は状態に基づいているため、一部のアプリケーションでは最適ではありません。たとえば、提供された値 (ランダムなど) の無限ツリーを作成したい場合があります。

tree :: (Something r) => Supply r (Tree r)
tree = Branch <$> supply <*> sequenceA [tree, tree]

ただし、供給は州に基づいているため、ツリーの一番左のパスにあるものを除いて、すべてのラベルが一番下になります。

分割可能なものが必要です（@ PhillipJFのようにComonoid）。しかし、これをモナドにしようとすると問題があります:

newtype Supply r a = Supply { runSupply :: r -> a }

instance (Splittable r) => Monad (Supply r) where
    return = Supply . const
    Supply m >>= f = Supply $ \r ->
        let (r',r'') = split r in
        runSupply (f (m r')) r''

モナドの法則は を要求するので、それは ..の定義でf >>= return = fそれを意味しますが、モナドの法則はそれも要求します。したがって、 forがモナドになると、通常の old が再び返されます。r'' = r(>>=)return x >>= f = f xr' = rSupplysplit x = (x,x)Reader

Haskell で使用される多くのモナドは、実際のモナドではありません。つまり、それらは、ある同値関係までの法則のみを満たします。たとえば、法則に従って変換すると、多くの非決定性モナドは異なる順序で結果を返します。特定の要素がwhereではなく、出力のリストに表示されるかどうかを知りたい場合は、モナドで十分です。

Supplyある同値関係までモナドであることを許せば、非自明な分裂を得ることができます。たとえば、value-supplyは、(マジックを使用して) リストから一意のラベルを指定されていない順序で分配する分割可能なエンティティを構築します。unsafe*したがって、value supply の supply モナドは、ラベルの順列までのモナドになります。多くのアプリケーションで必要なのはこれだけです。そして、実際には、機能があります

runSupply :: (forall r. Eq r => Supply r a) -> a

この等価関係を抽象化して、明確に定義された純粋なインターフェイスを提供します。これは、ラベルに対してできることは、それらが等しいかどうかを確認することだけであり、ラベルを並べ替えても変わらないためです。これrunSupplyが で許可する唯一の観察である場合Supply、Supply一意のラベルの供給は実モナドです。

于 2013-03-14T20:32:55.477 に答える