Agda.Utils.PartialOrd

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 Relevance

More relevant is smaller.

Methods

comparable :: Comparable Relevance

PartialOrd Quantity

Methods

comparable :: Comparable Quantity

PartialOrd Modality

Dominance ordering.

Methods

comparable :: Comparable Modality

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!