Early feedback: left-biasing `max`

Core Libraries Committee
#81

Yes, exactly.

Such as (==), in the current iteration of the min/max laws? With you so far, I think, although I’m not aware of other classes making this sort of allowance. When the Semigroup law says that (<>) should be associative, that’s not up to some particular observation function, is it? I default to interpreting such laws as holding up to any pure, safe predicate—when the documentation says x <> (y <> z) = (x <> y) <> z, I read that as meaning that for any safe function f :: a -> Bool, f (x <> (y <> z)) == f ((x <> y) <> z) (where now == can be simple boolean equality). That’s the same standard I’d like to use with min and max.

Is there a practical difference between arguing for weaker laws (such as laws up to some observation function) and arguing for fewer laws? They seem like the same thing to me—a stronger law subsumes a weaker law by adding an additional restriction, which could be seen as a second law in its own right.

What strikes me as more important than the difference between weaker and fewer is the spectrum with strong laws and fewer instances on one end and few/no/weak laws and many instances on the other end.

Bodigrim says that:

That’s the argument for pushing toward the many-instances side of the spectrum—that it’d be useful. That’s what I see as the general argument against laws—more instances are always useful!

He then gives some specific examples of cases that he thinks are particularly useful for min and max. I draw a parallel case to one of those examples with Semigroup, and point out that this would be useful in the same scenario that his example would be useful—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. Because ‘useful’ is not the deciding factor in determining what laws a class should have. Rather, what is most important is the intended meaning of the class abstraction. <> could represent some arbitrary binary operation—but we intend that the meaning of the Semigroup class is to represent, well, a semigroup. And to do that, <> must be associative.

Likewise, if min and max are to represent the abstract concepts of ‘take the lesser/greater of these two arguments’, it would be incorrect for them to (observably—under the hood I don’t care what they do) construct a third value. It might be ‘useful’, but it’s incorrect, and that’s that! If we let usefulness override our sense of what class operations are meant to represent, we would not have laws, because laws only get in the way of having more instances and being more useful.

#82

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. It allows you to distinguish m from m >>= return, violating right identity. 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.

#83

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.

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.

#84

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

Yes, I think that’s right.

#85

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.

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

1 Like
#86

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

#87

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)

#88

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 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. 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!)

1 Like
#89

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.

#90

(As it does.)

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

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.

#91

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

1 Like
#92

‘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?

#93

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

#94

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.

#95

Sure,

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)

$ ghc SplitRoot.hs && ./SplitRoot
[fromList [0,1],fromList [2],fromList [3]]
[fromList [0],fromList [1],fromList [2,3]]
2 Likes
#96

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

#97

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.

1 Like
#98

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?

#99

Looking at the documentation of class 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.

2 Likes
#100

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.

1 Like