RE: precedence bug with derived instances
Some last-ditch H98 stuff. I have the proofs now and have to send them back this week. Changes will become impossible (or at least much harder) after that. Ah well, I'm sure more errors will come to light. Simon | > | (3) Section D.4 gives the expected rule: | > | | > | head (readsPrec d (showsPrec d x "")) == (x,"") | > | | > | Why should this not be: | > | | > | readsPrec d (showsPrec d x "") == [(x,"")] | > | > I can't think why not, unless there is a shorter valid parse, which I | > suppose is conceivable. I'd rather not change this. | | In fact, neither rule above is true for the example given in section D.5. | To see this, run the following program: | | infix 5 :^: | data Tree a = Leaf a | Tree a :^: Tree a deriving (Eq, Ord, Read, Show) | main = mapM_ trial [0..10] | where trial d = print (readsPrec d (showsPrec d x "") :: [(Tree Int, | String)]) | x = Leaf 1 :^: Leaf 2 Uh huh. For readsPrec 0 "Leaf 1 :^: Leaf 2" we get [(Leaf 1, " :^ Leaf 2"), (Leaf1 :^: Leaf 2, "")] That is, there are two parses, and the shortest parse comes first. Same is true for Hugs. Not unreasonable, actually, and nothing in the specification seems to preclude this. I can only make minimal changes now. I suspect the smallest change is to require that (x,"") `elem` readsPrec d (showsPrec d x "") This weakens the existing equation by not requiring (x,"") to be the first parse returned. Dean writes: | Perhaps we want: | | readsPrec should be able to parse the string produced by showsPrec, and | should deliver the value that showsPrec started with. That is, the list | result of | | readsPrec d (showsPrec d x "") | | should contain exactly one pair whose second element is "", and the first | element of that pair should be equivalent to x. I don't understand this. What does "equivalent" mean? And how does this differ from the (incorrect) claim that readsPrec d (showsPrec d x "") == [(x,"")] Simon
Simon Peyton-Jones wrote:
I can only make minimal changes now. I suspect the smallest change is to require that (x,"") `elem` readsPrec d (showsPrec d x "")
This weakens the existing equation by not requiring (x,"") to be the first parse returned.
Dean writes: | Perhaps we want: | | readsPrec should be able to parse the string produced by showsPrec, and | should deliver the value that showsPrec started with. That is, the list | result of | | readsPrec d (showsPrec d x "") | | should contain exactly one pair whose second element is "", and the first | element of that pair should be equivalent to x.
I don't understand this. What does "equivalent" mean? And how does this differ from the (incorrect) claim that
readsPrec d (showsPrec d x "") == [(x,"")]
That >> whose second element is "" << obviously means to apply filter (("" ==) . snd) to the list. Using list comprehension, that gives [ r | (r,"") <- readsPrec d (showsPrec d x "") ] == [x] This is nearly what you suggested, with the additional condition that there may only be one complete parse. I think this is what we want. I guess "equivalent" just means equality without suggesting that the type is an instance of Eq. There are other places where the report uses == in situations where you can't really apply it, for example, in D.2 it says "we would have [Orange ..] == [Orange, Yellow, Green]", which is true, but we can't use this expresion and expect it to reduce to True, because it is just not type correct. So I think we should ignore this problem now. All the best Christian Sievers
On Tue, 29 Oct 2002, Christian Sievers wrote:
I guess "equivalent" just means equality without suggesting that the type is an instance of Eq. There are other places where the report uses == in situations where you can't really apply it, for example, in D.2 it says "we would have [Orange ..] == [Orange, Yellow, Green]", which is true, but we can't use this expresion and expect it to reduce to True, because it is just not type correct.
Why is that expression not type-correct? -- Dean
Dean Herington wrote:
On Tue, 29 Oct 2002, Christian Sievers wrote:
I guess "equivalent" just means equality without suggesting that the type is an instance of Eq. There are other places where the report uses == in situations where you can't really apply it, for example, in D.2 it says "we would have [Orange ..] == [Orange, Yellow, Green]", which is true, but we can't use this expresion and expect it to reduce to True, because it is just not type correct.
Why is that expression not type-correct?
[Answering my own question...] Duh. Because the type doesn't partake of Eq. -- Dean
Dean Herington wrote:
Why is that expression not type-correct?
[Answering my own question...]
Duh. Because the type doesn't partake of Eq.
Right. Of course, it's a different kind of error than for example [Orange] == Orange --- where no Eq Color instance decl would help, and I wonder if there is a special name for it. Bye Christian Sievers
On Tue, 29 Oct 2002, Simon Peyton-Jones wrote:
Some last-ditch H98 stuff. I have the proofs now and have to send them back this week. Changes will become impossible (or at least much harder) after that. Ah well, I'm sure more errors will come to light.
Simon
| > | (3) Section D.4 gives the expected rule: | > | | > | head (readsPrec d (showsPrec d x "")) == (x,"") | > | | > | Why should this not be: | > | | > | readsPrec d (showsPrec d x "") == [(x,"")] | > | > I can't think why not, unless there is a shorter valid parse, which I | > suppose is conceivable. I'd rather not change this. | | In fact, neither rule above is true for the example given in section D.5. | To see this, run the following program: | | infix 5 :^: | data Tree a = Leaf a | Tree a :^: Tree a deriving (Eq, Ord, Read, Show) | main = mapM_ trial [0..10] | where trial d = print (readsPrec d (showsPrec d x "") :: [(Tree Int, | String)]) | x = Leaf 1 :^: Leaf 2
Uh huh. For
readsPrec 0 "Leaf 1 :^: Leaf 2" we get [(Leaf 1, " :^ Leaf 2"), (Leaf1 :^: Leaf 2, "")]
That is, there are two parses, and the shortest parse comes first. Same is true for Hugs. Not unreasonable, actually, and nothing in the specification seems to preclude this.
I can only make minimal changes now. I suspect the smallest change is to require that (x,"") `elem` readsPrec d (showsPrec d x "")
This weakens the existing equation by not requiring (x,"") to be the first parse returned.
Dean writes: | Perhaps we want: | | readsPrec should be able to parse the string produced by showsPrec, and | should deliver the value that showsPrec started with. That is, the list | result of | | readsPrec d (showsPrec d x "") | | should contain exactly one pair whose second element is "", and the first | element of that pair should be equivalent to x.
I don't understand this. What does "equivalent" mean? And how does this differ from the (incorrect) claim that
readsPrec d (showsPrec d x "") == [(x,"")]
Simon
As Christian Sievers pointed out: 1. We want to require that there be exactly one complete parse. 2. It is not necessary that the type in question partake of Eq. If we're willing to accept the abuse of the (==) notation, I think his expression of the rule (involving a list comprehension) is fine. -- Dean
participants (3)
-
Christian Sievers -
Dean Herington -
Simon Peyton-Jones