HORIZON HASKELLDocslts/ghc-10.0.x8fef28d2026-11-02Search packagesCtrl K
Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8fef28d · 2026-11-02

Modulerefined-0.8.2Haskell2010

Refined

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/

Contents
  1. Refined type
  2. Creation
  3. Consumption
  4. Predicate
  5. Logical predicates
  6. Identity predicate
  7. Numeric predicates
  8. Foldable predicates
  9. Size predicates
  10. Ordering predicates
  11. Weakening
  12. Strengthening
  13. Error handling
  14. RefineException
  15. validate helpers
Synopsis
  • Packagerefined-0.8.2
  • Exports60
  • LanguageHaskell2010
  • LicenceMIT
  • SourceRefined.hs

Refined type

newtypenewtype Refined (p :: k) x
Source#

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

Instances13Lift, Foldable, Eq, Ord, Read, Show, …

Creation

valuerefineTH
  1. :: (Predicate p x, Lift x, Quote m, MonadFail m)
  2. => x
  3. -> Code m (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.

Consumption

Predicate

classclass Typeable p => Predicate (p :: k) x where
Source#

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

Methods

  • validate :: Proxy p -> x -> Maybe RefineException

    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.

Instances32Predicate, …

Logical predicates

datadata Not (p :: k)
Source#

The negation of a predicate.

Example1 expression
isRight (refine @(Not NonEmpty) @[Int] [])True
Example1 expression
isLeft (refine @(Not NonEmpty) @[Int] [1,2])True

Constructors

Instances5Generic1, Predicate, Generic, Rep, Rep1
datadata And (l :: k) (r :: k1)
Source#

The conjunction of two predicates.

Example1 expression
isLeft (refine @(And Positive Negative) @Int 3)True
Example1 expression
isRight (refine @(And Positive Odd) @Int 203)True

Constructors

Instances5Generic1, Predicate, Generic, Rep, Rep1
typetype (&&) = And
Source#

The conjunction of two predicates.

datadata Or (l :: k) (r :: k1)
Source#

The disjunction of two predicates.

Example1 expression
isRight (refine @(Or Even Odd) @Int 3)True
Example1 expression
isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)True
Example1 expression
isRight (refine @(Or Even Even) @Int 4)True

Constructors

Instances5Generic1, Predicate, Generic, Rep, Rep1
typetype (||) = Or
Source#

The disjunction of two predicates.

datadata Xor (l :: k) (r :: k1)
Source#

The exclusive disjunction of two predicates.

Example1 expression
isRight (refine @(Xor Even Odd) @Int 3)True
Example1 expression
isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)True
Example1 expression
isLeft (refine @(Xor Even Even) @Int 2)True

Constructors

Instances5Generic1, Predicate, Generic, Rep, Rep1

Identity predicate

datadata IdPred
Source#

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

Example1 expression
isRight (refine @IdPred @Int undefined)True
Example1 expression
isLeft (refine @IdPred @Int undefined)False

Constructors

Instances3Generic, Predicate, Rep

Numeric predicates

datadata LessThan (n :: Nat)
Source#

A Predicate ensuring that the value is less than the specified type-level number.

Example1 expression
isRight (refine @(LessThan 12) @Int 11)True
Example1 expression
isLeft (refine @(LessThan 12) @Int 12)True

Constructors

Instances5Weaken, Predicate, Generic, Rep
datadata GreaterThan (n :: Nat)
Source#

A Predicate ensuring that the value is greater than the specified type-level number.

Example1 expression
isRight (refine @(GreaterThan 65) @Int 67)True
Example1 expression
isLeft (refine @(GreaterThan 65) @Int 65)True

Constructors

Instances5Weaken, Predicate, Generic, Rep
datadata From (n :: Nat)
Source#

A Predicate ensuring that the value is greater than or equal to the specified type-level number.

Example1 expression
isRight (refine @(From 9) @Int 10)True
Example1 expression
isRight (refine @(From 10) @Int 10)True
Example1 expression
isLeft (refine @(From 11) @Int 10)True

Constructors

Instances6Weaken, Predicate, Generic, Rep
datadata To (n :: Nat)
Source#

A Predicate ensuring that the value is less than or equal to the specified type-level number.

Example1 expression
isRight (refine @(To 23) @Int 17)True
Example1 expression
isLeft (refine @(To 17) @Int 23)True

Constructors

Instances6Weaken, Predicate, Generic, Rep
datadata FromTo (mn :: Nat) (mx :: Nat)
Source#

A Predicate ensuring that the value is within an inclusive range.

Example1 expression
isRight (refine @(FromTo 0 16) @Int 13)True
Example1 expression
isRight (refine @(FromTo 13 15) @Int 13)True
Example1 expression
isRight (refine @(FromTo 13 15) @Int 15)True
Example1 expression
isLeft (refine @(FromTo 13 15) @Int 12)True

Constructors

Instances6Weaken, Predicate, Generic, Rep
datadata 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.

