Administrator

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?   KimEe
_______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
Administrator

(I'll respond with the original subject heading and with the full thread of Michal's reply copied below so that the convo stays in one place.) Hi Michal, I'm afraid you caricaturize my original email out of proportion here: > class Monoid m => T m o where > i :: o > t > c :: t > o > Bool <snip> Not only is your T type class more complicated than what I wrote, it's also riddled with suggestive but possibly misleading oneletter variable names. You even ask your reader to stay wary of the laws (snipped) that might not even be correctly stated. I do no such thing in my original email. In fact, the modicum of Haskell background that suffices for grasping the original query is only the next level up from recognizing that a universally polymorphic function of type (a > a > a) is inhabited by exactly two functions, modulo bottom. From there it's one more step to how (forall m. Monad m => m a > m b > m b) is inhabited by a mere handful of functions, again barring bottom. My query makes reference to how two of the those functions, namely (const id) and (liftM2 $ const id) are equivalent with some monads but not others. I even gave further clarification in plain English about "how the effect of the second parameter blocks the effect of the first." At the top of your email you wrote: > It is easier to understand it if: > 1. You give some examples of such monads > 2. Describe how this property arises > 3. Tell how whether the law is unique or part of a list of laws applicable Are you alluding to the XY problem? I assure you I labor under no such tunnelvision. Were I to request a cromulent adjective for the seventh powers of the natural numbers, what progress do you make by making counterdemands for examples? Behind which string of digits does the pellucid word hide itself?  KimEe On Wed, Nov 11, 2020 at 8:36 PM Michal J Gajda <[hidden email]> wrote:
 KimEe
_______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
Also, I think you want to say occlude, which means block from view, as opposed to occult which refers to magic and such. Which may, or may not be what you want.
Mike
Michael Matsko
From: HaskellCafe <[hidden email]> on behalf of KimEe Yeoh <[hidden email]>
Sent: Wednesday, November 11, 2020 8:33:34 PM To: Haskell Cafe <[hidden email]>; [hidden email] <[hidden email]> Subject: Re: [Haskellcafe] What to call Occult Effects (I'll respond with the original subject heading and with the full thread of Michal's reply copied below so that the convo stays in one place.)
Hi Michal, I'm afraid you caricaturize my original email out of proportion here:
> class Monoid m => T m o where
> i :: o > t
> c :: t > o > Bool
<snip>
Not only is your T type class more complicated than what I wrote, it's also riddled with suggestive but possibly misleading oneletter variable names. You even ask your reader to stay wary of the laws (snipped) that might not even be correctly
stated.
I do no such thing in my original email.
In fact, the modicum of Haskell background that suffices for grasping the original query is only the next level up from recognizing that a universally polymorphic function of type (a > a > a) is inhabited by exactly two functions, modulo bottom.
From there it's one more step to how (forall m. Monad m => m a > m b > m b) is inhabited by a mere handful of functions, again barring bottom. My query makes reference to how two of the those functions, namely (const id) and (liftM2 $ const
id) are equivalent with some monads but not others.
I even gave further clarification in plain English about "how the effect of the second parameter blocks the effect of the first."
At the top of your email you wrote:
> It is easier to understand it if:
> 1. You give some examples of such monads
> 2. Describe how this property arises
> 3. Tell how whether the law is unique or part of a list of laws applicable
Are you alluding to the XY problem?
I assure you I labor under no such tunnelvision.
Were I to request a cromulent adjective for the seventh powers of the natural numbers, what progress do you make by making counterdemands for examples?
Behind which string of digits does the pellucid word hide itself?
 KimEe
On Wed, Nov 11, 2020 at 8:36 PM Michal J Gajda <[hidden email]> wrote:
 KimEe
_______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
Administrator

In reply to this post by KimEe Yeoh
On Thu, Nov 12, 2020 at 12:17 AM Justin Bailey <[hidden email]> wrote: Looking up the definition "occult" on duckduckgo Hi Justin, Thank you for heads up, it's just the nudge I need that "occult" probably isn't the right word although I had the astronomical usage in mind. My goto solution is now "occlusive effects" unless something even better comes along.
 KimEe
