Hi folks I'm late into this thread, so apologies if I'm being dim. On 13 Mar 2008, at 16:17, kahl@cas.mcmaster.ca wrote:

Adrian Hey wrote:

...

I would ask for any correct Eq instance something like the law: (x==y) = True implies x=y (and vice-versa)

I wish I knew what = meant here. Did somebody say? I don't think it's totally obvious what equational propositions should mean. Nor do I think it's desirable to consider only those propositions expressible in QuickCheck. If = is reflexive and distinguishes undefined from True, then x = y implies (x == y) = True will be tricky to satisfy for quite a lot of types. What about undefined == undefined or repeat 'x' == repeat 'x' ? For some suitable (slightly subtle) definition of "finite", you might manage x finite and x = y implies (x == y) = True One rather intensional definition of x = y might be "x and y have a common n-step reduct" with respect to some suitable operational semantics. I don't think this is what Adrian had in mind, but it certainly falls foul of Wolfram's objection.

The easiest counterexample are sets (or finite maps) provided as an abstract data type (i.e., exported without access to the implementation, in particular constructors).

Different kinds of balanced trees typically do not produce the same representation for the same set constructed by different construction expressions.

This suggests that we should seek to define x = y on a type by type basis, to mean "x and y support the same observations", for some suitable notion of observation, which might depend crucially on what operations are exported from the (notional or actual) module which defines the type. If so, it's clearly crucial to allow some observations which rely on waiting for ever, in order to avoid _|_-induced collapse. Something of the sort should allow this...

Therefore, (==) on sets will be expected to produce equality of sets, which will only be an equivalence on set representations.

...but this...

...

which implies (f x == f y) = True (for expression types which are instances of Eq).

This specifies that (==) is a congurence for f, and is in my opinion the right specification: (==) should be a congurence on all datatypes with respect to all purely defineable functions.

...is more troublesome. Take f = repeat. Define f = f. I'd hope x == y = True would give us x = y, and that x == y would be defined if at least one of x and y is finite. That implies f x = f y, which should guarantee that f x == f y is not False.

But at least nowadays people occasionally do export functions that allow access to representation details,

[..]

I consider this as an argument to remove showTree from the interface of Data.Set, and to either specify toList to produce an ordered list (replacing toAscList), or to remove it from the interface as well.

Perhaps that's a little extreme but I agree with the sentiment. How about designating such abstraction- breaking functions "nosy", in the same way that functions which might break purity are "unsafe".

(mapMonotonic should of course be removed, too, or specified to fail (preferably in some MonadZero) if the precondition is violated, which should still be implementable in linear time.)

What's wrong with mapMonotonic that isn't wrong with, say, sortBy?, or Eq instances for parametrized types?

...

but if so would like to appeal to movers and shakers in the language definition to please decide exactly what the proper interpretation of standard Eq and Ord "class laws" are and in the next version of the report give an explanation of these

Strongly seconded, inserting ``precise'' before ``explanation'' ;-)

(And I'd expect equivalences and congruences to be accessible on the basis of standard first-year math...)

Before we can talk about what == should return, can we settle what we mean by = ? I think we need to pragmatic about breaking the rules, given suitable documentation and maybe warnings. We should at least aspire to some principles, which means we should try to know what we're talking about and to know what we're doing, even if we don't always do what we're talking about. I'll shut up now. Potatoes to peel Conor

Hi On 13 Mar 2008, at 23:42, kahl@cas.mcmaster.ca wrote:

Conor McBride responded to my comment:

...

...

(mapMonotonic should of course be removed, too, or specified to fail (preferably in some MonadZero) if the precondition is violated, which should still be implementable in linear time.)

What's wrong with mapMonotonic that isn't wrong with, say, sortBy?, or Eq instances for parametrized types?

Prelude> :m + Data.Set Prelude Data.Set> toAscList $ mapMonotonic (10 -) (fromList [1 .. 5]) [9,8,7,6,5] Prelude Data.Set> 5 `member` mapMonotonic (10 -) (fromList [1 .. 5]) False

Something's certainly wrong there!

But nothing out of the ordinary: garbage in, garbage out. Happens all the time, even in Haskell. Why pick on mapMonotonic? Prelude Data.List> sortBy (\_ _ -> GT) [1,3,2,5,4] [4,5,2,3,1] Prelude Data.List> sortBy (\_ _ -> GT) [4,5,3,2,1] [1,2,3,5,4] I guess there's a question of what we might call "toxic waste"---junk values other than undefined. I think undefined is bad enough already. So the type system can't express the spec. I don't think we should be casual about that: we should be precise in documentation about the obligations which fall on the programmer. Some dirt is pragmatically necessary: we shouldn't pretend that it ain't so; we shouldn't pretend that dirt is clean.

...

Before we can talk about what == should return, can we settle what we mean by = ?

``='' is not in the Haskell interface! ;-)

