[Haskell] standard prelude and specifications

Laszlo Nemeth lnemeth at cs.bilgi.edu.tr
Thu Apr 13 05:21:45 EDT 2006


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

More information about the Haskell mailing list