| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Rerefined.Predicate
Description
Base definitions for refinement predicates.
Synopsis
- class Predicate p => Refine (p :: k) a where
- validate :: Proxy# p -> a -> Maybe RefineFailure
- class Predicate p => Refine1 (p :: k) (f :: k1 -> Type) where
- validate1 :: forall (a :: k1). Proxy# p -> f a -> Maybe RefineFailure
- data RefineFailure = RefineFailure {}
- class Predicate (p :: k) where
- type PredicateName (d :: Natural) (p :: k) :: Symbol
- type KnownPredicateName (p :: k) = KnownSymbol (PredicateName 0 p)
- predicateName :: forall {k} (p :: k). KnownPredicateName p => String
Documentation
class Predicate p => Refine (p :: k) a where Source #
Refine a with predicate p.
Note that validate implementations decide what failure information is
emitted. They don't even have to emit their own predicate name, even though
Predicate is in the context. This is useful in certain cases such as
Rerefined.Predicate.Via.
That does mean that the Predicate context may not be used occasionally. But
it's very useful, since otherwise combinator predicates have to constantly
state (Refine p a, Predicate p), and all predicates should have a pretty
name even if it doesn't get printed under normal circumstances.
Methods
Instances
class Predicate p => Refine1 (p :: k) (f :: k1 -> Type) 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.
Methods
validate1 :: forall (a :: k1). Proxy# p -> f a -> Maybe RefineFailure Source #
Validate predicate p for the given f a.
Instances
| (KnownNat n, Foldable f, ReifyRelOp op, KnownPredicateName (CompareLength op n)) => Refine1 (CompareLength op n :: Type) (f :: Type -> Type) Source # | Compare the length of a |
Defined in Rerefined.Predicate.Relational.Length Methods validate1 :: Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure Source # | |
data RefineFailure Source #
Predicate validation failure.
Constructors
| RefineFailure | |
Fields
| |
Instances
| Show RefineFailure Source # | |
Defined in Rerefined.Predicate Methods showsPrec :: Int -> RefineFailure -> ShowS # show :: RefineFailure -> String # showList :: [RefineFailure] -> ShowS # | |
class Predicate (p :: k) Source #
Types which define refinements on other types.
Associated Types
type PredicateName (d :: Natural) (p :: k) :: Symbol Source #
Predicate name.
Predicate names should aim to communicate the meaning of the predicate as clearly and concisely as possible.
Consider using the package type-level-show to build this.
Instances
type KnownPredicateName (p :: k) = KnownSymbol (PredicateName 0 p) Source #
Constraint for reifying a predicate name.
predicateName :: forall {k} (p :: k). KnownPredicateName p => String Source #
Reify predicate name to a String.
Using this regrettably necessitates UndecidableInstances, due to the type
family in the constraint. It sucks, but that's life.