rerefined-0.5.1: Refinement types, again
Safe HaskellSafe-Inferred
LanguageGHC2021

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

Documentation

type LTE = LT `Or` EQ Source #

type NEQ = LT `Or` 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 = GT `Or` EQ Source #

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.

Associated Types

type ShowRelOp op :: Symbol Source #

Pretty op.

Methods

reifyRelOp :: forall a. 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 :: Symbol Source #

Methods

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

ReifyRelOp 'GT Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'GT :: Symbol Source #

Methods

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

ReifyRelOp 'LT Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp 'LT :: Symbol Source #

Methods

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

ReifyRelOp GTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE :: Symbol Source #

Methods

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

ReifyRelOp LTE Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE :: Symbol Source #

Methods

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

ReifyRelOp NEQ Source # 
Instance details

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ :: Symbol Source #

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

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

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

Methods

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

type family WidenRelOp op n m where ... Source #

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