
Conor McBride
(mapMonotonic should of course be removed, too, or specified to fail (preferably in some MonadZero) if the precondition is violated, which should still be implementable in linear time.)
What's wrong with mapMonotonic that isn't wrong with, say, sortBy?, or Eq instances for parametrized types?
Prelude> :m + Data.Set Prelude Data.Set> toAscList $ mapMonotonic (10 -) (fromList [1 .. 5]) [9,8,7,6,5] Prelude Data.Set> 5 `member` mapMonotonic (10 -) (fromList [1 .. 5]) False Something's certainly wrong there!
Before we can talk about what == should return, can we settle what we mean by = ?
``='' is not in the Haskell interface! ;-) Therefore, I talked only about (==). The best way to include ``='' seems to be the semantic equality of P-logic [Harrison-Kieburtz-2005], which is quite a heavy calibre, and at least in that paper, classes are not yet included. Wolfram -------------------- @Article{Harrison-Kieburtz-2005, author = {William L. Harrison and Richard B. Kieburtz}, title = {The logic of demand in {Haskell}}, journal = JFP, year = 2005, volume = 15, number = 6, pages = {837--891}, abstract = {Haskell is a functional programming language whose evaluation is lazy by default. However, Haskell also provides pattern matching facilities which add a modicum of eagerness to its otherwise lazy default evaluation. This mixed or ``non-strict'' semantics can be quite difficult to reason with. This paper introduces a programming logic, P-logic, which neatly formalizes the mixed evaluation in Haskell pattern-matching as a logic, thereby simplifying the task of specifying and verifying Haskell programs. In p-logic, aspects of demand are reflected or represented within both the predicate language and its model theory, allowing for expressive and comprehensible program verification.} }