8

用于环境共享和不确定性的规范“Monad 实例”如下（使用伪 Haskell，因为 HaskellData.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许多rband rb'），但bind'它足够复杂，以至于（对我而言）难以检查单子定律是否成立。

那么，我的问题是，是否eta'并且bind'真的是单子的——如果不是，违反了哪条法律，这可能对应于什么样的意外行为？

第二个问题，假设它不是一元的eta'，bind'是如何确定是否存在具有这些类型的函数？

4

2 回答 2

8

有趣的问题。这是我的看法 - 让我们看看我是否没有在任何地方犯错！

首先，我将用（稍微不那么伪的）Haskell 拼写你的签名：

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

在继续之前，值得一提的是两个实际的并发症。首先，正如您已经观察到的，由于Eq和/或Ord约束，给出集合Functor或Monad实例并非易事；无论如何，有办法绕过它。其次，更令人担忧的是，对于您建议的类型，(>>=)有必要在没有任何明显 s 供应的情况下从中提取 sa -或者换句话说，您需要遍历函数 functor 。当然，这在一般情况下是不可能的，即使在可能的情况下也往往是不切实际的——至少就 Haskell 而言。无论如何，为了我们的推测目的，假设我们可以遍历PSet (r -> a) r(>>=)(->) r(->) r通过将函数应用于所有可能的r值。我将通过一个手工波浪形的universe :: PSet r套装来表明这一点，以向这个包致敬。我还将使用universe :: PSet (r -> b), 并假设我们可以判断两个r -> 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并且(>=>)作为替代(>>=)- 因为切换演示文稿可能会与您的选择的例子更令人愉快。这里我将坚持(>>=)介绍Monad。）

继续第一条法律...

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 >>= 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 (!)
于 2017-02-16T03:20:22.570 回答
4

用 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}

说出我们所有的类型a,b和are cand 。有哪些功能？这个集合应该是，也就是。rIntegerf x = {const x, const -x}(return `kleisli'` f) 5f 5{const 5, const -5}

是吗？自然const 5和const -5两者都在，但不仅如此。例如，\r->if even r then 5 else -5也在。

于 2017-02-16T14:17:14.843 回答