Rerefined.Predicate.Relational.Internal

Relational operator definitions.

Haskell base exports the type Ordering, which is an enum that states the result of comparing two Ords. We can utilize this to define /relational operators/:

• LT, EQ and GT already map to relational operators.
• The others can be defined by combining the above with Or. e.g. LT `Or` EQ -> "less than or equal" (<=)

What's the point? We save on definitions, and get to reuse well-known data types which most users will have intuition for. We do have to contest with commutativity, but this is an extremely minor concern which can only come up if you don't use the provided type synonyms, or do lots of type-level predicate manipulation. And we provide those swapped-order instances anyway!

Documentation

type LTE = LT `Or` EQ

type NEQ = LT `Or` GT

"not equal to" is equivalent to "strictly less than or greater than". We could use Not, but sticking with just Or keeps the internals simple.

type GTE = GT `Or` EQ

class ReifyRelOp op where

Reify a relational operator type tag.

Permitted operators are Ordering constructors LT, EQ and GT; and combinations of these using Or.

Associated Types

type ShowRelOp op :: Symbol

Pretty op.

Methods

reifyRelOp :: forall a. Ord a => a -> a -> Bool

The term-level relational operator that op describes.

Instances

ReifyRelOp 'EQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'EQ :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'GT

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'GT :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp 'LT

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'LT :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'EQ 'GT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'EQ 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'GT 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

type family WidenRelOp op n m where ...

Can we widen the given RelOp on the given Natural from n to m?

Equations

WidenRelOp op n n = True

WidenRelOp LT n m = OrdCond (CmpNat n m) True True False

WidenRelOp LTE n m = OrdCond (CmpNat n m) True True False

WidenRelOp GTE n m = OrdCond (CmpNat n m) False True True

WidenRelOp GT n m = OrdCond (CmpNat n m) False True True

WidenRelOp (EQ `Or` LT) n m = OrdCond (CmpNat n m) True True False

WidenRelOp (EQ `Or` GT) n m = OrdCond (CmpNat n m) False True True

WidenRelOp _ _ _ = False

type family NormalizeOrRelOp op where ...

Equations

NormalizeOrRelOp (EQ `Or` LT) = LTE

NormalizeOrRelOp (GT `Or` LT) = NEQ

NormalizeOrRelOp (EQ `Or` GT) = GTE