Sim*_*n C 8 monads haskell reader-monad
用于环境共享和非确定性的规范"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许多rb和rb'),但是bind'复杂到足以让我(很难)检查monad法律是否成立.
我的问题,那么,无论是eta'和bind'真的是一元-和,如果不是,该法律(S)为侵犯,以及什么样的意外行为可能此对应？
假设eta'并且bind'不是monadic 的第二个问题是人们如何确定这些类型的函数是否存在？
有趣的问题.这是我的看法 - 让我们看看我是不是在任何地方蠢蠢欲动!
首先,我将在(稍微不那么伪)Haskell中拼写您的签名:
return :: a -> PSet (r -> a)
(>>=) :: PSet (r -> a) -> (a -> PSet (r -> b)) -> PSet (r -> b))
在继续之前,值得一提的是两个实际的并发症.首先,正如您已经观察到的那样,由于Eq和/或Ord约束,给出集合Functor或Monad实例是非常重要的; 在任何情况下,都有办法解决它.其次,更令人担忧的是,对于你提出的类型(>>=),有必要a从PSet (r -> a) 没有任何明显的rs - 提供s - 或者换句话说,你的(>>=)要求遍历函数functor (->) r.当然,这在一般情况下是不可能的,并且即使在可能的情况下也往往是不切实际的 - 至少就Haskell而言.在任何情况下,出于我们的推测目的,可以假设我们可以(->) r通过将函数应用于所有可能的r值来遍历.我将通过一个手工波浪universe :: PSet r组来表明这一点,以此包装为荣.我还将使用a 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
接下来,monad法则:
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 (!)