A refinement type, which wraps a value of type x.

Since: 0.1.0.0

A smart constructor of a Refined value. Checks the input value at runtime.

Since: 0.1.0.0

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

Constructs a Refined value at run-time, calling throwM if the value does not satisfy the predicate.

Since: 0.2.0.0

Constructs a Refined value at run-time, calling fail if the value does not satisfy the predicate.

Since: 0.2.0.0

Constructs a Refined value at run-time, calling throwError if the value does not satisfy the predicate.

Since: 0.2.0.0

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

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

Like refineTH, but immediately unrefines the value. This is useful when some value need only be refined at compile-time.

Since: 0.4.4

Extracts the refined value.

Since: 0.1.0.0

A refinement type, which wraps a value of type f x.

The predicate is applied over the functor f. Thus, we may safely recover various Functory instances, because no matter what you do to the values inside the functor, the predicate may not be invalidated.

A smart constructor of a Refined1 value. Checks the input value at runtime.

Since: 0.1.0.0

Extracts the refined value.

A typeclass which defines a runtime interpretation of a type-level predicate p for type x.

Since: 0.1.0.0

Check the value x according to the predicate p, producing an error RefineException if the value does not satisfy.

Same as validate but with more convenient type variable order for a better TypeApplications experience.

Reify a Predicate by turning it into a value-level predicate.

Since: 0.4.2.3

A typeclass which defines a runtime interpretation of a type-level predicate p for type forall a. f a.

The inner type may not be inspected. If you find yourself needing to add constraints to it, you want Predicate.

Check the value f a according to the predicate p, producing an error RefineException if the value does not satisfy.

Same as validate1 but with more convenient type variable order for a better TypeApplications experience.

The negation of a predicate.

>>> isRight (refine @(Not NonEmpty) @[Int] [])
True

>>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])
True

Since: 0.1.0.0

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

The conjunction of two predicates.

Since: 0.2.0.0

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

The disjunction of two predicates.

Since: 0.2.0.0

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

A predicate which is satisfied for all types. Arguments passed to validate in validate IdPred x are not evaluated.

>>> isRight (refine @IdPred @Int undefined)
True

>>> isLeft (refine @IdPred @Int undefined)
False

Since: 0.3.0.0

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

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

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

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

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

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

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

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

A Predicate ensuring that the value is odd.

>>> isRight (refine @Odd @Int 33)
True

>>> isLeft (refine @Odd @Int 32)
True

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

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

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

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

A Predicate ensuring that the value is greater than zero.

Since: 0.1.0.0

A Predicate ensuring that the value is less than or equal to zero.

Since: 0.1.2

A Predicate ensuring that the value is less than zero.

Since: 0.1.0.0

A Predicate ensuring that the value is greater than or equal to zero.

Since: 0.1.2

An inclusive range of values from zero to one.

Since: 0.1.0.0

A Predicate ensuring that the value is not equal to zero.

Since: 0.2.0.0

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

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

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

A Predicate ensuring that the type is empty.

Since: 0.5

A Predicate ensuring that the type is non-empty.

Since: 0.2.0.0

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

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

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

This function helps type inference. It is equivalent to the following:

instance Weaken (And l r) l

Since: 0.2.0.0

This function helps type inference. It is equivalent to the following:

instance Weaken (And l r) r

Since: 0.2.0.0

This function helps type inference. It is equivalent to the following:

instance Weaken l (Or l r)

Since: 0.2.0.0

This function helps type inference. It is equivalent to the following:

instance Weaken r (Or l r)

Since: 0.2.0.0

This function helps type inference. It is equivalent to the following:

instance Weaken from to => Weaken (And from x) (And to x)

Since: 0.8.1.0

This function helps type inference. It is equivalent to the following:

instance Weaken from to => Weaken (And x from) (And x to)

Since: 0.8.1.0

This function helps type inference. It is equivalent to the following:

instance Weaken from to => Weaken (Or from x) (Or to x)

Since: 0.8.1.0

This function helps type inference. It is equivalent to the following:

instance Weaken from to => Weaken (Or x from) (Or x to)

Since: 0.8.1.0

Strengthen a refinement by composing it with another.

Since: 0.4.2.2

An exception encoding the way in which a Predicate failed.

Since: 0.2.0.0