[Haskell] standard prelude and specifications

[Laszlo Nemeth]

Hi,

Chp 8 of the Haskell Report says:

> In this chapter the entire Haskell Prelude is given. 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.



My question is how strictly this word "specification" is to be 
interpreted? I can think of a strict and a loose interpretation:

(1 - strict) Whatever invariant I can read out from the code which is 
given I am allowed to interpret it as part of the specification. e.g  
here is the code for filter:

filter :: (a -> Bool) -> [a] -> [a]
filter p []                 = []
filter p (x:xs) | p x       = x : filter p xs
               | otherwise = filter p xs

Primarily this states that the resulting list have no elements for which 
the predicate 'p' does not hold.

But I can also read out from the code that filter does not rearrange the 
elements in the list: for example if the list was sorted, it remains so 
afterwards. Under the strict interpretation this is also taken as part 
of specification for filter.

(2 - loose)  Filter is  meant to drop elements for which the predicate 
'p' doesn' t hold, and an implementation is free to rearrange the elements.

There must have been some discussion of this earlier but google didn't 
find anything useful.

Thanks, Laszlo