【问题标题】:Does a Powerset-over-Reader monad exist?Powerset-over-Reader monad 是否存在?
【发布时间】:2017-07-04 21:25:40
【问题描述】:

环境共享和不确定性的规范“Monad 实例”如下(使用伪 Haskell,因为 Haskell 的 Data.Set 当然不是 monadic):

eta :: a -> r -> {a} -- '{a}' means the type of a set of a's
eta x = \r -> {x}

bind :: (r -> {a}) -> (a -> r -> {b}) -> r -> {b}
m `bind` f = \r -> {v | x ∈ m r, v ∈ f x r}

通常,当尝试将像 Powerset(List、Writer 等)这样的“容器”monad 与第二个 monad m(这里,大致是 Reader)结合起来时,一个“包裹”m 围绕容器 monad,如上所述。

然后,我想知道以下潜在的 Powerset-over-Reader 规范:

eta' :: a -> {r -> a}
eta' x = {\r -> x}

bind' :: {r -> a} -> (a -> {r -> b}) -> {r -> b}
m `bind'` f = {rb | x <- m, ∀r: ∃rb' ∈ f (x r): rb r == rb' r}

这似乎并不明显(我确实意识到 GHCi 无法检查 rb r == rb' r 的许多 rbrb'),但 bind' 足够复杂,以至于(对我而言)很难检查单子定律是否成立。

那么,我的问题是,eta'bind' 是否真的是一元的——如果不是,那么违反了哪条法律,这可能对应于什么样的意外行为?

第二个问题,假设 eta'bind' 不是一元的,如何确定是否这些类型的函数是?

