What to call Occult Effects

older
Re: [Haskell-cafe] What to call...

Kim-Ee Yeoh

10 Nov 2020 10 Nov '20

6:23 p.m.

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? -- -- Kim-Ee

Attachments:

attachment.html (text/html — 579 bytes)

Show replies by date

Kim-Ee Yeoh

11 Nov 11 Nov

8:33 p.m.

(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 one-letter 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

...

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

Most of mathematics we do is not entirely disconnected from applications.

If I tell you there is a class of monoids `m` over a set of objects `o` :

class Monoid m => T m o where i :: o -> t c :: t -> o -> Bool

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?

Or would you rather see some examples or descriptions of i and c operations?

PS you may respond to haskell-cafe, sure. I did not think that my previous question deserved sharing, but this answer certainly does. -- Cheers Michał

On Wed, Nov 11, 2020, 14:04 Kim-Ee Yeoh wrote:

...
Hi Michal,

How is it hermetic? I think I fully described the property whose name I am opening to discussion.

What is lacking in the definition?

Also, do you mind having this discussion at the cafe itself? You are probably not the only one with this query.

On Wed, Nov 11, 2020 at 7:37 PM Michał J Gajda wrote:

...
Hi, Your post to haskell-cafe is somewhat hermetic if you do not provide additional examples. What do you use these for? -- Cheers Michał

-- -- Kim-Ee

-- -- Kim-Ee

Michael Matsko

8:38 p.m.

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: Haskell-Cafe on behalf of Kim-Ee Yeoh Sent: Wednesday, November 11, 2020 8:33:34 PM To: Haskell Cafe ; mgajda@mimuw.edu.pl Subject: Re: [Haskell-cafe] 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>

...

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 X-Y problem? http://xyproblem.info/ I assure you I labor under no such tunnel-vision. Were I to request a cromulent adjective for the seventh powers of the natural numbers, what progress do you make by making counter-demands for examples? Behind which string of digits does the pellucid word hide itself? -- Kim-Ee On Wed, Nov 11, 2020 at 8:36 PM Michal J Gajda mailto:mgajda@mimuw.edu.pl> 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 Most of mathematics we do is not entirely disconnected from applications. If I tell you there is a class of monoids `m` over a set of objects `o` : class Monoid m => T m o where i :: o -> t c :: t -> o -> Bool 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? Or would you rather see some examples or descriptions of i and c operations? PS you may respond to haskell-cafe, sure. I did not think that my previous question deserved sharing, but this answer certainly does. -- Cheers Michał On Wed, Nov 11, 2020, 14:04 Kim-Ee Yeoh mailto:ky3@atamo.com> wrote: Hi Michal, How is it hermetic? I think I fully described the property whose name I am opening to discussion. What is lacking in the definition? Also, do you mind having this discussion at the cafe itself? You are probably not the only one with this query. On Wed, Nov 11, 2020 at 7:37 PM Michał J Gajda mailto:mjgajda@gmail.com> wrote: Hi, Your post to haskell-cafe is somewhat hermetic if you do not provide additional examples. What do you use these for? -- Cheers Michał -- -- Kim-Ee -- -- Kim-Ee

Michal J Gajda

12 Nov 12 Nov

8:30 a.m.

Dear Kim, This was not intended as caricature at all. But it seems an excellent example of x-y 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 anti-unification (<>), 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 anti-unification problems. Your question would be however fitting for ICFP 2021 trivia, since without examples provided by other haskell-cafe 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 Kim-Ee Yeoh 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 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ł

David Feuer

11 Nov 11 Nov

9:47 p.m.

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 non-trivial monoid w. On Tue, Nov 10, 2020, 6:23 PM Kim-Ee Yeoh wrote:

...

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? -- -- Kim-Ee _______________________________________________ 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.

Viktor Dukhovni

11:57 p.m.

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.

David Feuer

11:59 p.m.

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 wrote:

...

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. _______________________________________________ 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.

1650

Age (days ago)

1652

Last active (days ago)

List overview

Download

6 comments

5 participants

participants (5)

David Feuer
Kim-Ee Yeoh
Michael Matsko
Michal J Gajda
Viktor Dukhovni