Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Base definitions for refinement predicates.
Synopsis
- class Predicate p => Refine p a where
- validate :: Proxy# p -> a -> Maybe (RefineFailure String)
- class Predicate p => Refine1 p f where
- validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String)
- data RefineFailure a = RefineFailure {
- refineFailurePredicate :: a
- refineFailureDetail :: a
- refineFailureInner :: [RefineFailure a]
- class Predicate p where
- predicateName :: Proxy# p -> Int -> ShowS
Documentation
class Predicate p => Refine p a where Source #
Refine a
with predicate p
.
Instances
Refine Fail a Source # | |
Defined in Rerefined.Predicate.Fail | |
Refine Succeed a Source # | |
Defined in Rerefined.Predicate.Succeed | |
Refine p a => Refine (Not p :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical | |
(KnownNat n, MonoFoldable a, ReifyRelOp op) => Refine (CompareLength op n :: Type) a Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length validate :: Proxy# (CompareLength op n) -> a -> Maybe (RefineFailure String) Source # | |
(KnownNat n, Num a, Ord a, ReifyRelOp op, ReifySignedNat sign n, ReifySign sign) => Refine (CompareValue op sign n :: Type) a Source # | |
Defined in Rerefined.Predicate.Relational.Value validate :: Proxy# (CompareValue op sign n) -> a -> Maybe (RefineFailure String) Source # | |
(Refine l a, Refine r a, ReifyLogicOp op) => Refine (Logical op l r :: Type) a Source # | |
Defined in Rerefined.Predicate.Logical |
class Predicate p => Refine1 p f where Source #
Refine functor type f
with functor predicate p
.
By not making the contained type accessible, we ensure refinements apply
forall a. f a
. That is, refinements here apply only to the functor
structure, and not the stored elements.
validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String) Source #
Validate predicate p
for the given f a
.
Instances
(KnownNat n, Foldable f, ReifyRelOp op) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length validate1 :: forall (a :: k1). Proxy# (CompareLength op n) -> f a -> Maybe (RefineFailure String) Source # |
data RefineFailure a Source #
Predicate validation failure.
Polymorphic over the message type because I want to use Text
, but want it
doesn't have the convenient Show
internals that String
does.
RefineFailure | |
|
class Predicate p where Source #
Types which define refinements on other types.
predicateName :: Proxy# p -> Int -> ShowS Source #
The predicate name, as a Show
-like (for good bracketing).
Non-combinator predicates may derive this via Typeably
. Combinator
predicates must write a Show
-like instance manually, in order to avoid
incurring insidious Typeable
contexts for the wrapped predicate(s).
(TODO figure out some generics and/or TH to resolve that)