No, but "is" is in the human interface!

Therefore, I talked only about (==).

Ah, but you talked about things. Which things? Is one of the things you talked about the same as (==)? the same as (flip (==))?

The best way to include ``='' seems to be the semantic equality of P-logic [Harrison-Kieburtz-2005], which is quite a heavy calibre, and at least in that paper, classes are not yet included.

I expect it's hard work. It's hard work in much better behaved systems. My point is that it's worth it, in order to facilitate more meaningful discussions. All the best Conor

Hi On 14 Mar 2008, at 03:48, Roman Leshchinskiy wrote:

Adrian Hey wrote:

...

I would ask for any correct Eq instance something like the law: (x==y) = True implies x=y (and vice-versa) which implies f x = f y for all definable f which implies (f x == f y) = True (for expression types which are instances of Eq). This pretty much requires structural equality for concrete types. For abstract types you can do something different provided functions which can give different answers for two "equal" arguments are not exposed.

How do you propose something like this to be specified in the language definition? The report doesn't (and shouldn't) know about abstract types.

Why not? Why shouldn't there be at least a standard convention, if not an abstype-like feature for establishing an abstraction barrier, and hence determine the appropriate observational equality for an abstract type?

So you can either require your law to hold everywhere, which IMO isn't a good idea, or you don't require it to hold. From the language definition point of view, I don't see any middle ground here.

Why not demand it in the definition, but allow "unsafe" leaks in practice? As usual. Why are you so determined that there's nothing principled to do here? People like to say "Haskell's easy to reason about". How much of a lie would you like that not to be?

Also, when you talk about definable functions, do you include things like I/O? What if I want to store things (such as a Set) on a disk? If the same abstract value can have multiple representations, do I have to convert them all to some canonical representation before writing them to a file?

Canonical representations are not necessary for observational congruence. Representation hiding is enough.

This might be rather slow and is, IMO, quite unnecessary.

From a more philosophical points of view, I'd say that the appropriate concept of equality depends a lot on the problem domain.

It's certainly true that different predicates may respect different equivalence relations. The equivalence relation you call equality should be the finest of those, with finer representational distinctions abstracted away. What that buys you is a class of predicates which are guaranteed to respect equality without further ado...

Personally, I quite strongly disagree with restricting Eq instances in the way you propose. I have never found much use for strict structural equality (as opposed to domain-specific equality which may or may not coincide with the structural one).

...which is how we use equality when we think. I certainly don't think "strict structural equality" should be compulsory. In fact, for Haskell's lazy data structures, you rather need lazy structural simulation if you want to explain why cycle "x" = cycle "xx" What would be so wrong with establishing a convention for saying, at each given type (1) this is the propositional equivalence which we expect functions on this type to respect (2) here is an interface which respects that equivalence (3) here are some unsafe functions which break that equivalence: use them at your own risk ? Why is it pragmatically necessary to make reasoning difficult? I'm sure that wise folk out there have wise answers to that question which they don't consider to be an embarrassment. When representation-hiding is bliss, 'tis folly to be wise. All the best Conor