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 typeclass which defines a runtime interpretation of a type-level predicate p for type x.

Since: 0.1.0.0

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

Since: 0.4.2.3

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

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

Display a RefineException as String

This function can be extremely useful for debugging RefineExceptions, especially deeply nested ones.

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

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

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

An implementation of validate that always succeeds.

Examples

  data ContainsLetterE = ContainsLetterE

  instance Predicate ContainsLetterE Text where
    validate p t
      | any (== 'e') t = success
      | otherwise = Just $ throwRefineException (typeRep p) "Text doesn't contain letter 'e'".
  

Since: 0.5