Example1 expression
isRight (refine @(NegativeFromTo 5 12) @Int (-3))True
Example1 expression
isLeft (refine @(NegativeFromTo 4 3) @Int (-5))True

Constructors

Instances3Predicate, Generic, Rep
datadata EqualTo (n :: Nat)
Source#

A Predicate ensuring that the value is equal to the specified type-level number n.

Example1 expression
isRight (refine @(EqualTo 5) @Int 5)True
Example1 expression
isLeft (refine @(EqualTo 6) @Int 5)True

Constructors

Instances3Predicate, Generic, Rep
datadata NotEqualTo (n :: Nat)
Source#

A Predicate ensuring that the value is not equal to the specified type-level number n.

Example1 expression
isRight (refine @(NotEqualTo 6) @Int 5)True
Example1 expression
isLeft (refine @(NotEqualTo 5) @Int 5)True

Constructors

Instances3Predicate, Generic, Rep
datadata Odd
Source#

A Predicate ensuring that the value is odd.

Example1 expression
isRight (refine @Odd @Int 33)True
Example1 expression
isLeft (refine @Odd @Int 32)True

Constructors

Instances3Generic, Predicate, Rep
datadata Even
Source#

A Predicate ensuring that the value is even.

Example1 expression
isRight (refine @Even @Int 32)True
Example1 expression
isLeft (refine @Even @Int 33)True

Constructors

Instances3Generic, Predicate, Rep
datadata DivisibleBy (n :: Nat)
Source#

A Predicate ensuring that the value is divisible by n.

Example1 expression
isRight (refine @(DivisibleBy 3) @Int 12)True
Example1 expression
isLeft (refine @(DivisibleBy 2) @Int 37)True

Constructors

Instances3Predicate, Generic, Rep
datadata NaN
Source#

A Predicate ensuring that the value is IEEE "not-a-number" (NaN).

Example1 expression
isRight (refine @NaN @Double (0/0))True
Example1 expression
isLeft (refine @NaN @Double 13.9)True

Constructors

Instances3Generic, Predicate, Rep
datadata Infinite
Source#

A Predicate ensuring that the value is IEEE infinity or negative infinity.

Example1 expression
isRight (refine @Infinite @Double (1/0))True
Example1 expression
isRight (refine @Infinite @Double (-1/0))True
Example1 expression
isLeft (refine @Infinite @Double 13.20)True

Constructors

Instances3Generic, Predicate, Rep

Foldable predicates

Size predicates

datadata SizeLessThan (n :: Nat)
Source#

A Predicate ensuring that the value has a length which is less than the specified type-level number.

Example1 expression
isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])True
Example1 expression
isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])True
Example1 expression
isRight (refine @(SizeLessThan 4) @Text "Hi")True
Example1 expression
isLeft (refine @(SizeLessThan 4) @Text "Hello")True

Constructors

Instances7Weaken, Predicate, Generic, Rep, …
datadata SizeGreaterThan (n :: Nat)
Source#

A Predicate ensuring that the value has a length which is greater than the specified type-level number.

Example1 expression
isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])True
Example1 expression
isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])True
Example1 expression
isLeft (refine @(SizeGreaterThan 4) @Text "Hi")True
Example1 expression
isRight (refine @(SizeGreaterThan 4) @Text "Hello")True

Constructors

Instances7Weaken, Predicate, Generic, Rep, …
datadata SizeEqualTo (n :: Nat)
Source#

A Predicate ensuring that the value has a length which is equal to the specified type-level number.

Example1 expression
isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])True
Example1 expression
isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])True
Example1 expression
isRight (refine @(SizeEqualTo 4) @Text "four")True
Example1 expression
isLeft (refine @(SizeEqualTo 35) @Text "four")True

Constructors

Instances6Predicate, Generic, Rep

Ordering predicates

datadata Ascending
Source#

A Predicate ensuring that the Foldable contains elements in a strictly ascending order.

Example1 expression
isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])True
Example1 expression
isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])True

Constructors

Instances3Generic, Predicate, Rep
datadata Descending
Source#

A Predicate ensuring that the Foldable contains elements in a strictly descending order.

Example1 expression
isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])True
Example1 expression
isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])True

Constructors

Instances3Generic, Predicate, Rep

Weakening

classclass Weaken (from :: k) (to :: k1) 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.

Methods

Instances11Weaken, …
valueandLeft :: 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
valueandRight :: 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
valueleftOr :: 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)
valuerightOr :: 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)

Strengthening

Error handling

RefineException

datadata RefineException
Source#

An exception encoding the way in which a Predicate failed.

Constructors

Instances4Show, Generic, Exception, Rep
valuedisplayRefineException :: RefineException -> String
Source#

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

validate helpers

valuethrowRefineOtherException
  1. :: TypeRep

    The TypeRep of the Predicate. This can usually be given by using typeRep.

  2. -> Text

    A PP.Doc Void encoding a custom error message to be pretty-printed.

  3. -> Maybe RefineException
Source#

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.

valuesuccess :: Maybe RefineException
Source#

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'".

Orphan instances

6 instances