Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.PartialOrd

Contents

Comparison with partial result
Totally ordered types.
Generic partially ordered types.
PartialOrdering is itself partially ordered!

Synopsis

Documentation

data PartialOrdering #

The result of comparing two things (of the same type).

Constructors

POLT	Less than.
POLE	Less or equal than.
POEQ	Equal
POGE	Greater or equal.
POGT	Greater than.
POAny	No information (incomparable).

Instances

Bounded PartialOrdering #
Methods minBound :: PartialOrdering # maxBound :: PartialOrdering #
Enum PartialOrdering #
Methods succ :: PartialOrdering -> PartialOrdering # pred :: PartialOrdering -> PartialOrdering # toEnum :: Int -> PartialOrdering # fromEnum :: PartialOrdering -> Int # enumFrom :: PartialOrdering -> [PartialOrdering] # enumFromThen :: PartialOrdering -> PartialOrdering -> [PartialOrdering] # enumFromTo :: PartialOrdering -> PartialOrdering -> [PartialOrdering] # enumFromThenTo :: PartialOrdering -> PartialOrdering -> PartialOrdering -> [PartialOrdering] #
Eq PartialOrdering #
Methods (==) :: PartialOrdering -> PartialOrdering -> Bool # (/=) :: PartialOrdering -> PartialOrdering -> Bool #
Show PartialOrdering #
Methods showsPrec :: Int -> PartialOrdering -> ShowS # show :: PartialOrdering -> String # showList :: [PartialOrdering] -> ShowS #
Semigroup PartialOrdering #	Partial ordering forms a monoid under sequencing.
Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering # sconcat :: NonEmpty PartialOrdering -> PartialOrdering # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering #
Monoid PartialOrdering #
Methods mempty :: PartialOrdering # mappend :: PartialOrdering -> PartialOrdering -> PartialOrdering # mconcat :: [PartialOrdering] -> PartialOrdering #
PartialOrd PartialOrdering #	Less is ``less general'' (i.e., more precise).
Methods comparable :: Comparable PartialOrdering #

leqPO :: PartialOrdering -> PartialOrdering -> Bool #

Comparing the information content of two elements of PartialOrdering. More precise information is smaller.

Includes equality: x leqPO x == True.

oppPO :: PartialOrdering -> PartialOrdering #

Opposites.

related a po b iff related b (oppPO po) a.

orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering #

Combining two pieces of information (picking the least information). Used for the dominance ordering on tuples.

orPO is associative, commutative, and idempotent. orPO has dominant element POAny, but no neutral element.

seqPO :: PartialOrdering -> PartialOrdering -> PartialOrdering #

Chains (transitivity) x R y S z.

seqPO is associative, commutative, and idempotent. seqPO has dominant element POAny and neutral element (unit) POEQ.

fromOrdering :: Ordering -> PartialOrdering #

Embed Ordering.

fromOrderings :: [Ordering] -> PartialOrdering #

Represent a non-empty disjunction of Orderings as PartialOrdering.

toOrderings :: PartialOrdering -> [Ordering] #

A PartialOrdering information is a disjunction of Ordering informations.

Comparison with partial result

type Comparable a = a -> a -> PartialOrdering #

class PartialOrd a where #

Decidable partial orderings.

Minimal complete definition

comparable

Methods

comparable :: Comparable a #

Instances

