14

最近、 <-> と <->の関係について質問がありました。DList[]CodensityFree

にこんなものがあるのだろうかと考えさせられたMonadPlus。Codensityモナドは、 ではなく、モナド演算に対してのみ漸近性能を向上させますmplus。

さらに、以前は がありましたがControl.MonadPlus.Free、 のために削除されましたFreeT f []。また、明示的な free がないため、対応するバリアントMonadPlusをどのように表現するかわかりません。improveおそらく次のようなもの

improvePlus :: Functor f => (forall m. (MonadFree f m, MonadPlus m) => m a) -> FreeT f [] a

?

更新:バックトラッキング モナドを使用してそのようなモナドを作成しようとしましたがLogicT、これは次のような方法で定義されているようCodensityです:

newtype LogicT r m a = LogicT { unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

であり、バックトラッキング計算、つまり に適していMonadPlusます。

次に、次lowerLogicのようにを定義lowerCodensityしました。

{-# LANGUAGE RankNTypes, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses,
             UndecidableInstances, DeriveFunctor #-}
import Control.Monad
import Control.Monad.Trans.Free
import Control.Monad.Logic

lowerLogic :: (MonadPlus m) => LogicT m a -> m a
lowerLogic k = runLogicT k (\x k -> mplus (return x) k) mzero

次に、対応するMonadFreeインスタンスを補足した後

instance (Functor f, MonadFree f m) => MonadFree f (LogicT m) where
    wrap t = LogicT (\h z -> wrap (fmap (\p -> runLogicT p h z) t))

定義できる

improvePlus :: (Functor f, MonadPlus mr)
            => (forall m. (MonadFree f m, MonadPlus m) => m a)
            -> FreeT f mr a
improvePlus k = lowerLogic k

kただし、私の最初の実験から、いくつかの例では が とは異なるように見えるため、何かが正しくありませんimprovePlus k。これが基本的な制限でLogicTあり、別のより複雑なモナドが必要なのか、それとも定義lowerLogic(または他の何か) が間違っているのかはわかりません。

4

1 に答える 1

11

以下はすべて、Matthew Pickeringがコメントで投稿したこの非常に興味深い論文に対する私の (誤解) 理解に基づいています。 . すべての結果は彼らのものです。すべての間違いは私のものです。

自由モノイドからDList

直感を構築するために、まず[]Haskell 型のカテゴリの自由モノイドを考えますHask。問題の 1 つ[]は、

(xs `mappend` ys) `mappend` zs = (xs ++ ys) ++ zs

xs次に、 の左にネストされたアプリケーションごとにトラバースと再トラバースが必要な評価mappend。

解決策は、差分リストの形式で CPS を使用することです。

newtype DList a = DL { unDL :: [a] -> [a] }

この論文では、自由なモノイドに縛られていない、これの一般的な形式 (Cayley 表現と呼ばれる) を検討しています。

newtype Cayley m = Cayley{ unCayley :: Endo m }

変換あり

toCayley :: (Monoid m) => m -> Cayley m
toCayley m = Cayley $ Endo $ \m' -> m `mappend` m'

fromCayley :: (Monoid m) => Cayley m -> m
fromCayley (Cayley k) = appEndo k mempty

一般化の 2 つの方向

Hask上記の構成を 2 つの方法で一般化できHaskます。 すなわち モナド。第二に、代数構造を準セミリングに富化することによって。

FreeモナドCodensity

任意の Haskell (endo)functorに対して、フリー モナドfを構築できます。これには、Cayley 表現を使用する類似の解決策を使用して、左にネストされたバインドに関する類似のパフォーマンスの問題があり ます。 Free fCodensity

単なるモノイドではなく準セミリング

ここで、Haskell の現役プログラマーがよく知っている概念のレビューをやめ、その目標に焦点を合わせ始めます。近接セミリングはリングに似ていますが、加算と乗算の両方がモノイドである必要があるだけなので、より単純です。2 つの操作間の接続は、次のとおりです。

zero |*| a = zero
(a |+| b) |*| c = (a |*| c) |+| (b |*| c)

ここで(zero, |+|)、 と(one, |*|)は共有ベース上の 2 つのモノイドです。

class NearSemiring a where
    zero :: a
    (|+|) :: a -> a -> a
    one :: a
    (|*|) :: a -> a -> a

フリーニアセミリング ( over Hask) は、次の Forestタイプであることがわかります。

newtype Forest a = Forest [Tree a]
data Tree a = Leaf | Node a (Forest a)

instance NearSemiring (Forest a) where
    zero = Forest []
    one = Forest [Leaf]
    (Forest xs) |+| (Forest ys) = Forest (xs ++ ys)
    (Forest xs) |*| (Forest ys) = Forest (concatMap g xs)
      where
        g Leaf = ys
        g (Node a n) = [Node a (n |*| (Forest ys))]

(可換性や逆数がないのは良いことです。 それらは自明とはかけ離れた自由な表現を作成します ...)

次に、2 つのモノイド構造に Cayley 表現を 2 回適用します。

ただし、単純にこれを行うと、適切な表現が得られません。近接セミリングを表現したいため、選択した 1 つのモノイド構造だけでなく、ニアセミリング構造全体を考慮する必要があります。[...] [W]e は、自己同型写像​​上の準同型写像のセミリングを取得しDC(N)ます。

newtype DC n = DC{ unDC :: Endo (Endo n) }

instance (Monoid n) => NearSemiring (DC n) where
    f |*| g = DC $ unDC f `mappend` unDC g
    one = DC mempty
    f |+| g = DC $ Endo $ \h -> appEndo (unDC f) h `mappend` h
    zero = DC $ Endo $ const mempty

(構造を 2 回使用していることを強調するために、ここでの実装を論文から少し変更しましたEndo)。これを一般化すると、2 つのレイヤーは同じではなくなります。その後、同紙は次のように続けています。

は単位を保存しないため、 intorepから準半準準同型ではないことに注意してください [...] それにもかかわらず、[...] 値を表現に持ち上げると、準半準上の計算のセマンティクスが保存されます。 、そこでニアセミリング計算を行い、元のニアセミリングに戻ります。NDC(N)

MonadPlusほぼセミリングです

次に論文は、MonadPlus型クラスを半準規則に対応するように再定式化することを続けます: (mzero, mplus)is monoidal:

m `mplus` mzero = m
mzero `mplus` m = m
m1 `mplus` (m2 `mplus` m3) = (m1 `mplus` m2) `mplus` m3

そして期待通りにモナドモノイドと相互作用します:

join mzero = mzero
join (m1 `mplus` m2) = join m1 `mplus` join m2

または、バインドを使用して:

mzero >>= _ = mzero
(m1 `mplus` m2) >>= k = (m1 >>= k) `mplus` (m2 >>= k)

ただし、これらは から の既存の型クラスの規則ではなく、次のようにリストされています。MonadPlusbase

mzero >>= _  =  mzero
_ >> mzero   =  mzero

この論文ではMonadPlus、セミリングに近い法則を満たすインスタンスを「非決定性モナド」と呼び、 との設定が の反例であるため、非決定性モナドではないが非決定性モナドではないMaybe例を挙げています。MonadPlusm1 = Just Nothingm2 = Just (Just False)join (m1 `mplus` m2) = join m1 `mplus` join m2

非決定性モナドの自由表現と Cayley 表現

すべてをまとめると、一方で - のForestような自由な非決定性モナドがあります。

newtype FreeP f x = FreeP { unFreeP :: [FFreeP f x] }
data FFreeP f x = PureP x | ConP (f (FreeP f x))

instance (Functor f) => Functor (FreeP f) where
    fmap f x = x >>= return . f

instance (Functor f) => Monad (FreeP f) where
    return x = FreeP $ return $ PureP x
    (FreeP xs) >>= f = FreeP (xs >>= g)
      where
        g (PureP x) = unFreeP (f x)
        g (ConP x) = return $ ConP (fmap (>>= f) x)

instance (Functor f) => MonadPlus (FreeP f) where
    mzero = FreeP mzero
    FreeP xs `mplus` FreeP ys = FreeP (xs `mplus` ys)

もう 1 つは、2 つのモノイド層の二重 Cayley 表現です。

newtype (:^=>) f g x = Ran{ unRan :: forall y. (x -> f y) -> g y }
newtype (:*=>) f g x = Exp{ unExp :: forall y. (x -> y) -> (f y -> g y) }

instance Functor (g :^=> h) where
    fmap f m = Ran $ \k -> unRan m (k . f)

instance Functor (f :*=> g) where
    fmap f m = Exp $ \k -> unExp m (k . f)

newtype DCM f x = DCM {unDCM :: ((f :*=> f) :^=> (f :*=> f)) x}

instance Monad (DCM f) where
    return x = DCM $ Ran ($x)
    DCM (Ran m) >>= f = DCM $ Ran $ \g -> m $ \a -> unRan (unDCM (f a)) g

instance MonadPlus (DCM f) where
    mzero = DCM $ Ran $ \k -> Exp (const id)
    mplus m n = DCM $ Ran $ \sk -> Exp $ \f fk -> unExp (a sk) f (unExp (b sk) f fk)
      where
        DCM (Ran a) = m
        DCM (Ran b) = n

caylize :: (Monad m) => m a -> DCM m a
caylize x = DCM $ Ran $ \g -> Exp $ \h m -> x >>= \a -> unExp (g a) h m

-- I wish I called it DMC earlier...
runDCM :: (MonadPlus m) => DCM m a -> m a
runDCM m = unExp (f $ \x -> Exp $ \h m -> return (h x) `mplus` m) id mzero
  where
    DCM (Ran f) = m

この論文は、次の非決定性モナドで実行されている計算の例を示していますFreeP。

anyOf :: (MonadPlus m) => [a] -> m a
anyOf [] = mzero
anyOf (x:xs) = anyOf xs `mplus` return x

確かに、一方で

length $ unFreeP (anyOf [1..100000] :: FreeP Identity Int)

ケイリーの変身バージョン

length $ unFreeP (runDCM $ anyOf [1..100000] :: FreeP Identity Int)

即座に戻ります。

于 2015-09-01T13:56:28.653 に答える