Joe Fasel <[EMAIL PROTECTED]> writes on 19 Jan 2000
on partition and lifted products
that
partition1 p xs = (filter p xs, filter (not . p) xs)
(is this the recent standard description of `partition' ?)
and optimized implementations, like, say,
partition2 p = foldr (\x (ys, zs) -> if p x then (x:ys,zs) else (ys,x:zs))
([],[])
may be not equivalent.
Because they behave differently respectively to `undefined'.
Indeed, this is very important. I asked about this a couple of days
earlier. But no-one noticed.
The questions are:
(1) What laziness freedom is allowed for a Standard function
implementation?
(2) Should Haskell consider also the stronger equivalence relation
on programs?
Example for (1).
For the standard description
partition p xs = (filter p xs, filter (not . p) xs)
which of implementations are _correct_:
pt _ [] = ([], [])
pt p (x:xs) = if p x then (x:ys, zs) else (ys, x:zs)
where (ys,zs) = pt p xs
pt' _ [] = ([],[])
pt' p (x:xs) = case pt' p xs
of
(ys,zs) -> if p x then (x:ys, zs) else (ys, x:zs)
?
It may occur, that suggesting optimizations for the standard function
implementations would mostly mean suggesting the change of the
library description.
What is the Haskell policy in respect to this?
On (2).
Maybe, this is rather naive, but still I ask.
If we introduce the stronger equivalence (u-equivalence),
for example,
tail = (\xs -> case xs of _:ys -> ys
_ -> error "tail []"
)
and tail' = (\xs -> case xs of _:ys -> ys
_ -> []
)
to be u-equivalent, would it have some practical sense?
And who knows the proper notion and the term for this?
The functions have to be equivalent when their maps coincide at some
good domain where both have values different from `undefined' -
something of this sort.
Giving certain compilation key, the programmer allows strong
optimizations but knows that the run-time result will be correct
only for the "regular" argument - which do not cause esoteric
`undefined'-s in the computation way.
It is (mostly) on the programmer to recognize the "regular"
arguments.
The u-equivalence would provide a huge possibility to transform
and optimize the programs. For example, several discussed here
definitions for `partition' become transformable to each other.
If this does not lead to any great nonsense, then we could require
the compilation key
-ueq
to support the u-equivalence, to give the compiler more freedom to
transform the functions changing laziness policy, and such.
Maybe, the pragma {-# ueq ...-#}
may help to separate the ueq segments in the program.
Similar question appeared about an year ago, when people discussed
how widely the _rules_ can be treated. For example, as it may occur
n = undefined, then what sense may have the rule
n - n :: Integer === 0.
What the experts think of this -ueq ?
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