PartialOrd Int #
Methods comparable :: Comparable Int #
PartialOrd Integer #
Methods comparable :: Comparable Integer #
PartialOrd () #
Methods comparable :: Comparable () #
PartialOrd PartialOrdering #	Less is ``less general'' (i.e., more precise).
Methods comparable :: Comparable PartialOrdering #
PartialOrd Order #	Information order: `Unknown` is least information. The more we decrease, the more information we have. When having comparable call-matrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information).
Methods comparable :: Comparable Order #
PartialOrd a => PartialOrd (Maybe a) #	`Nothing` and `Just _` are unrelated. Partial ordering for `Maybe a` is the same as for `Either () a`.
Methods comparable :: Comparable (Maybe a) #
Ord a => PartialOrd (Inclusion [a]) #	Sublist for ordered lists.
Methods comparable :: Comparable (Inclusion [a]) #
Ord a => PartialOrd (Inclusion (Set a)) #	Sets are partially ordered by inclusion.
Methods comparable :: Comparable (Inclusion (Set a)) #
PartialOrd a => PartialOrd (Pointwise [a]) #	The pointwise ordering for lists of the same length. There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.
Methods comparable :: Comparable (Pointwise [a]) #
PartialOrd (CallMatrixAug cinfo) #
Methods comparable :: Comparable (CallMatrixAug cinfo) #
PartialOrd a => PartialOrd (CallMatrix' a) #
Methods comparable :: Comparable (CallMatrix' a) #
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b) #	Partial ordering for disjoint sums: `Left _` and `Right _` are unrelated.
Methods comparable :: Comparable (Either a b) #
(PartialOrd a, PartialOrd b) => PartialOrd (a, b) #	Pointwise partial ordering for tuples. `related (x1,x2) o (y1,y2)` iff `related x1 o x2` and `related y1 o y2`.
Methods comparable :: Comparable (a, b) #
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) #	Pointwise comparison. Only matrices with the same dimension are comparable.
Methods comparable :: Comparable (Matrix i a) #

comparableOrd :: Ord a => Comparable a #

Any Ord is a PartialOrd.

related :: PartialOrd a => a -> PartialOrdering -> a -> Bool #

Are two elements related in a specific way?

related a o b holds iff comparable a b is contained in o.

Totally ordered types.

Generic partially ordered types.

newtype Pointwise a #

Pointwise comparison wrapper.

Constructors

Pointwise
Fields pointwise :: a

Instances

Functor Pointwise #
Methods fmap :: (a -> b) -> Pointwise a -> Pointwise b # (<$) :: a -> Pointwise b -> Pointwise a #
Eq a => Eq (Pointwise a) #
Methods (==) :: Pointwise a -> Pointwise a -> Bool # (/=) :: Pointwise a -> Pointwise a -> Bool #
Show a => Show (Pointwise a) #
Methods showsPrec :: Int -> Pointwise a -> ShowS # show :: Pointwise a -> String # showList :: [Pointwise a] -> ShowS #
PartialOrd a => PartialOrd (Pointwise [a]) #	The pointwise ordering for lists of the same length. There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.
Methods comparable :: Comparable (Pointwise [a]) #

newtype Inclusion a #

Inclusion comparison wrapper.

Constructors

Inclusion
Fields inclusion :: a

Instances

Functor Inclusion #
Methods fmap :: (a -> b) -> Inclusion a -> Inclusion b # (<$) :: a -> Inclusion b -> Inclusion a #
Eq a => Eq (Inclusion a) #
Methods (==) :: Inclusion a -> Inclusion a -> Bool # (/=) :: Inclusion a -> Inclusion a -> Bool #
Ord a => Ord (Inclusion a) #
Methods compare :: Inclusion a -> Inclusion a -> Ordering # (<) :: Inclusion a -> Inclusion a -> Bool # (<=) :: Inclusion a -> Inclusion a -> Bool # (>) :: Inclusion a -> Inclusion a -> Bool # (>=) :: Inclusion a -> Inclusion a -> Bool # max :: Inclusion a -> Inclusion a -> Inclusion a # min :: Inclusion a -> Inclusion a -> Inclusion a #
Show a => Show (Inclusion a) #
Methods showsPrec :: Int -> Inclusion a -> ShowS # show :: Inclusion a -> String # showList :: [Inclusion a] -> ShowS #
Ord a => PartialOrd (Inclusion [a]) #	Sublist for ordered lists.
Methods comparable :: Comparable (Inclusion [a]) #
Ord a => PartialOrd (Inclusion (Set a)) #	Sets are partially ordered by inclusion.
Methods comparable :: Comparable (Inclusion (Set a)) #

PartialOrdering is itself partially ordered!