读卡器电源单功能是否存在? [英] Does a Powerset-over-Reader monad exist?

问题描述

用于环境共享和不确定性的规范化"Monad实例"如下(使用伪Haskell，因为Haskell的Data.Set当然不是单子):

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(列表，Writer等)之类的容器" monad与第二个monad m(此处大致为Reader)组合时，一个"wrap" 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和rb'的rb r == rb' r)，但是bind'太复杂了，以至于(对我来说)很难检查单子法是否成立.

那么，我的问题是eta'和bind'是否真的是一元论的，如果不是，则违反了哪一条法律，这可能对应于哪种意外行为? >

第二个问题是，假设eta'和bind'不是一元的，那么如何确定是否具有这些类型的函数?

解决方案

有趣的问题.这是我的看法-让我们看看我是否在任何地方都没事！

首先，我将在(略为伪的)Haskell中拼写您的签名:

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

在继续之前，值得一提的是两个实际的并发症.首先，正如您已经观察到的，由于Eq和/或Ord的限制，赋予集合Functor或Monad实例并非易事；在任何情况下，都可以解决.其次，更令人担忧的是，对于您为(>>=)提出的类型，有必要从PSet (r -> a) 中提取a s，而没有任何明显的r s 供给-或者，在换句话说，您的(>>=)要求遍历函数functor (->) r.当然，这在一般情况下是不可能的，并且即使在可能的情况下也往往是不切实际的-至少就Haskell而言.在任何情况下，出于推测的目的，最好假设我们可以通过将函数应用于所有可能的r值来遍历(->) r.我将通过一个波浪形的universe :: PSet r集合来表明这一点，该集合的名称是对 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 (!)

The canonical 'Monad instance' for environment sharing plus nondeterminism is as follows (using pseudo-Haskell, since Haskell's Data.Set isn't, of course, 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}

Generally, when trying to combine a 'container' monad like Powerset (List, Writer, etc) with a second monad m (here, roughly, Reader), one 'wraps' m around the container monad, as done above.

I wonder, then, about the following potential Powerset-over-Reader specification:

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}

This doesn't seem obviously crazy (I do realize that GHCi can't check rb r == rb' r for many rb and rb'), but bind' is complicated enough to make it difficult (for me) to check whether the monad laws hold.

My question, then, is whether eta' and bind' really are monadic -- and, if not, which of the law(s) is violated, and what sort of unexpected behavior might this correspond to?

A secondary question, assuming that eta' and bind' aren't monadic, is how one might ascertain whether there are functions with these types that are?

解决方案

Fun question. Here is my take -- let's see if I didn't goof anywhere!

To begin with, I will spell your signatures in (slightly less pseudo) Haskell:

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

Before continuing, it is worth mentioning two practical complications. Firstly, as you have already observed, thanks to Eq and/or Ord constraints it is non-trivial to give sets Functor or Monad instances; in any case, there are ways around it. Secondly, and more worryingly, with the type you propose for (>>=) it is necessary to extract as from PSet (r -> a) without having any obvious supply of rs -- or, in other words, your (>>=) demands a traversal of the function functor (->) r. That, of course, is not possible in the general case, and tends to be impractical even when possible -- at least as far as Haskell is concerned. In any case, for our speculative purposes it is fine to suppose we can traverse (->) r by applying the function to all possible r values. I will indicate this through a hand-wavy universe :: PSet r set, named in tribute to this package. I will also make use of an universe :: PSet (r -> b), and assume we can tell whether two r -> b functions agree on a certain r even without requiring an Eq constraint. (The pseudo-Haskell is getting quite fake indeed!)

Preliminary remarks made, here are my pseudo-Haskell versions of your methods:

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

Next, the monad laws:

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

(By the way, when doing this sort of thing it is good to keep in mind the other presentations of the class we are working with -- in this case, we have join and (>=>) as alternatives to (>>=) -- as switching presentations might make working with your instance of choice more pleasant. Here I will stick with the (>>=) presentation of Monad.)

Onwards to the first law...

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

One down, two to go.

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, therefore, might possibly be a much larger set than f y. We have a violation of the second law; therefore, we don't have a monad -- at least not with the instance proposed here.

---

Appendix: here is an actual, runnable implementation of your functions, which is usable enough at least for playing with small types. It takes advantage of the aforementioned universe package.

{-# 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 (!)

这篇关于读卡器电源单功能是否存在?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！