Rerefined.Predicate.Relational.Length

Documentation

data CompareLength op (n :: Natural)

Compare length to a type-level Natural using the given RelOp.

Instances

(KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type)

Compare the length of a Foldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure

Predicate (CompareLength op n :: Type)

Precedence of 4 (matching base relational operators e.g. >=).

Defined in Rerefined.Predicate.Relational.Length

Associated Types

type PredicateName d (CompareLength op n) :: Symbol

(KnownNat n, MonoFoldable a, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine (CompareLength op n :: Type) a

Compare the length of a MonoFoldable to a type-level Natural using the given RelOp.

Defined in Rerefined.Predicate.Relational.Length

Methods

validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure

type PredicateName d (CompareLength op n :: Type)

Defined in Rerefined.Predicate.Relational.Length

type PredicateName d (CompareLength op n :: Type) = ShowParen (d > 4) ((("Length " ++ ShowRelOp op) ++ ShowChar ' ') ++ ShowNatDec n)

validateCompareLength :: forall op n. (KnownNat n, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure

widenCompareLength :: forall m op n a. WROE op n m => Refined (CompareLength op n) a -> Refined (CompareLength op m) a

Widen a length comparison predicate.

Only valid widenings are permitted, checked at compile time.

Example: Given a >= 1, we know also that a >= 0. Thus, this function allows you to turn a Refined (CompareLength GTE 1) a into a Refined (CompareLength GTE 0) a.

TODO improve type error here

widenCompareLength1 :: forall m op n f a. WROE op n m => Refined1 (CompareLength op n) f a -> Refined1 (CompareLength op m) f a

Widen a length comparison predicate.

Only valid widenings are permitted, checked at compile time.

Example: Given a >= 1, we know also that a >= 0. Thus, this function allows you to turn a Refined1 (CompareLength GTE 1) f a into a Refined1 (CompareLength GTE 0) f a.

TODO improve type error here

type WROE op n m = WROE' op n m (WidenRelOp op n m)

type family WROE' op n m b where ...

Equations

WROE' op n m True = ()

WROE' op n m False = TypeError (((Text "can't widen relational equation " :$$: ((ShowType op :<>: Text " ") :<>: ShowType n)) :$$: Text "to") :$$: ((ShowType op :<>: Text " ") :<>: ShowType m))