A refinement type, which wraps a value of type x, ensuring that it satisfies a type-level predicate p.

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

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.

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

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

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

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

If it's not evident, 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.

It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/

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

Extracts the refined value.

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

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

The negation of a predicate.

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

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

The conjunction of two predicates.

>>> isLeft (refine @(And Positive Negative) @Int 3)
True

>>> isRight (refine @(And Positive Odd) @Int 203)
True

The conjunction of two predicates.

The disjunction of two predicates.

>>> isRight (refine @(Or Even Odd) @Int 3)
True

>>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
True

The disjunction of two predicates.

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

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

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

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

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

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

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

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

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

A Predicate ensuring that the value is odd.

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

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

A Predicate ensuring that the value is even.

>>> isRight (refine @Even @Int 32)
True

>>> isLeft (refine @Even @Int 33)
True

A Predicate ensuring that the value is divisible by n.

>>> isRight (refine @(DivisibleBy 3) @Int 12)
True

>>> isLeft (refine @(DivisibleBy 2) @Int 37)
True

A Predicate ensuring that the value is greater than zero.

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

A Predicate ensuring that the value is less than zero.

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

An inclusive range of values from zero to one.

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

A Predicate ensuring that the Foldable 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

A Predicate ensuring that the Foldable 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

A Predicate ensuring that the Foldable 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

A Predicate ensuring that the Foldable is non-empty.

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

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

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 guarunteed to satisy 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.

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

instance Weaken (And l r) l

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

instance Weaken (And l r) r

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

instance Weaken l (Or l r)

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

instance Weaken r (Or l r)

Strengthen a refinement by composing it with another.

Strengthen a refinement by composing it with another inside of the RefineT monad.

An exception encoding the way in which a Predicate failed.

Display a RefineException as a Doc ann

A monad transformer that adds RefineExceptions to other monads.

The pure and return functions yield computations that produce the given value, while >>= sequences two subcomputations, exiting on the first RefineException.

The inverse of RefineT.

Constructor for computations in the RefineT movie. (The inverse of runRefineT).

Map the unwrapped computation using the given function.

runRefineT (mapRefineT f m) = f (runRefineT m)

RefineM a is equivalent to RefineT Identity a for any type a.

Constructs a computation in the RefineM monad. (The inverse of runRefineM).

Run a monadic action of type RefineM a, yielding an Either RefineException a.

This is just defined as runIdentity . runRefineT.

One can use throwRefine inside of a monadic context to begin processing a RefineException.

A handler function to handle previous RefineExceptions and return to normal execution. A common idiom is:

 do { action1; action2; action3 } `catchRefine' handler

where the action functions can call throwRefine. Note that handler and the do-block must have the same return type.

A handler for a RefineException.

throwRefineOtherException is useful for defining what behaviour validate should have in the event of a predicate failure.

>>> pretty 1 <+> pretty "hello" <+> pretty 1.234
1 hello 1.234