Some clarity please! (was Re: [Haskell-cafe] Re: (flawed?) benchmark : sort)

[kahl at cas.mcmaster.ca]

Conor McBride <conor at strictlypositive.org> 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.}
}