> By an occult effect I mean that under the type signature (M a -> M b
> -> M > b) of a particular monad M, the two expressions (const id) and > (liftM2 $ > const id) are equivalent. > > Occult here refers to how the effect of the second parameter blocks > the > effect of the first one. > > In your opinion, is there a better word than occult to describe the > property of such monads? Dear Kim-Ee, TL;DR: Why not the simpler do {y <- b; a} = a My name for your property would be "distribution-like" or "lazy" because of an old post of mine [1]. In that thread we discussed models of probability and I emphasized the property fmap.const = const.return :: a -> M b -> M a (Functor-const) which we will see is equivalent to your occultness. Categorically it can be re-phrased as: "M as a functor maps constant functions to constant functions." First, instead of `const id` I will use `const`, that is, we shall prove const = liftM2 const :: M a -> M b -> M a (occultness) which I believe should be equivalent to your property. For the proof it will be convenient to use the following. Lemma: liftM2 f a b = a >>= (\x -> fmap (f x) b) Proof: We de-sugar the do-notation in the source code for liftM2. liftM2 f a b = a >>= (\x -> b >>= (\y -> return (f x y))) Now use the equation fmap h b = b >>= (\y -> return (h y)) with h instantiated to `f x` to obtain the desired identity. q.e.d. Armed with the Lemma we instantiate f = const. liftM2 const a b = a >>= (\x -> fmap (const x) b) If we now assume my property (Functor-const) then we may re-write to liftM2 const a b = a >>= (\x -> const (return x) b) = a >>= (\x -> return x) = a We have shown (Functor-const) implies (occultness). For the reverse implication, we shall prove (Functor-const) holds with the arguments swapped, that is, we prove the equation \b -> \x -> fmap (const x) b = \b -> \x -> return x Starting with the left-hand side, we eta-expand using the law (k :: a -> M b) x = return x >>= k and obtain \b -> \x -> (return x >>= (\x -> fmap (const x) b)) Using the Lemma we identify the expression in the outermost parentheses as liftM2 const (return x) b which by assumption equals return x, whence we re-write the entire term to \b -> \x -> return x q.e.d. Next consider a law with the same type as (occultness): (=<<).const = const :: M a -> M b -> M a (Kleisli-const) do {y <- b; a} = a (same in do-notation) Any MonadPlus fails this due to the law k =<< mzero = mzero. Categorically it can be re-phrased as "The functor from the Kleisli category of M to Hask preserves constant arrows." I will prove that if M is commutative then (Kleisli-const) implies (occultness). liftM2 const a b = do {x <- a; y <- b; return (const x y)} = do {y <- b; x <- a; return (const x y)} (by commutative) = do {y <- b; x <- a; return x} = do {y <- b; a} = a (by Kleisli-const) Probability distributions have property (Functor-const) because it essentially says that if you map any distribution through a constant function, you will end up with all mass in one place. It is related to lazyness because a priori const a :: M b -> M a is lazy in its argument whereas \b -> a >>= (\x -> fmap (const x) b) is not lazy a priori, i.e. may examine its argument b and execute side- effects. Such lazyness was desired in [1] because inspecting an argument in that context meant computationally expensive sampling of a random distribution. Are there concrete Haskell monads with this property? NonEmpty lists have this property up to multiplicity and order, that is, non-empty finite sets are an example of an occult M. The Reader monad is easily seen to have this property. And that seems to be all. Observe that my two example monads above are indeed commutative and have the property (Kleisli-const). I'm curious whether (Kleisli-const) makes sense in your application. Olaf [1] https://mail.haskell.org/pipermail/haskell-cafe/2019-October/131605.html _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |