Safe Haskell | Safe-Inferred |
---|---|
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 Ord
s. We can utilize this to define /relational
operators/:
LT
,EQ
andGT
already map to relational operators.- The others can be defined by combining the above with
Or
. e.g.
-> "less than or equal" (LT
`Or`
EQ
<=
)
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 = LT `Or` EQ
- type NEQ = LT `Or` GT
- type GTE = GT `Or` EQ
- class ReifyRelOp op where
- type ShowRelOp op :: Symbol
- reifyRelOp :: forall a. Ord a => a -> a -> Bool
- type family WidenRelOp op n m where ...
- type family NormalizeOrRelOp op where ...
Documentation
class ReifyRelOp op where Source #
Reify a relational operator type tag.
Permitted operators are Ordering
constructors LT
, EQ
and GT
; and
combinations of these using Or
.
Methods
reifyRelOp :: forall a. Ord a => a -> a -> Bool Source #
The term-level relational operator that op
describes.
Instances
ReifyRelOp 'EQ Source # | |
ReifyRelOp 'GT Source # | |
ReifyRelOp 'LT Source # | |
ReifyRelOp GTE Source # | |
ReifyRelOp LTE Source # | |
ReifyRelOp NEQ Source # | |
ReifyRelOp (Or 'EQ 'GT) Source # | |
ReifyRelOp (Or 'EQ 'LT) Source # | |
ReifyRelOp (Or 'GT 'LT) Source # | |
type family WidenRelOp op n m where ... Source #
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 ... Source #
Equations
NormalizeOrRelOp (EQ `Or` LT) = LTE | |
NormalizeOrRelOp (GT `Or` LT) = NEQ | |
NormalizeOrRelOp (EQ `Or` GT) = GTE |