Conor McBride <[EMAIL PROTECTED]> responded to my comment:
> > (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.}
}
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
