ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.PartialOrd

4 types
1 class
9 values

PackageAgda-2.7.0.1
Exports14
LanguageHaskell2010
LicenceMIT
SourcePartialOrd.hs

datadata 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).

Instances7Bounded, Enum, Eq, Show, Semigroup, Monoid, …

Bounded PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Enum PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Eq PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Show PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Semigroup PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Partial ordering forms a monoid under sequencing.
Monoid PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
PartialOrd PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Less is ``less general'' (i.e., more precise).

valueleqPO :: PartialOrdering -> PartialOrdering -> Bool

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

Includes equality: x leqPO x == True.

valueoppPO :: PartialOrdering -> PartialOrdering

Opposites.

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

valueorPO :: 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.

valueseqPO :: 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.

valuefromOrdering :: Ordering -> PartialOrdering

Embed Ordering.

valuefromOrderings :: [Ordering] -> PartialOrdering

Represent a non-empty disjunction of Orderings as PartialOrdering.

valuetoOrderings :: PartialOrdering -> [Ordering]

A PartialOrdering information is a disjunction of Ordering informations.

Comparison with partial result

4 declarations

typetype Comparable a = a -> a -> PartialOrdering

classclass PartialOrd a where

Decidable partial orderings.

Methods

comparable :: Comparable a

Instances20PartialOrd, …

PartialOrd CohesionDefined in Agda-2.7.0.1 · Agda.Syntax.Common
Flatter is smaller.
PartialOrd ModalityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
Dominance ordering.
PartialOrd QuantityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
Note that the order is ω ≤ 0,1, more options is smaller.
PartialOrd RelevanceDefined in Agda-2.7.0.1 · Agda.Syntax.Common
More relevant is smaller.
PartialOrd OrderDefined in Agda-2.7.0.1 · Agda.Termination.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).
PartialOrd PartialOrderingDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Less is ``less general'' (i.e., more precise).
PartialOrd IntegerDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
PartialOrd IntDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
PartialOrd ()Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
PartialOrd (CallMatrixAug cinfo)Defined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
PartialOrd a => PartialOrd (CallMatrix' a)Defined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
PartialOrd a => PartialOrd (Pointwise [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
The pointwise ordering for lists of the same length.
There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.
PartialOrd a => PartialOrd (Maybe a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Nothing and Just _ are unrelated.
Partial ordering for Maybe a is the same as for Either () a.
PartialOrd t => PartialOrd (UnderAddition t)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
PartialOrd t => PartialOrd (UnderComposition t)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
Ord a => PartialOrd (Inclusion (Set a))Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Sets are partially ordered by inclusion.
Ord a => PartialOrd (Inclusion [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Sublist for ordered lists.
(PartialOrd a, PartialOrd b) => PartialOrd (Either a b)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Partial ordering for disjoint sums: Left _ and Right _ are unrelated.
(PartialOrd a, PartialOrd b) => PartialOrd (a, b)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Pointwise partial ordering for tuples.
related (x1,x2) o (y1,y2) iff related x1 o x2 and related y1 o y2.
(Ord i, PartialOrd a) => PartialOrd (Matrix i a)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Pointwise comparison. Only matrices with the same dimension are comparable.

valuecomparableOrd :: Ord a => Comparable a

Any Ord is a PartialOrd.

Totally ordered types.

0 declarations

Generic partially ordered types.

2 declarations

newtypenewtype Pointwise a

Pointwise comparison wrapper.

Constructors

Pointwise
- pointwise :: a

Instances4Functor, Eq, Show, PartialOrd

Functor PointwiseDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Eq a => Eq (Pointwise a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Show a => Show (Pointwise a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
PartialOrd a => PartialOrd (Pointwise [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
The pointwise ordering for lists of the same length.
There are other partial orderings for lists, e.g., prefix, sublist, subset, lexicographic, simultaneous order.

newtypenewtype Inclusion a

Inclusion comparison wrapper.

Constructors

Inclusion
- inclusion :: a

Instances6Functor, Eq, Ord, Show, PartialOrd

Functor InclusionDefined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Eq a => Eq (Inclusion a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Ord a => Ord (Inclusion a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Show a => Show (Inclusion a)Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Ord a => PartialOrd (Inclusion (Set a))Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Sets are partially ordered by inclusion.
Ord a => PartialOrd (Inclusion [a])Defined in Agda-2.7.0.1 · Agda.Utils.PartialOrd
Sublist for ordered lists.

PartialOrdering is itself partially ordered!

0 declarations