On Wed, 2007-03-21 at 14:06 -0700, John Meacham wrote:

On Mon, Mar 19, 2007 at 11:22:47AM +1100, Duncan Coutts wrote:

note, this is most likely not what you want at all:

...

...

{-# RULES "sort/nub" sort . nub = map head . group . sort #-}

desugars to

...

...

{-# RULES "sort/nub" (.) sort nub = map head . group . sort #-}

meaning you are actually adding a RULE to (.), not sort or nub. this hasa couple of unfortunate consequences.

Yes, I know. I just wrote it that way for clarity.

that said, I do not believe this is an appropriate use of rules to begin with, it changes the asymptotic complexity, so should be available as an explicit option, and is just a generally useful routine. not that rules can't also exist, but attached to the right thing.

(sort (nub xs)) = nubSort xs (nub (sort xs)) = nubSort xs

Though as several people pointed out these rules are sadly wrong in the presence of dodgy Eq/Ord instances. :-(

now, I would also like to see (and it might turn out to be more useful),

fastNub, which is a nub that uses Ord and sets to be just as fast, but works on infinite lists. accidentally evaluating a whole list in memory is the quickest way to a space leak and 'sort' is the most common culprit. this is why 'nub' can often be _faster_ than sortNub when you only partially evaluate a list, with ordNub, you get the benefits of both!

Yes. I guess I'm convinced. :-) Duncan

On Tue, 20 Mar 2007, Duncan Coutts wrote:

H98 requires that Eq and Ord be equality classes and total orders

Does it? I was under the impression that a compiler can never assume that any laws hold of any user-defined instances (to do optimisations, for instance). The report states the following: "The Eq class provides equality (==) and inequality (/=) methods." "The Ord class is used for totally ordered datatypes." I interpret this as being mere usage guidelines, and nothing more. What would it mean to state that Ord is a total order, by the way? Should (<=) always return True or False, never ⊥? In that case there is only one implementation of (<=): const (const True).

So one could say that we can't really rely on any laws that should go along with type class instances, but that's clearly not right since then we cannot sort!

Libraries can of course depend on various laws (hopefully this dependence is explicit in the documentation). I guess you can argue whether rewrite rules are part of the compiler or the library. To me a rewrite rule is fishy unless the two sides are observationally equivalent, though.

If we cannot rely on Ord then the current Data.List.sort implementation is wrong because it gives different answers from the H98 spec sort when the Ord instance is not a total order (this is easiest to see with sortBy).

Then I would say it is wrong (according to H98), yes. -- /NAD

On Tue, 2007-03-20 at 14:11 +0100, Nils Anders Danielsson wrote:

On Tue, 20 Mar 2007, Duncan Coutts wrote:

...

H98 requires that Eq and Ord be equality classes and total orders

Does it? I was under the impression that a compiler can never assume that any laws hold of any user-defined instances (to do optimisations, for instance).

The report states the following:

"The Eq class provides equality (==) and inequality (/=) methods." "The Ord class is used for totally ordered datatypes."

I interpret this as being mere usage guidelines, and nothing more.

Aye.

...

If we cannot rely on Ord then the current Data.List.sort implementation is wrong because it gives different answers from the H98 spec sort when the Ord instance is not a total order (this is easiest to see with sortBy).

Then I would say it is wrong (according to H98), yes.

Actually it's fine. The library report states that: When the "By" function replaces an Eq context by a binary predicate, the predicate is assumed to define an equivalence; when the "By" function replaces an Ord context by a binary predicate, the predicate is assumed to define a total ordering. So we can assume they're ok for the specification of those List module functions but as you say, beyond that we can't make any hard assumptions. In other words we can assume Ord is a total order (for non-_|_ values) for the purposes of defining sort but not for rules like: sort . nub = sortDiscardingDuplicates So Lennart is allowed to keep his bogus Eq instances, we have to promise not to break his programs, although the implementation of the sort function doesn't have to sort his values correctly (since presumably it's allowed to use == as well as <= >= etc). So can anyone break this hypothesis? nub . sort = map head . group . sort ie sort first then discard duplicates? Duncan

Duncan Coutts wrote:

So can anyone break this hypothesis?

nub . sort = map head . group . sort

Just make Eq and Ord instances that are completely unrelated, say data Foo = Foo Int Int deriving Show instance Eq Foo where Foo a _ == Foo b _ = a == b instance Ord Foo where Foo _ a `compare` Foo _ b = a `compare` b example = [Foo 0 1, Foo 0 2, Foo 1 1] With these instances nub . sort does something well-defined; sort only uses `compare` and nub only uses (==). Note that Data.List.sort actually provides a stable sort. I don't know if that's specified anywhere, but it's true for both Data.List and for the Haskell report implementation of sort. The rule

nub . sort = map head . group . sort

on the other hand relies on a correspondence between Eq and Ord and breaks: > nub . sort $ example [Foo 0 1,Foo 1 1] > map head . group . sort $ example [Foo 0 1,Foo 1 1,Foo 0 2] More precisely the rule works iff a <= b && b <= c && a == c implies a == b. I'm not sure whether mismatching Eq and Ord [*] instances should be a programmer error, but if so this needs to be stated somewhere. Right now, Data.List has no such restriction. Bertram [*] Ideally, the correspondance should be that (a == b) == (a <= b && b <= a)

On Tue, 20 Mar 2007, Duncan Coutts wrote:

Actually it's fine. The library report states that:

When the "By" function replaces an Eq context by a binary predicate, the predicate is assumed to define an equivalence; when the "By" function replaces an Ord context by a binary predicate, the predicate is assumed to define a total ordering.

So we can assume they're ok for the specification of those List module functions but as you say, beyond that we can't make any hard assumptions.

Well, the report says (about the Prelude, but I think the same applies to the libraries): "It constitutes a specification for the Prelude. Many of the definitions are written with clarity rather than efficiency in mind, and it is not required that the specification be implemented as shown here." I interpret this as "you can change (optimise) the definitions, but the user shouldn't be able to observe the difference (except by measuring resource usage)". What else could "specification" mean?

In other words we can assume Ord is a total order (for non-_|_ values) for the purposes of defining sort [...]

I'd say you still need to define a function observationally equivalent to the one given in the report. -- /NAD

Of course it means that a function must have exactly the same strictness. If it doesn't have the same strictness it's not the same function. I agree the report should be fixed where the functions in the report do not have the appropriate strictness. But this is a change to the report. -- Lennart On Mar 21, 2007, at 22:17 , Duncan Coutts wrote:

On Wed, 2007-03-21 at 16:18 +0100, Nils Anders Danielsson wrote:

...

On Tue, 20 Mar 2007, Duncan Coutts wrote:

...

Well, the report says (about the Prelude, but I think the same applies to the libraries):

"It constitutes a specification for the Prelude. Many of the definitions are written with clarity rather than efficiency in mind, and it is not required that the specification be implemented as shown here."

I interpret this as "you can change (optimise) the definitions, but the user shouldn't be able to observe the difference (except by measuring resource usage)". What else could "specification" mean?

In particular does that mean that an implementation must have *exactly* the same strictness as given in the report? It never says explicitly. Probably it should mean that, but in that case there are a handful of cases where the report needs to be fixed. There are a couple cases where the report is stricter than is necessary and conversely a couple cases where it is lazier than was probably really indented.

I will set out the detail on this to the libraries and haskell' list soonish.

...

I'd say you still need to define a function observationally equivalent to the one given in the report.

Then we would really have to use insertion sort, not quicksort, or mergesort or heapsort. I don't think that's what the spec intends.

It does after all say for the various *By functions that we can assume the passed function is an equivalence or a total order:

When the "By" function replaces an Eq context by a binary predicate, the predicate is assumed to define an equivalence; when the "By" function replaces an Ord context by a binary predicate, the predicate is assumed to define a total ordering.

It also defines sort = sortBy compare and nub = nubBy (==) so we can also assume that Eq is an equivalence and Ord instance is a total order for the purposes of defining sort, nub etc. But only for those library functions, not in general.

Duncan

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Well, I think people use the functions that come with an implementation as the de facto spec. So we should update the spec to reflect reality. (BTW, I wouldn't be surprised if I'm to blame for some of the discrepancies, even though I tried to be careful when I implemented more efficient versions for the Prelude functions for hbc.) -- Lennart On Mar 22, 2007, at 00:58 , Duncan Coutts wrote:

On Wed, 2007-03-21 at 23:41 +0000, Lennart Augustsson wrote:

...

Of course it means that a function must have exactly the same strictness. If it doesn't have the same strictness it's not the same function.

Of course.

...

I agree the report should be fixed where the functions in the report do not have the appropriate strictness. But this is a change to the report.

It's interesting to note that the implementations in base for some functions in Data.List have been inconsistent with the report for years and nobody has noticed (or at least if they noticed they didn't complain very loudly).

For example the standard implementations of partition and splitAt have been inconsistent with the H98 spec forever. I say forever since the implementations were consistent with the Haskell 1.2, 1.3 and 1.4 specifications but the Haskell98 report changed the specification and the implementations were never updated.

Similarly, GHC has had an incorrect implementation of genericTake for some years and no-one has noticed. The current implementation is inconsistent with Haskell98 and looking back, GHC 3.02 was inconsistent with Haskell 1.4 which as far as I can tell was the first version of the spec to define genericTake.

Duncan

On Thu, 2007-03-22 at 12:10 +0100, Nils Anders Danielsson wrote:

On Thu, 22 Mar 2007, Duncan Coutts wrote:

...

It's interesting to note that the implementations in base for some functions in Data.List have been inconsistent with the report for years and nobody has noticed (or at least if they noticed they didn't complain very loudly).

I have certainly found some discrepancies in the past. If you never reason about partial or infinite values you're not likely to stumble over these inconsistencies, though.

Certainly. I've come across some some very subtle examples that I'd not have spotted normally. I came across your ChasingBottoms lib yesterday. It's very nice. I'd started to implement something similar to test the strictness properties of our list reimplementation but what you've got is a good deal more complete. I started by looking at Olaf Chitil's StrictCheck module which uses your lib however the SYB technique it uses to generate partial values of various types doesn't help when it comes to function types. So instead I modified SmallCheck to generate values with bottoms in them. That copes with function types very nicely. It can generate all the partial monotone functions up to a given depth ( I think :-) ). My one gripe with ChasingBottoms is that I can't customise the ApproxShow instances. I want to show functions in the SmallCheck style but deal with _|_'s properly. SmallCheck defines a Show instance for functions that shows the mappings up to a certain depth. It's very cute. I can't define my own ApproxShow instance for functions since it overlaps with the Data a => ApproxShow a instance. Duncan

I have certainly used Eq and Ord similar to the ones in my example. I know under what circumstances I can call what library functions, but the compiler doesn't. It should not make any unprovable assumptions about my code; I'd be very perturbed if it did. -- Lennart On Mar 19, 2007, at 23:05 , Duncan Coutts wrote:

On Mon, 2007-03-19 at 19:43 +0000, Lennart Augustsson wrote:

...

As I pointed out in the GHC trac report, this rule is wrong. E.g.,

data T = T Int Int deriving (Ord, Show) instance Eq T where T x _ == T y _ = x == y

ts = [T 1 1, T 1 undefined]

So the problem in that example is that if we nub first then we get [T 1 1] and sorting that is presumably fine, however if we sort we compare both fields.

My grumble here is that your Eq and Ord instances are not in agreement with each other. If you can claim that they're equal by only comparing the first components then surely you must for Ord too.

Isn't some law being violated here: T 1 0 < T 1 1 and yet T 1 0 == T 1 1

but shouldn't a < b imply that a != b

H98 requires that Eq and Ord be equality classes and total orders, does it say nothing about any relationship between the two, that they be in any way consistent?

So one could say that we can't really rely on any laws that should go along with type class instances, but that's clearly not right since then we cannot sort!

If we cannot rely on Ord then the current Data.List.sort implementation is wrong because it gives different answers from the H98 spec sort when the Ord instance is not a total order (this is easiest to see with sortBy).

Duncan