Safe Haskell | None |
---|---|
Language | Haskell2010 |
In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.
This library allows one to capture the idea of a refinement type
using the Refined
type. A Refined
p
x
wraps a value
of type x
, ensuring that it satisfies a type-level predicate p
.
A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
Synopsis
- data Refined (p :: k) x
- refine :: forall p x. Predicate p x => x -> Either RefineException (Refined p x)
- refine_ :: forall p x. Predicate p x => x -> Either RefineException x
- refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
- refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)
- refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x)
- refineEither :: forall p x. Predicate p x => x -> Either (Refined (Not p) x) (Refined p x)
- refineTH :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))
- refineTH_ :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp x)
- unrefine :: Refined p x -> x
- class Typeable p => Predicate p x where
- validate :: Proxy p -> x -> Maybe RefineException
- reifyPredicate :: forall p a. Predicate p a => a -> Bool
- data Not p = Not
- data And l r = And
- type (&&) = And
- data Or l r = Or
- type (||) = Or
- data Xor l r = Xor
- data IdPred = IdPred
- data LessThan (n :: Nat) = LessThan
- data GreaterThan (n :: Nat) = GreaterThan
- data From (n :: Nat) = From
- data To (n :: Nat) = To
- data FromTo (mn :: Nat) (mx :: Nat) = FromTo
- data NegativeFromTo (n :: Nat) (m :: Nat) = NegativeFromTo
- data EqualTo (n :: Nat) = EqualTo
- data NotEqualTo (n :: Nat) = NotEqualTo
- data Odd = Odd
- data Even = Even
- data DivisibleBy (n :: Nat) = DivisibleBy
- data NaN = NaN
- data Infinite = Infinite
- type Positive = GreaterThan 0
- type NonPositive = To 0
- type Negative = LessThan 0
- type NonNegative = From 0
- type ZeroToOne = FromTo 0 1
- type NonZero = NotEqualTo 0
- data SizeLessThan (n :: Nat) = SizeLessThan
- data SizeGreaterThan (n :: Nat) = SizeGreaterThan
- data SizeEqualTo (n :: Nat) = SizeEqualTo
- type Empty = SizeEqualTo 0
- type NonEmpty = SizeGreaterThan 0
- data Ascending = Ascending
- data Descending = Descending
- class Weaken from to where
- andLeft :: Refined (And l r) x -> Refined l x
- andRight :: Refined (And l r) x -> Refined r x
- leftOr :: Refined l x -> Refined (Or l r) x
- rightOr :: Refined r x -> Refined (Or l r) x
- strengthen :: forall p p' x. (Predicate p x, Predicate p' x) => Refined p x -> Either RefineException (Refined (p && p') x)
- data RefineException
- = RefineNotException !TypeRep
- | RefineAndException !TypeRep !(These RefineException RefineException)
- | RefineOrException !TypeRep !RefineException !RefineException
- | RefineXorException !TypeRep !(Maybe (RefineException, RefineException))
- | RefineSomeException !TypeRep !SomeException
- | RefineOtherException !TypeRep !Text
- displayRefineException :: RefineException -> String
- throwRefineOtherException :: TypeRep -> Text -> Maybe RefineException
- throwRefineSomeException :: TypeRep -> SomeException -> Maybe RefineException
- success :: Maybe RefineException
Refined
type
data Refined (p :: k) x Source #
A refinement type, which wraps a value of type x
.
Since: 0.1.0.0
Instances
Lift x => Lift (Refined p x :: Type) Source # | Since: 0.1.0.0 |
Foldable (Refined p) Source # | Since: 0.2 |
Defined in Refined.Unsafe.Type fold :: Monoid m => Refined p m -> m # foldMap :: Monoid m => (a -> m) -> Refined p a -> m # foldMap' :: Monoid m => (a -> m) -> Refined p a -> m # foldr :: (a -> b -> b) -> b -> Refined p a -> b # foldr' :: (a -> b -> b) -> b -> Refined p a -> b # foldl :: (b -> a -> b) -> b -> Refined p a -> b # foldl' :: (b -> a -> b) -> b -> Refined p a -> b # foldr1 :: (a -> a -> a) -> Refined p a -> a # foldl1 :: (a -> a -> a) -> Refined p a -> a # toList :: Refined p a -> [a] # length :: Refined p a -> Int # elem :: Eq a => a -> Refined p a -> Bool # maximum :: Ord a => Refined p a -> a # minimum :: Ord a => Refined p a -> a # | |
Eq x => Eq (Refined p x) Source # | Since: 0.1.0.0 |
Ord x => Ord (Refined p x) Source # | Since: 0.1.0.0 |
Defined in Refined.Unsafe.Type | |
(Read x, Predicate p x) => Read (Refined p x) Source # | This instance makes sure to check the refinement. Since: 0.1.0.0 |
Show x => Show (Refined p x) Source # | Since: 0.1.0.0 |
(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) Source # | Since: 0.4 |
Hashable x => Hashable (Refined p x) Source # | Since: 0.6.3 |
Defined in Refined.Unsafe.Type | |
(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source # | Since: 0.4 |
(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source # | Since: 0.6.3 |
Defined in Refined toJSONKey :: ToJSONKeyFunction (Refined p a) # toJSONKeyList :: ToJSONKeyFunction [Refined p a] # | |
(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source # | Since: 0.4 |
(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # | |
Defined in Refined fromJSONKey :: FromJSONKeyFunction (Refined p a) # fromJSONKeyList :: FromJSONKeyFunction [Refined p a] # | |
NFData x => NFData (Refined p x) Source # | Since: 0.5 |
Defined in Refined.Unsafe.Type |
Creation
refine :: forall p x. Predicate p x => x -> Either RefineException (Refined p x) Source #
A smart constructor of a Refined
value.
Checks the input value at runtime.
Since: 0.1.0.0
refine_ :: forall p x. Predicate p x => x -> Either RefineException x Source #
Like refine
, but discards the refinement.
This _can_ be useful when you only need to validate
that some value at runtime satisfies some predicate.
See also reifyPredicate
.
Since: 0.4.4
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) Source #
refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x) Source #
Constructs a Refined
value at run-time,
calling throwError
if the value
does not satisfy the predicate.
Since: 0.2.0.0
refineEither :: forall p x. Predicate p x => x -> Either (Refined (Not p) x) (Refined p x) Source #
Like refine
, but, when the value doesn't satisfy the predicate, returns
a Refined
value with the predicate negated, instead of returning
RefineException
.
>>>
isRight (refineEither @Even @Int 42)
True
>>>
isLeft (refineEither @Even @Int 43)
True
refineTH :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp (Refined p x)) Source #
Constructs a Refined
value at compile-time using -XTemplateHaskell
.
For example:
$$(refineTH 23) :: Refined Positive Int Refined 23
Here's an example of an invalid value:
$$(refineTH 0) :: Refined Positive Int <interactive>:6:4: Value is not greater than 0 In the Template Haskell splice $$(refineTH 0) In the expression: $$(refineTH 0) :: Refined Positive Int In an equation for ‘it’: it = $$(refineTH 0) :: Refined Positive Int
The example above indicates a compile-time failure, which means that the checking was done at compile-time, thus introducing a zero-runtime overhead compared to a plain value construction.
Note: It may be useful to use this function with the th-lift-instances package.
Since: 0.1.0.0
refineTH_ :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp x) Source #
Like refineTH
, but immediately unrefines the value.
This is useful when some value need only be refined
at compile-time.
Since: 0.4.4
Consumption
Predicate
class Typeable p => Predicate p x where Source #
A typeclass which defines a runtime interpretation of
a type-level predicate p
for type x
.
Since: 0.1.0.0
validate :: Proxy p -> x -> Maybe RefineException Source #
Check the value x
according to the predicate p
,
producing an error RefineException
if the value
does not satisfy.
Note: validate
is not intended to be used
directly; instead, it is intended to provide the minimal
means necessary for other utilities to be derived. As
such, the Maybe
here should be interpreted to mean
the presence or absence of a RefineException
, and
nothing else.
Instances
reifyPredicate :: forall p a. Predicate p a => a -> Bool Source #
Reify a Predicate
by turning it into a value-level predicate.
Since: 0.4.2.3
Logical predicates
The negation of a predicate.
>>>
isRight (refine @(Not NonEmpty) @[Int] [])
True
>>>
isLeft (refine @(Not NonEmpty) @[Int] [1,2])
True
Since: 0.1.0.0
Not | Since: 0.4.2 |
The conjunction of two predicates.
>>>
isLeft (refine @(And Positive Negative) @Int 3)
True
>>>
isRight (refine @(And Positive Odd) @Int 203)
True
Since: 0.1.0.0
And | Since: 0.4.2 |
The disjunction of two predicates.
>>>
isRight (refine @(Or Even Odd) @Int 3)
True
>>>
isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
True
>>>
isRight (refine @(Or Even Even) @Int 4)
True
Since: 0.1.0.0
Or | Since: 0.4.2 |
The exclusive disjunction of two predicates.
>>>
isRight (refine @(Xor Even Odd) @Int 3)
True
>>>
isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)
True
>>>
isLeft (refine @(Xor Even Even) @Int 2)
True
Since: 0.5
Xor | Since: 0.5 |
Identity predicate
A predicate which is satisfied for all types.
Arguments passed to
in validate
are not evaluated.validate
IdPred
x
>>>
isRight (refine @IdPred @Int undefined)
True
>>>
isLeft (refine @IdPred @Int undefined)
False
Since: 0.3.0.0
IdPred | Since: 0.4.2 |
Numeric predicates
data LessThan (n :: Nat) Source #
A Predicate
ensuring that the value is less than the
specified type-level number.
>>>
isRight (refine @(LessThan 12) @Int 11)
True
>>>
isLeft (refine @(LessThan 12) @Int 12)
True
Since: 0.1.0.0
LessThan | Since: 0.4.2 |
Instances
Generic (LessThan n) Source # | Since: 0.3.0.0 |
(Ord x, Num x, KnownNat n) => Predicate (LessThan n :: Type) x Source # | Since: 0.1.0.0 |
n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source # | Since: 0.2.0.0 |
n <= m => Weaken (LessThan n :: Type) (LessThan m :: Type) Source # | Since: 0.2.0.0 |
type Rep (LessThan n) Source # | |
data GreaterThan (n :: Nat) Source #
A Predicate
ensuring that the value is greater than the
specified type-level number.
>>>
isRight (refine @(GreaterThan 65) @Int 67)
True
>>>
isLeft (refine @(GreaterThan 65) @Int 65)
True
Since: 0.1.0.0
GreaterThan | Since: 0.4.2 |
Instances
Generic (GreaterThan n) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (GreaterThan n) :: Type -> Type # from :: GreaterThan n -> Rep (GreaterThan n) x # to :: Rep (GreaterThan n) x -> GreaterThan n # | |
(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n :: Type) x Source # | Since: 0.1.0.0 |
Defined in Refined validate :: Proxy (GreaterThan n) -> x -> Maybe RefineException Source # | |
m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source # | Since: 0.2.0.0 |
m <= n => Weaken (GreaterThan n :: Type) (GreaterThan m :: Type) Source # | Since: 0.2.0.0 |
Defined in Refined weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x Source # | |
type Rep (GreaterThan n) Source # | |
A Predicate
ensuring that the value is greater than or equal to the
specified type-level number.
>>>
isRight (refine @(From 9) @Int 10)
True
>>>
isRight (refine @(From 10) @Int 10)
True
>>>
isLeft (refine @(From 11) @Int 10)
True
Since: 0.1.2
From | Since: 0.4.2 |
Instances
Generic (From n) Source # | Since: 0.3.0.0 |
(Ord x, Num x, KnownNat n) => Predicate (From n :: Type) x Source # | Since: 0.1.2 |
m <= n => Weaken (From n :: Type) (From m :: Type) Source # | Since: 0.2.0.0 |
m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source # | Since: 0.2.0.0 |
p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source # | Since: 0.2.0.0 |
type Rep (From n) Source # | |
A Predicate
ensuring that the value is less than or equal to the
specified type-level number.
>>>
isRight (refine @(To 23) @Int 17)
True
>>>
isLeft (refine @(To 17) @Int 23)
True
Since: 0.1.2
To | Since: 0.4.2 |
Instances
Generic (To n) Source # | Since: 0.3.0.0 |
(Ord x, Num x, KnownNat n) => Predicate (To n :: Type) x Source # | Since: 0.1.2 |
n <= m => Weaken (To n :: Type) (To m :: Type) Source # | Since: 0.2.0.0 |
n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source # | Since: 0.2.0.0 |
m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source # | Since: 0.2.0.0 |
type Rep (To n) Source # | |
data FromTo (mn :: Nat) (mx :: Nat) Source #
A Predicate
ensuring that the value is within an inclusive range.
>>>
isRight (refine @(FromTo 0 16) @Int 13)
True
>>>
isRight (refine @(FromTo 13 15) @Int 13)
True
>>>
isRight (refine @(FromTo 13 15) @Int 15)
True
>>>
isLeft (refine @(FromTo 13 15) @Int 12)
True
Since: 0.1.2
FromTo | Since: 0.4.2 |
Instances
m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source # | Since: 0.2.0.0 |
p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source # | Since: 0.2.0.0 |
(p <= n, m <= q) => Weaken (FromTo n m :: Type) (FromTo p q :: Type) Source # | Since: 0.2.0.0 |
(Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx :: Type) x Source # | Since: 0.1.2 |
Generic (FromTo mn mx) Source # | Since: 0.3.0.0 |
type Rep (FromTo mn mx) Source # | |
data NegativeFromTo (n :: Nat) (m :: Nat) Source #
A Predicate
ensuring that the value is greater or equal than a negative
number specified as a type-level (positive) number n
and less than a
type-level (positive) number m
.
>>>
isRight (refine @(NegativeFromTo 5 12) @Int (-3))
True
>>>
isLeft (refine @(NegativeFromTo 4 3) @Int (-5))
True
Since: 0.4
NegativeFromTo | Since: 0.4.2 |
Instances
(Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m :: Type) x Source # | Since: 0.4 |
Defined in Refined validate :: Proxy (NegativeFromTo n m) -> x -> Maybe RefineException Source # | |
Generic (NegativeFromTo n m) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (NegativeFromTo n m) :: Type -> Type # from :: NegativeFromTo n m -> Rep (NegativeFromTo n m) x # to :: Rep (NegativeFromTo n m) x -> NegativeFromTo n m # | |
type Rep (NegativeFromTo n m) Source # | |
data EqualTo (n :: Nat) Source #
A Predicate
ensuring that the value is equal to the specified
type-level number n
.
>>>
isRight (refine @(EqualTo 5) @Int 5)
True
>>>
isLeft (refine @(EqualTo 6) @Int 5)
True
Since: 0.1.0.0
EqualTo | Since: 0.4.2 |
data NotEqualTo (n :: Nat) Source #
A Predicate
ensuring that the value is not equal to the specified
type-level number n
.
>>>
isRight (refine @(NotEqualTo 6) @Int 5)
True
>>>
isLeft (refine @(NotEqualTo 5) @Int 5)
True
Since: 0.2.0.0
NotEqualTo | Since: 0.4.2 |
Instances
Generic (NotEqualTo n) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (NotEqualTo n) :: Type -> Type # from :: NotEqualTo n -> Rep (NotEqualTo n) x # to :: Rep (NotEqualTo n) x -> NotEqualTo n # | |
(Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n :: Type) x Source # | Since: 0.2.0.0 |
Defined in Refined validate :: Proxy (NotEqualTo n) -> x -> Maybe RefineException Source # | |
type Rep (NotEqualTo n) Source # | |
A Predicate
ensuring that the value is odd.
>>>
isRight (refine @Odd @Int 33)
True
>>>
isLeft (refine @Odd @Int 32)
True
Since: 0.4.2
Odd | Since: 0.4.2 |
A Predicate
ensuring that the value is even.
>>>
isRight (refine @Even @Int 32)
True
>>>
isLeft (refine @Even @Int 33)
True
Since: 0.4.2
Even | Since: 0.4.2 |
data DivisibleBy (n :: Nat) Source #
A Predicate
ensuring that the value is divisible by n
.
>>>
isRight (refine @(DivisibleBy 3) @Int 12)
True
>>>
isLeft (refine @(DivisibleBy 2) @Int 37)
True
Since: 0.4.2
DivisibleBy | Since: 0.4.2 |
Instances
Generic (DivisibleBy n) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (DivisibleBy n) :: Type -> Type # from :: DivisibleBy n -> Rep (DivisibleBy n) x # to :: Rep (DivisibleBy n) x -> DivisibleBy n # | |
(Integral x, KnownNat n) => Predicate (DivisibleBy n :: Type) x Source # | Since: 0.4.2 |
Defined in Refined validate :: Proxy (DivisibleBy n) -> x -> Maybe RefineException Source # | |
type Rep (DivisibleBy n) Source # | |
A Predicate
ensuring that the value is IEEE "not-a-number" (NaN).
>>>
isRight (refine @NaN @Double (0/0))
True
>>>
isLeft (refine @NaN @Double 13.9)
True
Since: 0.5
NaN | Since: 0.5 |
A Predicate
ensuring that the value is IEEE infinity or negative infinity.
>>>
isRight (refine @Infinite @Double (1/0))
True
>>>
isRight (refine @Infinite @Double (-1/0))
True
>>>
isLeft (refine @Infinite @Double 13.20)
True
Since: 0.5
Infinite | Since: 0.5 |
type Positive = GreaterThan 0 Source #
A Predicate
ensuring that the value is greater than zero.
Since: 0.1.0.0
type NonPositive = To 0 Source #
A Predicate
ensuring that the value is less than or equal to zero.
Since: 0.1.2
type Negative = LessThan 0 Source #
A Predicate
ensuring that the value is less than zero.
Since: 0.1.0.0
type NonNegative = From 0 Source #
A Predicate
ensuring that the value is greater than or equal to zero.
Since: 0.1.2
type NonZero = NotEqualTo 0 Source #
A Predicate
ensuring that the value is not equal to zero.
Since: 0.2.0.0
Foldable predicates
Size predicates
data SizeLessThan (n :: Nat) Source #
A Predicate
ensuring that the value has a length
which is less than the specified type-level number.
>>>
isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
True
>>>
isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
True
>>>
isRight (refine @(SizeLessThan 4) @Text "Hi")
True
>>>
isLeft (refine @(SizeLessThan 4) @Text "Hello")
True
Since: 0.2.0.0
SizeLessThan | Since: 0.4.2 |
Instances
Generic (SizeLessThan n) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (SizeLessThan n) :: Type -> Type # from :: SizeLessThan n -> Rep (SizeLessThan n) x # to :: Rep (SizeLessThan n) x -> SizeLessThan n # | |
KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException Source # | |
KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException Source # | |
KnownNat n => Predicate (SizeLessThan n :: Type) Text Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeLessThan n) -> Text -> Maybe RefineException Source # | |
(Foldable t, KnownNat n) => Predicate (SizeLessThan n :: Type) (t a) Source # | Since: 0.2.0.0 |
Defined in Refined validate :: Proxy (SizeLessThan n) -> t a -> Maybe RefineException Source # | |
type Rep (SizeLessThan n) Source # | |
data SizeGreaterThan (n :: Nat) Source #
A Predicate
ensuring that the value has a length
which is greater than the specified type-level number.
>>>
isLeft (refine @(SizeGreaterThan 3) @[Int] [1,2,3])
True
>>>
isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
True
>>>
isLeft (refine @(SizeGreaterThan 4) @Text "Hi")
True
>>>
isRight (refine @(SizeGreaterThan 4) @Text "Hello")
True
Since: 0.2.0.0
SizeGreaterThan | Since: 0.4.2 |
Instances
data SizeEqualTo (n :: Nat) Source #
A Predicate
ensuring that the value has a length
which is equal to the specified type-level number.
>>>
isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
True
>>>
isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
True
>>>
isRight (refine @(SizeEqualTo 4) @Text "four")
True
>>>
isLeft (refine @(SizeEqualTo 35) @Text "four")
True
Since: 0.2.0.0
SizeEqualTo | Since: 0.4.2 |
Instances
Generic (SizeEqualTo n) Source # | Since: 0.3.0.0 |
Defined in Refined type Rep (SizeEqualTo n) :: Type -> Type # from :: SizeEqualTo n -> Rep (SizeEqualTo n) x # to :: Rep (SizeEqualTo n) x -> SizeEqualTo n # | |
KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException Source # | |
KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException Source # | |
KnownNat n => Predicate (SizeEqualTo n :: Type) Text Source # | Since: 0.5 |
Defined in Refined validate :: Proxy (SizeEqualTo n) -> Text -> Maybe RefineException Source # | |
(Foldable t, KnownNat n) => Predicate (SizeEqualTo n :: Type) (t a) Source # | Since: 0.2.0.0 |
Defined in Refined validate :: Proxy (SizeEqualTo n) -> t a -> Maybe RefineException Source # | |
type Rep (SizeEqualTo n) Source # | |
type Empty = SizeEqualTo 0 Source #
A Predicate
ensuring that the type is empty.
Since: 0.5
type NonEmpty = SizeGreaterThan 0 Source #
A Predicate
ensuring that the type is non-empty.
Since: 0.2.0.0
Ordering predicates
A Predicate
ensuring that the Foldable
contains elements
in a strictly ascending order.
>>>
isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
True
>>>
isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
True
Since: 0.2.0.0
Ascending | Since: 0.4.2 |
data Descending Source #
A Predicate
ensuring that the Foldable
contains elements
in a strictly descending order.
>>>
isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
True
>>>
isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
True
Since: 0.2.0.0
Descending | Since: 0.4.2 |
Instances
Generic Descending Source # | Since: 0.3.0.0 |
Defined in Refined type Rep Descending :: Type -> Type # from :: Descending -> Rep Descending x # to :: Rep Descending x -> Descending # | |
(Foldable t, Ord a) => Predicate Descending (t a) Source # | Since: 0.2.0.0 |
Defined in Refined validate :: Proxy Descending -> t a -> Maybe RefineException Source # | |
type Rep Descending Source # | |
Weakening
class Weaken from to where Source #
A typeclass containing "safe" conversions between refined predicates where the target is weaker than the source: that is, all values that satisfy the first predicate will be guaranteed to satisfy the second.
Take care: writing an instance declaration for your custom
predicates is the same as an assertion that weaken
is
safe to use:
instance Weaken
Pred1 Pred2
For most of the instances, explicit type annotations for the result value's type might be required.
Since: 0.2.0.0
Nothing
Instances
n <= m => Weaken (To n :: Type) (To m :: Type) Source # | Since: 0.2.0.0 |
m <= n => Weaken (From n :: Type) (From m :: Type) Source # | Since: 0.2.0.0 |
m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source # | Since: 0.2.0.0 |
m <= n => Weaken (GreaterThan n :: Type) (GreaterThan m :: Type) Source # | Since: 0.2.0.0 |
Defined in Refined weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x Source # | |
n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source # | Since: 0.2.0.0 |
n <= m => Weaken (LessThan n :: Type) (LessThan m :: Type) Source # | Since: 0.2.0.0 |
m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source # | Since: 0.2.0.0 |
p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source # | Since: 0.2.0.0 |
(p <= n, m <= q) => Weaken (FromTo n m :: Type) (FromTo p q :: Type) Source # | Since: 0.2.0.0 |
andLeft :: Refined (And l r) x -> Refined l x Source #
This function helps type inference. It is equivalent to the following:
instance Weaken (And l r) l
Since: 0.2.0.0
andRight :: Refined (And l r) x -> Refined r x Source #
This function helps type inference. It is equivalent to the following:
instance Weaken (And l r) r
Since: 0.2.0.0
leftOr :: Refined l x -> Refined (Or l r) x Source #
This function helps type inference. It is equivalent to the following:
instance Weaken l (Or l r)
Since: 0.2.0.0
rightOr :: Refined r x -> Refined (Or l r) x Source #
This function helps type inference. It is equivalent to the following:
instance Weaken r (Or l r)
Since: 0.2.0.0
Strengthening
strengthen :: forall p p' x. (Predicate p x, Predicate p' x) => Refined p x -> Either RefineException (Refined (p && p') x) Source #
Strengthen a refinement by composing it with another.
Since: 0.4.2.2
Error handling
RefineException
data RefineException Source #
An exception encoding the way in which a Predicate
failed.
Since: 0.2.0.0
RefineNotException !TypeRep | A Since: 0.2.0.0 |
RefineAndException !TypeRep !(These RefineException RefineException) | A Since: 0.2.0.0 |
RefineOrException !TypeRep !RefineException !RefineException | A Since: 0.2.0.0 |
RefineXorException !TypeRep !(Maybe (RefineException, RefineException)) | A Since: 0.5 |
RefineSomeException !TypeRep !SomeException | A Since: 0.5 |
RefineOtherException !TypeRep !Text | A Since: 0.2.0.0 |
Instances
displayRefineException :: RefineException -> String Source #
Display a RefineException
as String
This function can be extremely useful for debugging
, especially deeply nested ones.RefineException
s
Consider:
myRefinement = refine @(And (Not (LessThan 5)) (Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3) ) ) ) @Int 3
This function will show the following tree structure, recursively breaking down every issue:
And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3))) ├── The predicate (Not (LessThan 5)) does not hold. └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3)) ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10 └── And (EqualTo 4) (EqualTo 3) └── The predicate (EqualTo 4) failed with the message: Value does not equal 4
Note: Equivalent to show
@RefineException
Since: 0.2.0.0
validate
helpers
throwRefineOtherException Source #
:: TypeRep | The |
-> Text | A |
-> Maybe RefineException |
A handler for a
.RefineException
throwRefineOtherException
is useful for defining what
behaviour validate
should have in the event of a predicate failure.
Typically the first argument passed to this function
will be the result of applying typeRep
to the first
argument of validate
.
Since: 0.2.0.0
throwRefineSomeException Source #
:: TypeRep | The |
-> SomeException | A custom exception. |
-> Maybe RefineException |
A handler for a
.RefineException
throwRefineSomeException
is useful for defining what
behaviour validate
should have in the event of a predicate failure
with a specific exception.
Since: 0.5
Orphan instances
(Read x, Predicate p x) => Read (Refined p x) Source # | This instance makes sure to check the refinement. Since: 0.1.0.0 |
(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) Source # | Since: 0.4 |
(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source # | Since: 0.4 |
(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source # | Since: 0.6.3 |
toJSONKey :: ToJSONKeyFunction (Refined p a) # toJSONKeyList :: ToJSONKeyFunction [Refined p a] # | |
(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source # | Since: 0.4 |
(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # | |
fromJSONKey :: FromJSONKeyFunction (Refined p a) # fromJSONKeyList :: FromJSONKeyFunction [Refined p a] # |