Copyright | (c) Nils Anders Danielsson 2004-2022 2024 |
---|---|
License | See the file LICENCE. |
Maintainer | http://www.cse.chalmers.se/~nad/ |
Stability | experimental |
Portability | non-portable (GHC-specific) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Generic semantic equality and order. The semantic order referred
to is that of a typical CPO for Haskell types, where e.g. (
, but where True
,
bottom
) <=!
(True
, False
)(
and True
, True
)(
are incomparable.True
, False
)
The implementation is based on isBottom
, and has the same
limitations. Note that non-bottom functions are not handled by any
of the functions described below.
One could imagine using QuickCheck for testing equality of functions, but I have not managed to tweak the type system so that it can be done transparently.
Synopsis
- data Tweak = Tweak {
- approxDepth :: Maybe Nat
- timeOutLimit :: Maybe Int
- noTweak :: Tweak
- class SemanticEq a where
- class SemanticEq a => SemanticOrd a where
Documentation
The behaviour of some of the functions below can be tweaked.
Tweak | |
|
class SemanticEq a where Source #
SemanticEq
contains methods for testing whether two terms are
semantically equal.
class SemanticEq a => SemanticOrd a where Source #
SemanticOrd
contains methods for testing whether two terms are
related according to the semantic domain ordering.
(<!) :: a -> a -> Bool infix 4 Source #
(<=!) :: a -> a -> Bool infix 4 Source #
(>=!) :: a -> a -> Bool infix 4 Source #
(>!) :: a -> a -> Bool infix 4 Source #
semanticCompare :: Tweak -> a -> a -> Maybe Ordering Source #
returns semanticCompare
tweak x yNothing
if x
and y
are
incomparable, and
otherwise, where Just
oo ::
represents the relation between Ordering
x
and y
.
(\/!) :: a -> a -> Maybe a infix 5 Source #
(/\!) :: a -> a -> a infixl 5 Source #
semanticJoin :: Tweak -> a -> a -> Maybe a Source #
semanticMeet :: Tweak -> a -> a -> a Source #
x
and \/!
yx
compute the least upper and greatest
lower bounds, respectively, of /\!
yx
and y
in the semantical
domain ordering. Note that the least upper bound may not always
exist.
This functionality was implemented just because it was
possible (and to provide analogues of max
and min
in the Ord
class). If anyone finds any use for it, please let me know.
Instances
Data a => SemanticOrd a Source # | |
Defined in Test.ChasingBottoms.SemanticOrd (<!) :: a -> a -> Bool Source # (<=!) :: a -> a -> Bool Source # (>=!) :: a -> a -> Bool Source # (>!) :: a -> a -> Bool Source # semanticCompare :: Tweak -> a -> a -> Maybe Ordering Source # (\/!) :: a -> a -> Maybe a Source # semanticJoin :: Tweak -> a -> a -> Maybe a Source # semanticMeet :: Tweak -> a -> a -> a Source # |