[Haskell] standard prelude and specifications
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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] standard prelude and specifications
Laszlo Nemeth [EMAIL PROTECTED] wrote: Chp 8 of the Haskell Report says: In this chapter the entire Haskell Prelude is given. It constitutes a *specification* for the Prelude. My question is how strictly this word specification is to be interpreted? I can think of a strict and a loose interpretation: Surely the obvious meaning is observational equivalence, also sometimes known as referential transparency. For any Prelude function specified as p, you can implement it differently as p', provided that for all possible arguments x to p, p x == p' x So this is your non-loose interpretation. I hesitate to use the word strict, because that has a different accepted meaning in this context. If p is strict in x, then p' must be strict in x as well, and vice versa; if p is non-strict in x, then p' must also be non-strict. The important point is that p and p' could use algorithms that belong to different complexity classes, or have different constant factors, and that is fine, provided the results are the same. Regards, Malcolm ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
