Существует ли монада с надписью «Поверхность»?

Question

Канонический «Монада экземпляр» для совместного использования среды плюс недетерминизм следующим образом (с использованием псевдо-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} 

Как правило, при попытке сочетать " (List, Writer и т. д.) со второй монадой m (здесь примерно, Reader), один «обертывает» m вокруг монады-контейнера, как это было сделано выше.

Интересно, то, о следующей потенциальной спецификации Powerset-над-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' достаточно сложно, чтобы затруднить (для меня) проверить, соблюдаются ли законы монады.

Мой вопрос в том, являются ли eta' и bind' действительно монадическими - и если нет, то какой закон (ы) нарушен и какое неожиданное поведение может это соответствовать?

вопрос второстепенный, если предположить, что eta' и bind' не монадические, как можно было бы определить, ли есть функции с этими типами, которые являются?

Answer 1

Веселый вопрос. Вот мой прием - посмотрим, не поймал ли я нигде!

Для начала, я запишет свои подписи (чуть меньше псевдо) Haskell:

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

Перед тем как продолжить, стоит отметить два практических осложнений. Во-первых, как вы уже заметили, благодаря ограничениям Eq и/или Ord нетривиальным, чтобы дать набор Functor или Monad экземпляров; в любом случае, there are ways around it. Во-вторых, и более беспокойно, с типом вы предлагаете для (>>=) необходимо извлечь a с от PSet (r -> a)без какой-либо очевидной поставки r s - или, другими словами, ваш (>>=) требует обхода функции функтора (->) r , Это, конечно, невозможно в общем случае и, как правило, непрактично, если это возможно, по крайней мере, до Хаскелла. В любом случае, для наших спекулятивных целей, можно предположить, что мы можем пройти (->) r, применив эту функцию ко всем возможным значениям r. Я укажу это через ручной волнистый набор universe :: PSet r, названный в честь this package. Я также воспользуюсь universe :: PSet (r -> b) и предположим, что мы можем определить, согласуются ли две функции r -> b на определенном r, даже не требуя ограничения Eq. (Псевдо-Хаскелл становится действительно фальшивым!)

Предварительные замечания сделаны, вот мои версии псевдо-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 и (>=>) в качестве альтернативы (>>=) - поскольку переключение презентаций может заставить работать с вашим экземпляром choic е приятнее. Здесь я буду придерживаться (>>=) презентации Monad.)

Onwards первого закона ...

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. У нас есть нарушение второго закона; поэтому у нас нет монады - по крайней мере, не с предлагаемым здесь экземпляром.

---

Приложения: здесь является актуальной, запускаемой реализацией ваших функций, которые достаточно использовать по крайней мере, для игры с маленькими типами. Он использует вышеупомянутый пакет 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 (!) 

Answer 2

Это несколько проще проверить законы в нотации Клейсли.

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} 

Say всех наших типов a, b, c и r являются Integer и f x = {const x, const -x}. Какие функции находятся в (return `kleisli'` f) 5? Этот набор должен быть f 5, то есть {const 5, const -5}.

Не так ли? Естественно, const 5 и const -5 оба, но не только. Например, \r->if even r then 5 else -5 также присутствует.