# Early feedback: left-biasing \`max\`

**URL:** <https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392>\
**Category:** Core Libraries Committee\
**Created:** [August 23, 2023, 12:25am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392 "2023-08-23T00:25:53Z")\
**Posts on this page:** 19\
**Page:** 4

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 4, 2023, 9:28am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/82 "2023-09-04T09:28:05Z")

</div>

> [@rhendric](#):
>
> Is there a practical difference between arguing for weaker laws (i.e., laws up to some observation function) and arguing for fewer laws?

No, but you didn’t say “My issue with all three of these points is that they’re general arguments in favour of weaker laws” you said “against ever having laws”! That’s a very strong statement. I don’t see how you concluded that. That is my only point of contention.

> by Bodigrim’s reasoning, I would expect him to object to a strict interpretation of `Semigroup`’s laws in that scenario as well. But I doubt that he does

I suspect he does! An example that was widely discussed in the Haskell community around ten years ago, as early effect systems were being thrashed out, was Apfelmus’s [operational free monad](https://hackage.haskell.org/package/operational-0.2.4.2/docs/Control-Monad-Operational.html#t:ProgramViewT). It allows you to distinguish `m` from `m >>= return`, violating [right identity](https://www.stackage.org/haddock/lts-21.9/base-4.17.2.0/Prelude.html#t:Monad). In this debate there were two camps: 1) this is bad because it violates the law, and 2) this is fine because the laws still hold up to reasonable observation functions.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 9:46am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/83 "2023-09-04T09:46:28Z")

</div>

> [@tomjaguarpaw](#):
>
> No, but you didn’t say “My issue with all three of these points is that they’re general arguments in favour of weaker laws” you said “against ever having laws”! That’s a very strong statement. I don’t see how you concluded that. That is my only point of contention.

All I’m trying to convey with that hyperbolic-sounding claim is that no matter where you currently are on the having-laws spectrum, someone can always point out that it’d be more useful to have fewer laws. By induction, this is an argument for no laws. I don’t expect anyone to actually follow that inductive argument to its absurd conclusion; I’m just saying that without some counterbalancing force, that argument alone takes you to no-law-town.

> [@tomjaguarpaw](#):
>
> I suspect he does! An example that was widely discussed in the Haskell community around ten years ago, as early effect systems were being thrashed out, was Apfelmus’s [operational free monad](https://hackage.haskell.org/package/operational-0.2.4.2/docs/Control-Monad-Operational.html#t:ProgramViewT). It allows you to distinguish `m` from `m >>= return`, violating [right identity](https://www.stackage.org/haddock/lts-21.9/base-4.17.2.0/Prelude.html#t:Monad). In this debate there were two camps: 1) this is bad because it violates the law, and 2) this is fine because the laws still hold up to reasonable observation functions.

That’s an interesting bit of history!

Where’s the camp that this is fine if and only if:

- the constructors of `ProgramViewT` are hidden in an internal module
- any functions that can distinguish between the two sides of the right identity law are also hidden in an internal module, or otherwise labeled as unsafe or improper

Is that what camp 2 meant by reasonable observation functions?

Anyway, I note that despite this, the right identity law is still listed among the laws for `Monad`, without any specification of the observation functions for which it holds. So perhaps the community consensus is that it’s okay for laws to be strong, and for debatably-non-abiding instances to exist anyway if they’re useful enough—which would support my position.

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 4, 2023, 10:01am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/84 "2023-09-04T10:01:29Z")

</div>

> someone can always point out that it’d be more useful to have fewer laws. By induction, this is an argument for no laws

Sorry, I still don’t think I understand this line of reasoning, but that’s OK. I don’t need to understand it. Hopefully I’ve stated my position clearly enough.

> Is that what camp 2 meant by reasonable observation functions?

I don’t think that either the camps or the terms of the debate were well enough defined to give a precise answer to that question

> [@rhendric](#):
>
> So perhaps the community consensus is that it’s okay for laws to be strong, and for debatably-non-abiding instances to exist anyway if they’re useful enough—which would support my position.

Yes, I think that’s right.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [September 4, 2023, 10:11am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/85 "2023-09-04T10:11:09Z")

</div>

> [@tomjaguarpaw](#):
>
> laws holding up to fairly fine-grained observation functions.

Not just one or a few observation functions, the usual convention is that the laws should hold up to observability through the public interface of the types involved. There should not be any safe public function exposed from the library that is able to tell that the laws do not hold.

That’s also why I would say `Arg` should be renamed to `UnsafeArg` as it breaks the `Eq` extensionality property. I think the only reason it is not explicitly named that currently is because `Eq` technically has no laws.

> [@rhendric](#):
>
> When the `Semigroup` law says that `(<>)` should be associative, that’s not up to some particular observation function, is it?

It is. A good example is are the Applicative and Monad classes and the Haxl monad, which does not satisfy the law `p <*> q = p >>= \f -> q >>= \x -> pure (f x)` literally, but it does satisfy that law up to observability through its public interface (although in the presence of I/O you can’t really reason about observational equivalence).

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 4, 2023, 10:20am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/86 "2023-09-04T10:20:03Z")

</div>

> [@jaror](#):
>
> the usual convention is that the laws should hold up to observability through the public interface of the types involved

Sure, that is a very well-behaved convention, but that’s not the only convention as the example of `operational` shows.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [September 4, 2023, 10:26am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/87 "2023-09-04T10:26:02Z")

</div>

I don’t see an obvious way that ProgramViewT violates right identity, can you show how that’s done? (In fact, it seems like it is essentially a free(r) monad to me)

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [September 4, 2023, 10:57am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/88 "2023-09-04T10:57:14Z")

</div>

Ah, I misremembered. It wasn’t `operational` that exposed operations that allowed you to obtain the “bind” structure of the program. Perhaps there were some other attempts at libraries that exposed the constructors of the type, or maybe it was a more philosophical argument that “morally” `operational` violated the monad laws even though “observationally” it didn’t. I wrote an article about an attempt at a [free applicative](http://web.jaguarpaw.co.uk/~tom/blog/posts/2012-09-09-towards-free-applicatives.html) that mentions the matter.

Anyway, I had an insight that maybe explains my confusion. Perhaps @rhendric thinks that some people are saying ‘the documentation for `Ord` should state “these laws hold only up to some observation function”’ or “we shouldn’t be stricter in the documentation about what `min` and `max` can return”. If they are saying that then I object too! (This thread has gone on so long it’s hard to check whether someone said that.) My position is that we should state that the laws hold “on the nose” yet accept conventionally that they will be violated in ways that work out reasonably in practice.

EDIT: Ah, maybe that is indeed what Bodigrim is saying in [Early feedback: left-biasing `max` - #76 by Bodigrim](http://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/76). I didn’t interpret it like that, and I don’t think that’s what Bodigrim meant, but I can understand how one could interpret it like that. (FWIW I thought Bodigrim meant “it’s fine to make the documentation more strict but we should also recognise that sometimes we’re going to violate those laws for practical reasons”. I may well be wrong!)

---

<div class="post-metadata">

**Author:** ![bmacho](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bmacho/32/3448_2.png) [@bmacho](https://discourse.haskell.org/u/bmacho)\
**Post date:** [September 4, 2023, 11:28am UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/89 "2023-09-04T11:28:53Z")

</div>

I love this examples! I fail to see however, why should this reasoning only apply to Ord, and not, say, Semigroup. It would be similarly useful if all the Semigroup laws were only defined up to an Eq.

Also I think that the current Base documentation, and Arg, and everything that builds on it is against the Haskell report. Also I think that this change is for the worse, and probably you should consider to change back: the only allowed min and max functions should be semantically equivalent to the min/max functions in the Haskell report.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 4:59pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/90 "2023-09-04T16:59:56Z")

</div>

> [@tomjaguarpaw](#):
>
> Perhaps @rhendric thinks that some people are saying ‘the documentation for `Ord` should state “these laws hold only up to some observation function”’

(As it does.)

> [@tomjaguarpaw](#):
>
> or “we shouldn’t be stricter in the documentation about what `min` and `max` can return”.

Yes, that’s what I thought Bodigrim’s position was.

> [@tomjaguarpaw](#):
>
> My position is that we should state that the laws hold “on the nose” yet accept conventionally that they will be violated in ways that work out reasonably in practice.

Basically agree, though I think all of Bodigrim’s numbered examples are cases to which I would not be comfortable turning a blind eye, personally. (The unnumbered `ByteString` example is totally fine.) But as a practical matter, non-abiding instances generally exist and there’s little that stricter folks like myself can do about it except disclaim that things you might expect to be true generally (like `maximum = maximumBy compare`) may not hold in the presence of such instances.

---

<div class="post-metadata">

**Author:** ![Bodigrim](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bodigrim/32/1457_2.png) [@Bodigrim](https://discourse.haskell.org/u/Bodigrim)\
**Post date:** [September 4, 2023, 9:24pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/91 "2023-09-04T21:24:13Z")

</div>

> [@bmacho](#):
>
> I love this examples! I fail to see however, why should this reasoning only apply to Ord, and not, say, Semigroup. It would be similarly useful if all the Semigroup laws were only defined up to an Eq.

`Semigroup` laws _are_ defined up to `Eq`, otherwise there would be neither `instance Monoid ByteString` nor `instance Ord a => Semigroup (Set a)`.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 9:30pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/92 "2023-09-04T21:30:45Z")

</div>

> [@Bodigrim](#):
>
> `Semigroup` laws _are_ defined up to `Eq`, otherwise there would be neither `instance Monoid ByteString` nor `instance Ord a => Semigroup (Set a)`.

‘Otherwise’ as in if the laws were defined up to observability, you mean?

In which case, you should be able to provide a function `f :: ByteString -> Bool` that doesn’t use internal or unsafe functions, such that `f lhs /= f rhs` where `lhs = rhs` is a `Monoid` law; resp. a function `g :: Ord a => Set a -> Bool` for a `Semigroup` law.

I don’t believe such functions exist, so prove me wrong please?

---

<div class="post-metadata">

**Author:** ![atravers](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@atravers](https://discourse.haskell.org/u/atravers)\
**Post date:** [September 4, 2023, 9:53pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/93 "2023-09-04T21:53:46Z")

</div>

…presumably because your ongoing attempts to find such functions haven’t been successful:

> [@](#):
>
> ### Search, and research
> 
> Before posting a question [or insist that someone _“should”_ provide something], we strongly recommend that you spend a reasonable amount of time researching the problem and searching for existing questions on this site that may provide an answer.
> 
> [How do I ask a good question? - Help Center - Stack Overflow](https://stackoverflow.com/help/how-to-ask)

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 10:25pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/94 "2023-09-04T22:25:27Z")

</div>

So what, you’re implying that my request for a counterexample is invalid because I haven’t proved that no such counterexample can exist?

Bodigrim seems pretty confident that the laws can’t hold for `ByteString` or `Set a` unless they are weakened down from observably-equal to equal-under-`Eq`. If he knows that observably-equal doesn’t work, he should be able to explain why, no?

Whereas I assume by default that the laws hold up to observability unless otherwise documented, and yeah, I didn’t succeed in finding a counterexample so I’m going to keep on assuming that, but corrections are welcome.

---

<div class="post-metadata">

**Author:** ![Bodigrim](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bodigrim/32/1457_2.png) [@Bodigrim](https://discourse.haskell.org/u/Bodigrim)\
**Post date:** [September 4, 2023, 10:27pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/95 "2023-09-04T22:27:16Z")

</div>

Sure,

```haskell
import Data.Set (Set)
import qualified Data.Set as S

main :: IO ()
main = do
  let x = S.fromList [1]
      y = S.fromList [0]
      z = S.fromList [2,3]
  print $ S.splitRoot (x <> (y <> z))
  print $ S.splitRoot ((x <> y) <> z)

```

```haskell
$ ghc SplitRoot.hs && ./SplitRoot
[fromList [0,1],fromList [2],fromList [3]]
[fromList [0],fromList [1],fromList [2,3]]

```

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 10:29pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/96 "2023-09-04T22:29:36Z")

</div>

Thanks, that’s that question sorted! Adjusting my assumptions accordingly.

---

<div class="post-metadata">

**Author:** ![Bodigrim](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bodigrim/32/1457_2.png) [@Bodigrim](https://discourse.haskell.org/u/Bodigrim)\
**Post date:** [September 4, 2023, 10:51pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/97 "2023-09-04T22:51:09Z")

</div>

I understand the appeal of structural interpretation of equality in class laws, because it allows you to deduce much more consequences. The problem is however that it’s next to impossible to prove that the law holds to start with.

You see, “concatenation is associative wrt semantical equality (= with respect to instance `Eq`)” is _actionable_, it talks about a closed set of definitions, and one (who is cleverer than me) can sit down and prove it. But “concatenation is associative wrt structural equality unless one uses something internal or unsafe” talks about undefined and unlimited set of objects, it’s not even a proper statement. How do you define internal and unsafe? Is `splitRoot` internal? Are `Data` / `Generic` / `Lift` unsafe? What about `dataToTag#`? `HasCallStack`? If we dare to speak about “laws” we should be able to provide precise definitions.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [September 4, 2023, 11:10pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/98 "2023-09-04T23:10:26Z")

</div>

So are you therefore opposed to including a guarantee that `(min a b, max a b)` equals `(a, b)` or `(b, a)` in a more-than-just-`Eq`-equality way in the `Ord` documentation, even though some people seem to care about this and it’s currently ambiguous whether an instance is expected to respect it?

---

<div class="post-metadata">

**Author:** ![Bodigrim](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bodigrim/32/1457_2.png) [@Bodigrim](https://discourse.haskell.org/u/Bodigrim)\
**Post date:** [September 4, 2023, 11:53pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/99 "2023-09-04T23:53:48Z")

</div>

> [@rhendric](#):
>
> even though … it’s currently ambiguous whether an instance is expected to respect it?

Looking at the documentation of [`class Ord`](https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-Ord.html#t:Ord), it seems unambiguous that there is no such expectation at the moment.

I’m generally opposed to requiring more-than-just-`Eq`-equality in class laws without prescribing its extent precisely.

As for `(min a b, max a b)` equal to sorted `(a, b)` in particular, I don’t know a convincing reason to care much about this identity.

---

<div class="post-metadata">

**Author:** ![carter](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/carter/32/186_2.png) [@carter](https://discourse.haskell.org/u/carter)\
**Post date:** [September 21, 2023, 9:16pm UTC](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392/100 "2023-09-21T21:16:20Z")

</div>

in some ways, its kinda like how as one learns about unix/linux, you initially think theres useful distinctions between /bin/ ,/usr/bin , and /usr/local/bin and their associated prefixes, and then you learn its because on the original prototype machine they had to upgrade the drive space 3 times! (i could be misremembering the history).

my point being, sometimes complexity is anthropogenic rather than coming from some logical or mathematical ideal.

[Previous page](https://discourse.haskell.org/t/early-feedback-left-biasing-max/7392.md?page=3)