31

Set、同様に[]完全に定義されたモナド操作を持っています。問題は、値が制約を満たす必要があるため、制約なしOrdで定義することは不可能です。同じ問題は、可能な値に対して何らかの制約を必要とする他の多くのデータ構造にも当てはまります。return>>=

標準的なトリック ( haskell-cafe の投稿Setで私に提案された) は、継続モナドにラップすることです。ContT基になる型ファンクターに制約があるかどうかは気にしません。制約は、Sets を継続に/からラップ/アンラップする場合にのみ必要になります。

import Control.Monad.Cont
import Data.Foldable (foldrM)
import Data.Set

setReturn :: a -> Set a
setReturn = singleton

setBind :: (Ord b) => Set a -> (a -> Set b) -> Set b
setBind set f = foldl' (\s -> union s . f) empty set

type SetM r a = ContT r Set a

fromSet :: (Ord r) => Set a -> SetM r a
fromSet = ContT . setBind

toSet :: SetM r r -> Set r
toSet c = runContT c setReturn

これは必要に応じて機能します。たとえば、引数を 1 増やすか、そのままにしておく非決定論的関数をシミュレートできます。

step :: (Ord r) => Int -> SetM r Int
step i = fromSet $ fromList [i, i + 1]

-- repeated application of step:
stepN :: Int -> Int -> Set Int
stepN times start = toSet $ foldrM ($) start (replicate times step)

確かに、stepN 5 0利回りfromList [0,1,2,3,4,5]. []代わりにモナドを使用すると、次のようになります

[0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5]

代わりは。

問題は効率です。を呼び出すとstepN 20 0、出力に数秒かかり、stepN 30 0妥当な時間内に終了しません。Set.union各モナド計算の後に実行するのではなく、すべての操作が最後に実行されることがわかります。その結果、指数関数的に多くSetの が構築さunionれ、最後にのみ編集されることになり、これはほとんどのタスクでは受け入れられません。

この構造を効率的にするために、それを回避する方法はありますか? 私は試しましたが、成功しませんでした。

(私は、カリー・ハワード同型とグリベンコの定理から、ある種の理論的限界があるのではないかとさえ思っています。グリベンコの定理は、任意の命題トートロジーφに対して、式¬¬φは直観論的論理で証明できると述べています。しかし、私は、証明の長さは (通常の形式で) 指数関数的に長くなる可能性があります. したがって, 計算を継続モナドにラップすると指数関数的に長くなる場合があるかもしれません?)

4

4 に答える 4

21

モナドは、計算を構造化し、順序付けする特定の方法の 1 つです。モナドのバインドは、魔法のように計算を再構築して、より効率的な方法で実行することはできません。計算を構造化する方法には 2 つの問題があります。

  1. を評価するときstepN 20 0、 の結果はstep 020 回計算されます。これは、計算の各ステップで 1 つの選択肢として 0 が生成され、それが次のステップに渡され、次のステップでも選択肢として 0 が生成されるためです...

    おそらく、ここで少しメモしておくと役立つでしょう。

  2. より大きな問題は、ContT計算の構造に対する の影響です。replicate 20 stepの結果、 の定義、foldrMおよび必要な回数の単純化を展開して、少し等式の推論を行うと、 は次stepN 20 0と同等であることがわかります。

    (...(return 0 >>= step) >>= step) >>= step) >>= ...)

    この式の括弧はすべて左に関連付けられます。これは素晴らしいことです。これは、 が出現するたびに RHS が(>>=)基本的な計算、つまりstep、構成された計算ではなく であることを意味するからです。(>>=)ただし、 forの定義を拡大するとContT、

    m >>= k = ContT $ \c -> runContT m (\a -> runContT (k a) c)

    左への連想チェーンを評価するとき(>>=)、各バインドは新しい計算を現在の継続にプッシュすることがわかりますc。何が起こっているかを説明するために、再び少しの等式推論を使用して、この定義(>>=)と の定義を拡張しrunContT、単純化して次のようにします。

    setReturn 0 `setBind`
    (\x1 -> step x1 `setBind`
        (\x2 -> step x2 `setBind` (\x3 -> ...)...)

    ここで、 が出現するたびにsetBind、RHS 引数が何であるかを自問してみましょう。左端のオカレンスでは、RHS 引数は の後の残りの計算全体setReturn 0です。2 番目のオカレンスでは、 などの後のすべてですstep x1。 の定義にズームインしましょう。setBind

    setBind set f = foldl' (\s -> union s . f) empty set

    ここでfは、計算の残りのすべて、出現する の右側のすべてsetBindを表します。つまり、各ステップで残りの計算を としてキャプチャし、内の要素の数だけf適用します。計算は以前のように初歩的なものではなく、構成されたものであり、これらの計算は何度も繰り返されます。fset

問題の核心は、ContTモナドトランスフォーマーが計算の初期構造を変換していることです。これは、 の左連想チェーンとして意味していましたsetBindが、別の構造を持つ計算、つまり右連想チェーンに変換しています。モナドの法則の 1 つが、ごとmにfg

(m >>= f) >>= g = m >>= (\x -> f x >>= g)

ただし、モナドの法則は、各法則の方程式の両側で複雑さが同じままであることを強制しません。実際、この場合、この計算を構造化する左連想法の方がはるかに効率的です。の左連想チェーンはsetBindすぐに評価されます。これは、基本的なサブ計算のみが複製されるためです。

Setモナドにシューホーニングする他のソリューションも同じ問題を抱えていることがわかりました。特に、set-monadパッケージは同様のランタイムを生成します。その理由は、それも左結合式を右結合式に書き換えるからです。

インターフェイスに従うことを主張することに関して、非常に重要でありながら微妙な問題に指を置いたと思います。そして、それは解決できないと思います。問題は、モナドのバインドの型がSetMonad

(>>=) :: m a -> (a -> m b) -> m b

aつまり、またはのいずれにもクラス制約は許可されませんb。つまり、最初にモナド則を呼び出して右連想チェーンに書き換えずに、バインドを左にネストすることはできません。理由は次のとおりです。与えられ(m >>= f) >>= gた 、計算の型は(m >>= f)の形式m bです。計算の値の(m >>= f)型はbです。しかし、クラス制約を型変数に掛けることができないためb、取得した値が制約を満たすことを知ることができOrdず、したがって、計算できるようにしたいセットの要素としてこの値を使用することはできませんunionの。

于 2012-08-30T14:50:17.820 に答える
2

この場合のパフォーマンスの問題は、の使用によるものではないと思いますCont 

step' :: Int -> Set Int
step' i = fromList [i,i + 1]

foldrM' f z0 xs = Prelude.foldl f' setReturn xs z0
  where f' k x z = f x z `setBind` k

stepN' :: Int -> Int -> Set Int
stepN' times start = foldrM' ($) start (replicate times step')

ベースの実装と同様のパフォーマンスが得られContますが、完全にSet「制限されたモナド」で発生します

Glivenko の定理が (正規化された) プルーフ サイズの指数関数的な増加につながるというあなたの主張を信じているかどうかはわかりませんが、少なくとも Call-By-Need のコンテキストでは。これは、部分証明を任意に再利用できるためです (そして、論理は二次的なものであり、 の証明は 1 つだけ必要ですforall a. ~~(a \/ ~a))。証明はツリーではなく、グラフ (共有) です。

Cont一般に、ラッピングによるパフォーマンス コストが発生する可能性がありますがSet、通常は次の方法で回避できます。

smash :: (Ord r, Ord k) => SetM r r -> SetM k r
smash = fromSet . toSet
于 2012-08-29T23:29:14.343 に答える
1

GHC のConstraintKinds拡張に基づいて、別の可能性を見つけました。アイデアはMonad、許可された値にパラメトリックな制約が含まれるように再定義することです:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RebindableSyntax #-}

import qualified Data.Foldable as F
import qualified Data.Set as S
import Prelude hiding (Monad(..), Functor(..))

class CFunctor m where
    -- Each instance defines a constraint it valust must satisfy:
    type Constraint m a
    -- The default is no constraints.
    type Constraint m a = ()
    fmap   :: (Constraint m a, Constraint m b) => (a -> b) -> (m a -> m b)
class CFunctor m => CMonad (m :: * -> *) where
    return :: (Constraint m a) => a -> m a
    (>>=)  :: (Constraint m a, Constraint m b) => m a -> (a -> m b) -> m b
    fail   :: String -> m a
    fail   = error

-- [] instance
instance CFunctor [] where
    fmap = map
instance CMonad [] where
    return  = (: [])
    (>>=)   = flip concatMap

-- Set instance
instance CFunctor S.Set where
    -- Sets need Ord.
    type Constraint S.Set a = Ord a
    fmap = S.map
instance CMonad S.Set where
    return  = S.singleton
    (>>=)   = flip F.foldMap

-- Example:

-- prints fromList [3,4,5]
main = print $ do
    x <- S.fromList [1,2]
    y <- S.fromList [2,3]
    return $ x + y

(このアプローチの問題は、モナドの値が のような関数である場合です。これm (a -> b)は、 のような制約を満たすことができないためです。したがって、この制約されたモナドに(または) のOrd (a -> b)ようなコンビネータを使用することはできません。)<*>apSet

于 2013-06-13T21:28:31.360 に答える