【问题讨论】:

    标签: haskell monads reader-monad


    【解决方案1】:

    有趣的问题。这是我的看法 - 让我们看看我是否没有在任何地方搞砸!

    首先,我将用(稍微不那么伪的)Haskell 拼写你的签名:

    return :: a -> PSet (r -> a)
    (>>=) :: PSet (r -> a) -> (a -> PSet (r -> b)) -> PSet (r -> b))
    

    在继续之前,值得一提的是两个实际问题。首先,正如您已经观察到的,由于Eq 和/或Ord 约束,给集合FunctorMonad 实例是不平凡的;无论如何,there are ways around it。其次,更令人担忧的是,对于您为 (&gt;&gt;=) 建议的类型,有必要从 PSet (r -&gt; a) 中提取 as 而没有任何明显的 rs 供应 - 或者,在换句话说,您的(&gt;&gt;=) 需要遍历函数函子(-&gt;) r。当然,这在一般情况下是不可能的,即使在可能的情况下也往往是不切实际的——至少就 Haskell 而言。无论如何,为了我们的推测目的,假设我们可以通过将函数应用于所有可能的r 值来遍历(-&gt;) r。我将通过一个手工波浪形的universe :: PSet r 集合来表明这一点,以向this package 致敬。我还将使用universe :: PSet (r -&gt; b),并假设我们可以判断两个r -&gt; b 函数是否同意某个r,即使不需要Eq 约束。 (伪 Haskell 确实越来越假了!)

    初步评论,这是我的伪 Haskell 版本的方法:

    return :: a -> PSet (r -> a)
    return x = singleton (const x)
    
    (>>=) :: PSet (r -> a) -> (a -> PSet (r -> b)) -> PSet (r -> b))
    m >>= f = unionMap (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                any (\rb' -> rb' r == rb r) (f (x r)))
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) m
        where
        unionMap f = unions . map f
        intersectionMap f = intersections . map f
    

    接下来,单子定律:

    m >>= return = m
    return y >>= f = f y
    m >>= f >>= g = m >>= \y -> f y >>= g
    

    (顺便说一句,在做这种事情时,最好记住我们正在使用的课程的其他演示文稿 - 在这种情况下,我们有 join(&gt;=&gt;) 作为 @ 的替代品987654347@ -- 因为切换演示文稿可能会使您选择的实例更愉快。这里我将坚持使用Monad(&gt;&gt;=) 演示文稿。)

    继续第一定律...

    m >>= return = m
    m >>= return -- LHS
    unionMap (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                any (\rb' -> rb' r == rb r) (singleton (const (x r))))
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) m
    unionMap (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                const (x r) r == rb r)
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) m
    unionMap (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                x r == rb r)
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) m
    -- In other words, rb has to agree with x for all r. 
    unionMap (\x -> singleton x) m
    m -- RHS
    

    一个下来,两个去。

    return y >>= f = f y
    return y -- LHS
    unionMap (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                any (\rb' -> rb' r == rb r) (f (x r)))
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) (singleton (const y))
    (\x ->
        intersectionMap (\r ->
            filter (\rb -> 
                any (\rb' -> rb' r == rb r) (f (x r)))
                (universe :: PSet (r -> b)))
            (universe :: PSet r)) (const y)
    intersectionMap (\r ->
        filter (\rb -> 
            any (\rb' -> rb' r == rb r) (f (const y r)))
            (universe :: PSet (r -> b)))
        (universe :: PSet r)
    intersectionMap (\r ->
        filter (\rb -> 
            any (\rb' -> rb' r == rb r) (f y)))
            (universe :: PSet (r -> b)))
        (universe :: PSet r)
    -- This set includes all functions that agree with at least one function
    -- from (f y) at each r.
    

    因此,return y &gt;&gt;= f 可能是一个比f y 大得多的集合。我们违反了第二定律;因此,我们没有 monad —— 至少在此处提出的实例中没有。


    附录:这是一个实际的、可运行的函数实现,它至少可以用于小类型。它利用了前面提到的universe 包。

    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    module FunSet where
    
    import Data.Universe
    import Data.Map (Map)
    import qualified Data.Map as M
    import Data.Set (Set)
    import qualified Data.Set as S
    import Data.Int
    import Data.Bool
    
    -- FunSet and its would-be monad instance
    
    newtype FunSet r a = FunSet { runFunSet :: Set (Fun r a) }
        deriving (Eq, Ord, Show)
    
    fsreturn :: (Finite a, Finite r, Ord r) => a -> FunSet r a
    fsreturn x = FunSet (S.singleton (toFun (const x)))
    
    -- Perhaps we should think of a better name for this...
    fsbind :: forall r a b.
        (Ord r, Finite r, Ord a, Ord b, Finite b, Eq b)
        => FunSet r a -> (a -> FunSet r b) -> FunSet r b
    fsbind (FunSet s) f = FunSet $
        unionMap (\x ->
            intersectionMap (\r ->
                S.filter (\rb ->
                    any (\rb' -> funApply rb' r == funApply rb r)
                        ((runFunSet . f) (funApply x r)))
                    (universeF' :: Set (Fun r b)))
                (universeF' :: Set r)) s
    
    toFunSet :: (Finite r, Finite a, Ord r, Ord a) => [r -> a] -> FunSet r a
    toFunSet = FunSet . S.fromList . fmap toFun
    
    -- Materialised functions
    
    newtype Fun r a = Fun { unFun :: Map r a }
        deriving (Eq, Ord, Show, Functor)
    
    instance (Finite r, Ord r, Universe a) => Universe (Fun r a) where
        universe = fmap (Fun . (\f ->
            foldr (\x m ->
                M.insert x (f x) m) M.empty universe))
            universe
    
    instance (Finite r, Ord r, Finite a) => Finite (Fun r a) where
        universeF = universe
    
    funApply :: Ord r => Fun r a -> r -> a
    funApply f r = maybe
        (error "funApply: Partial functions are not fun")
        id (M.lookup r (unFun f))
    
    toFun :: (Finite r, Finite a, Ord r) => (r -> a) -> Fun r a
    toFun f = Fun (M.fromList (fmap ((,) <$> id <*> f) universeF))
    
    -- Set utilities
    
    unionMap :: (Ord a, Ord b) => (a -> Set b) -> (Set a -> Set b)
    unionMap f = S.foldl S.union S.empty . S.map f
    
    -- Note that this is partial. Since for our immediate purposes the only
    -- consequence is that r in FunSet r a cannot be Void, I didn't bother
    -- with making it cleaner.
    intersectionMap :: (Ord a, Ord b) => (a -> Set b) -> (Set a -> Set b)
    intersectionMap f s = case ss of
        [] -> error "intersectionMap: Intersection of empty set of sets"
        _ -> foldl1 S.intersection ss
        where
        ss = S.toList (S.map f s)
    
    universeF' :: (Finite a, Ord a) => Set a
    universeF' = S.fromList universeF
    
    -- Demo
    
    main :: IO ()
    main = do
        let andor = toFunSet [uncurry (&&), uncurry (||)]
        print andor -- Two truth tables
        print $ funApply (toFun (2+)) (3 :: Int8) -- 5
        print $ (S.map (flip funApply (7 :: Int8)) . runFunSet)
            (fsreturn (Just True)) -- fromList [Just True]
        -- First monad law demo
        print $ fsbind andor fsreturn == andor -- True
        -- Second monad law demo
        let twoToFour = [ bool (Left False) (Left True)
                        , bool (Left False) (Right False)]
            decider b = toFunSet
                (fmap (. bool (uncurry (&&)) (uncurry (||)) b) twoToFour)
        print $ fsbind (fsreturn True) decider == decider True -- False (!)
    

    【讨论】:

    • &gt;&gt;=的定义如何与OP中的bind'对应?量词和包含相等比较的守卫在哪里?使用原始伪代码,m &gt;&gt;= return{rb | x &lt;- m, ∀r: rb r == x r} 在集合论中实际上只是 m。在实际的 Haskell 中可能无法准确捕获给定的语义,但我认为问题不是在问这个问题。
    • 我想我同意上述评论。在 OP 中 bind'f (x r)rb r 都接收相同的环境 r。我不明白你的(仍然很可爱)&gt;&gt;= 是如何保证的。
    • @user2407038 [1/2] 在上面的伪 Haskell 中,量词由 fromList [minBound..maxBound] 表示,表示包含所有可能的 r 值的集合。也就是说……
    • ... [2/2] 正如您和@SimonC 指出的那样,我省略了相等性,因为我误解了定义。让我们删除错误的部分,看看我能不能做得更好。
    • 是的,太好了。我不禁注意到这里的问题与here 讨论的问题相似。我仍然很想知道如何确定这些类型是否可以/不可以单子操作。
    【解决方案2】:

    用 Kleisli 表示法来验证定律要容易一些。

    kleisli' :: (a -> {r -> b}) -> (b -> {r -> c}) -> (a -> {r -> c})
    g `kleisli'` f = \z -> {rb | x <- g z, ∀r: ∃rb' ∈ f (x r): rb r == rb' r}
    

    让我们尝试验证return `kleisli'` f = f

    (\a -> {\r->a}) `kleisli'` f = 
    \z -> {rb | x <- {\r->z}, ∀r: ∃rb' ∈ f (x r): rb r == rb' r} = 
    \z -> {rb | ∀r: ∃rb' ∈ f z: rb r == rb' r}
    

    假设我们所有的类型abcrIntegerf x = {const x, const -x}(return `kleisli'` f) 5 中有哪些功能?这个集合应该是f 5,也就是{const 5, const -5}

    是吗?当然const 5const -5 都在,但不仅如此。比如\r-&gt;if even r then 5 else -5也在里面。

    【讨论】:

    • 很好的例子,很高兴在这里也能用Monad的不同表示和更紧凑的符号进行验证。
    猜你喜欢
    • 1970-01-01
    • 2018-03-26
    • 2017-08-16
    • 1970-01-01
    • 2019-11-30
    • 2017-06-22
    • 1970-01-01
    • 2021-07-18
    • 2015-12-31
    相关资源
    最近更新 更多