HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

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/

  • 35 types
  • 2 classes
  • 23 values
  • Packagerefined-0.8.2
  • Exports60
  • LanguageHaskell2010
  • LicenceMIT
  • SourceRefined.hs

Refined type

1 declaration
newtypenewtype Refined (p :: k) x
#

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

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

Creation

valuerefineEither
  1. :: Predicate p x
  2. => x
  3. -> Either (Refined (Not p) x) (Refined p x)
#

Like refine, but, when the value doesn't satisfy the predicate, returns a Refined value with the predicate negated, instead of returning RefineException.

Example1 expression
isRight (refineEither @Even @Int 42)True
Example1 expression
isLeft (refineEither @Even @Int 43)True
valuerefineTH
  1. :: (Predicate p x, Lift x, Quote m, MonadFail m)
  2. => x
  3. -> Code m (Refined p x)
#

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

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

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

6 declarations
datadata Not (p :: k)
#

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)
#

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
#

The conjunction of two predicates.

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

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
#

The disjunction of two predicates.

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

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

1 declaration
datadata IdPred
#

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

19 declarations
datadata LessThan (n :: Nat)
#

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)
#

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)
#

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)
#

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)
#

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)
#

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)
#

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)
#

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
#

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
#

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)
#

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
#

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
#

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
typetype ZeroToOne = FromTo 0 1
#

An inclusive range of values from zero to one.

Foldable predicates

0 declarations

Size predicates

datadata SizeLessThan (n :: Nat)
#

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)
#

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)
#

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
#

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
#

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

9 declarations
classclass Weaken (from :: k) (to :: k1) where
#

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
#

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
#

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
#

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
#

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

instance Weaken r (Or l r)
valueweakenAndLeft
  1. :: Weaken from to
  2. => Refined (And from x) a
  3. -> Refined (And to x) a
#

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

instance Weaken from to => Weaken (And from x) (And to x)
valueweakenAndRight
  1. :: Weaken from to
  2. => Refined (And x from) a
  3. -> Refined (And x to) a
#

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

instance Weaken from to => Weaken (And x from) (And x to)
valueweakenOrLeft
  1. :: Weaken from to
  2. => Refined (And from x) a
  3. -> Refined (And to x) a
#

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

instance Weaken from to => Weaken (Or from x) (Or to x)
valueweakenOrRight
  1. :: Weaken from to
  2. => Refined (And x from) a
  3. -> Refined (And x to) a
#

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

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

Strengthening

1 declaration

Error handling

0 declarations

RefineException

datadata RefineException
#

An exception encoding the way in which a Predicate failed.

Constructors

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

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

valuesuccess :: Maybe RefineException
#

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