_______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
In reply to this post by KimEe Yeoh
Interesting. There seem to be quite a few of these. const id (Identity x) (Identity y) = Identity y = liftA2 (const id) (Identity x) (Identity y) If m is occlusive, so is ReaderT e m: liftA2 (const id) (ReaderT f) (ReaderT g) = ReaderT $ \r > liftA2 (const id) (f r) (g r) = ReaderT $ \r > g r = ReaderT g I believe this works for StateT as well. The first counterexample is Writer w for a nontrivial monoid w. On Tue, Nov 10, 2020, 6:23 PM KimEe Yeoh <[hidden email]> wrote:
_______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
On Wed, Nov 11, 2020 at 09:47:43PM 0500, David Feuer wrote:
> If m is occlusive, so is ReaderT e m: > > [...] > > I believe this works for StateT as well. I am puzzled what you mean by that, given that State s a = StateT s Identity a and while "Identity" is "occlusive", State is not. λ> import Control.Monad λ> import Control.Monad.Trans.State.Strict λ> runState (liftM2 (const id) (put True :: State Bool ()) get) False (True,True) λ> runState ((const id) (put True :: State Bool ()) get) False (False,False)  Viktor. _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
Ah, you're right. I wrote that while recovering from a migraine, and it was bogus! On Wed, Nov 11, 2020, 11:57 PM Viktor Dukhovni <[hidden email]> wrote: On Wed, Nov 11, 2020 at 09:47:43PM 0500, David Feuer wrote: _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
In reply to this post by KimEe Yeoh
Dear Kim,
This was not intended as caricature at all. But it seems an excellent example of xy problem indeed. When asking for a real life examples, I provided a case when I can provide example that is familiar to most readers: T = Types i = infer :: object > type c = check :: type > object > Bool Laws just make sure that type checking is preserved over unification or antiunification (<>), except for commutativity  which is omitted on purpose (further description here: https://arxiv.org/abs/2011.03076.) Naturally this example just enumerates the laws that are true for both unification and antiunification problems. Your question would be however fitting for ICFP 2021 trivia, since without examples provided by other haskellcafe readers I would not have guessed that you want to mean "occlusion", instead of magic of "occult" here. On Thu, Nov 12, 2020 at 2:33 AM KimEe Yeoh <[hidden email]> wrote: > > (I'll respond with the original subject heading and with the full thread of Michal's reply copied below so that the convo stays in one place.) > > Hi Michal, I'm afraid you caricaturize my original email out of proportion here: > > > class Monoid m => T m o where > > i :: o > t > > c :: t > o > Bool > <snip> (...) > On Wed, Nov 11, 2020 at 8:36 PM Michal J Gajda <[hidden email]> wrote: (...) >> Such that the following laws are satisfied: >> >> Forall x y z m n. >> c (i x) x =True >> c mempty x = False >> c m y = True => c (m <> n) y = True >> c n y = True => c (m <> n) y = True >> >> What does it tell you about the definitions? >> Can you tell if this set of laws is correctly stated or exhaustive? >> Whether it models what I intend to do? >> Without further examples could I claim that it may be universal model for some phenomena f and g? Cheers Michał _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
In reply to this post by KimEe Yeoh
> First, instead of `const id` I will use `const`, that is, we shall
> prove > > const = liftM2 const :: M a > M b > M a > > which I believe should be equivalent to your property. My belief was wrong, which is evident when using donotation. KimEe stated do {_ < b; x < a; return x} = a while I examined do {x < a; _ < b; return x} = a Since do {x < a; return x} = a holds for any monad, KimEe's property can be reduced to do {_ < b; a} = a or more concisely b >> a = a which I called Kleisliconst in my previous post. As we seemed to have settled for "occlusive" I suggest calling b >> a = a "rightocclusive" or "occlusive from the right" because the right action occludes the sideeffects of the left action, and do {x < a; _ < b; return x} = a should be called "leftocclusive" or "occlusive from the left" because the left action hides the effect of the right action. Under commutativity, both are the same but in general these might be different properties. I do not have a distinguishing counterexample, though, because all monads I come up with are commutative. David Feuer hinted at the possibility to define occlusiveness more generally for Applicative functors. Commutativity might be stated for Applicatives as liftA2 f a b = liftA2 (flip f) b a So far I can only see two classes of occlusive monads: The readerlike (Identity ~ Reader ()) and the setlike monads. Olaf _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
First, for clarity, note that const id = flip const Consider a (right)occlusive functor. We immediately see that liftA2 (flip const) m (pure x) = pure x Using the Applicative laws, we can restate this: x <$ m = pure x We get the same sort of result for a leftocclusive effect. So an occlusive effect can't have any *observable* side effects. It must be "read only". On Thu, Nov 12, 2020, 3:59 PM Olaf Klinke <[hidden email]> wrote: > First, instead of `const id` I will use `const`, that is, we shall _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
On Thu, 20201112 at 16:25 0500, David Feuer wrote:
> First, for clarity, note that > > const id = flip const > > Consider a (right)occlusive functor. We immediately see that > > liftA2 (flip const) m (pure x) = pure x > > Using the Applicative laws, we can restate this: > > x <$ m = pure x > > We get the same sort of result for a leftocclusive effect. > > So an occlusive effect can't have any *observable* side effects. It > must be > "read only". > I'd rather interpret this as a form of lazyness or callbyneed: If the action's return value is not used, then the sideeffects are also not executed. Computationally, constantness of a function is an undecidable property. Therefore it is questionable whether any implementation can exhibit this sort of lazyness with sideeffectful actions. Olaf _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
In reply to this post by Olaf Klinke
Dear Olaf and everyone,
the law do {_ < b; a} = a is equivalent to do {_ < b; return ()} = return (), for, assuming the latter, do {_ < b; a} = do {_ < do {_ < b; return ()}; a} = do {_ < return (); a} = a and it does actually have some history. It was dubbed 'discardability' by Thielecke [1] and explored by Führmann in [2] together with some other important properties of effects, such as 'centrality' and 'commutativity'. Combinations of these properties and examples are explored in the conventional Haskelllike style in [3] (where 'discardability' is called 'sideeffect freeness' though). Cheers, Sergey [1] H. Thielecke, Categorical structure of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997. [2] C. Führmann, Varieties of effects, in: M. Nielsen, U. Engberg (Eds.), Foundations of Software Science and Computation Structures, FOSSACS 2002, in: Lect. Notes Comput. Sci., vol. 2303, Springer, 2002, pp. 144–158. [3] L. Schröder, T. Mossakowski, Monadindependent dynamic logic in HasCasl, J. Logic Comput. 14 (2004) 571–619 _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. smime.p7s (7K) Download Attachment 
In reply to this post by David Feuer
Here is a shorter proof that rightocclusive implies leftocclusive.
b >>= const a = join (fmap (const a) b) monad law (=<<) = (join.).fmap = join (const (return a) b) assumption: leftocclusive = join (return a) = a monad law join.return = id I still don't know whether rightocclusive implies leftocclusive. But I found a noncommutative monad which is not a reader monad and which is leftocclusive: the Set monad from the infinitesearch package [1]. This monad is nontrivial and quite obviously satisfies fmap.const = const.return when you look at the source of the Functor instance. I verified by timing search over a vast and a tiny Set. In accordance with your arguments, I am beginning to think that b >> a = a could be taken as a _definition_ of a sideeffectfree monad. Cheers, Olaf [1] http://hackage.haskell.org/package/infinitesearch On Thu, 20201112 at 16:25 0500, David Feuer wrote: > First, for clarity, note that > > const id = flip const > > Consider a (right)occlusive functor. We immediately see that > > liftA2 (flip const) m (pure x) = pure x > > Using the Applicative laws, we can restate this: > > x <$ m = pure x > > We get the same sort of result for a leftocclusive effect. > > So an occlusive effect can't have any *observable* side effects. It > must be > "read only". > > On Thu, Nov 12, 2020, 3:59 PM Olaf Klinke <[hidden email]> > wrote: > > > > First, instead of `const id` I will use `const`, that is, we > > > shall > > > prove > > > > > > const = liftM2 const :: M a > M b > M a > > > > > > which I believe should be equivalent to your property. > > > > My belief was wrong, which is evident when using donotation. > > KimEe stated > > > > do {_ < b; x < a; return x} = a > > > > while I examined > > > > do {x < a; _ < b; return x} = a > > > > Since do {x < a; return x} = a holds for any monad, KimEe's > > property > > can be reduced to > > > > do {_ < b; a} = a > > or more concisely > > b >> a = a > > > > which I called Kleisliconst in my previous post. As we seemed to > > have > > settled for "occlusive" I suggest calling > > b >> a = a > > "rightocclusive" or "occlusive from the right" because the right > > action occludes the sideeffects of the left action, and > > do {x < a; _ < b; return x} = a > > should be called "leftocclusive" or "occlusive from the left" > > because > > the left action hides the effect of the right action. Under > > commutativity, both are the same but in general these might be > > different properties. I do not have a distinguishing > > counterexample, > > though, because all monads I come up with are commutative. > > > > David Feuer hinted at the possibility to define occlusiveness more > > generally for Applicative functors. Commutativity might be stated > > for > > Applicatives as > > > > liftA2 f a b = liftA2 (flip f) b a > > > > So far I can only see two classes of occlusive monads: The reader > > like > > (Identity ~ Reader ()) and the setlike monads. > > > > Olaf > > > > _______________________________________________ > > HaskellCafe mailing list > > To (un)subscribe, modify options or view archives go to: > > http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe > > Only members subscribed via the mailman list are allowed to post. _______________________________________________ HaskellCafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgibin/mailman/listinfo/haskellcafe Only members subscribed via the mailman list are allowed to post. 
Free forum by Nabble  Edit this page 