Safe Haskell	None
Language	GHC2021

Rerefined.Predicate.Relational.Internal

Description

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!

Synopsis

type LTE = Or 'LT 'EQ
type NEQ = Or 'LT 'GT
type GTE = Or 'GT 'EQ
class ReifyRelOp (op :: k) where
- type ShowRelOp (op :: k) :: Symbol
- reifyRelOp :: Ord a => a -> a -> Bool
type family WidenRelOp (op :: k) (n :: Natural) (m :: Natural) :: Bool where ...
type family NormalizeOrRelOp op where ...

Documentation

type LTE = Or 'LT 'EQ Source #

type NEQ = Or 'LT 'GT Source #

"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 = Or 'GT 'EQ Source #

class ReifyRelOp (op :: k) where Source #

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 :: k) :: Symbol Source #

Pretty op.

Methods

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

The term-level relational operator that op describes.

Instances

Instances details

ReifyRelOp 'EQ Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'EQ
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp 'EQ = "=="

Methods

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

ReifyRelOp 'GT Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'GT
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp 'GT = ">"

Methods

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

ReifyRelOp 'LT Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'LT
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp 'LT = "<"

Methods

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

ReifyRelOp GTE Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp GTE = ">="

Methods

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

ReifyRelOp LTE Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp LTE = "<="

Methods

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

ReifyRelOp NEQ Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp NEQ = "/="

Methods

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

ReifyRelOp (Or 'EQ 'GT) Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT)	Hidden instance. You won't see this if you use the type synonyms.
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

Methods

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

ReifyRelOp (Or 'EQ 'LT) Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT)	Hidden instance. You won't see this if you use the type synonyms.
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

Methods

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

ReifyRelOp (Or 'GT 'LT) Source #

Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT)	Hidden instance. You won't see this if you use the type synonyms.
Instance details Defined in Rerefined.Predicate.Relational.Internal type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

Methods

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

type family WidenRelOp (op :: k) (n :: Natural) (m :: Natural) :: Bool where ... Source #

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

Equations

WidenRelOp (op :: k) 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 (Or 'EQ 'LT) n m = OrdCond (CmpNat n m) 'True 'True 'False
WidenRelOp (Or 'EQ 'GT) n m = OrdCond (CmpNat n m) 'False 'True 'True
WidenRelOp (_1 :: k) _2 _3 = 'False

type family NormalizeOrRelOp op where ... Source #

Equations

NormalizeOrRelOp (Or 'EQ 'LT) = LTE
NormalizeOrRelOp (Or 'GT 'LT) = NEQ
NormalizeOrRelOp (Or 'EQ 'GT) = GTE