[Haskell] standard prelude and specifications
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.
More information about the Haskell