refined-0.8.1: Refinement types with static and runtime checking
Safe HaskellSafe-Inferred
LanguageHaskell2010

Refined

Description

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/

Synopsis

Refined type

data Refined (p :: k) x Source #

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

Since: 0.1.0.0

Instances

Instances details
Lift x => Lift (Refined p x :: Type) Source #

Since: 0.1.0.0

Instance details

Defined in Refined.Unsafe.Type

Methods

lift :: Quote m => Refined p x -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Refined p x -> Code m (Refined p x) #

Foldable (Refined p) Source #

Since: 0.2

Instance details

Defined in Refined.Unsafe.Type

Methods

fold :: Monoid m => Refined p m -> m #

foldMap :: Monoid m => (a -> m) -> Refined p a -> m #

foldMap' :: Monoid m => (a -> m) -> Refined p a -> m #

foldr :: (a -> b -> b) -> b -> Refined p a -> b #

foldr' :: (a -> b -> b) -> b -> Refined p a -> b #

foldl :: (b -> a -> b) -> b -> Refined p a -> b #

foldl' :: (b -> a -> b) -> b -> Refined p a -> b #

foldr1 :: (a -> a -> a) -> Refined p a -> a #

foldl1 :: (a -> a -> a) -> Refined p a -> a #

toList :: Refined p a -> [a] #

null :: Refined p a -> Bool #

length :: Refined p a -> Int #

elem :: Eq a => a -> Refined p a -> Bool #

maximum :: Ord a => Refined p a -> a #

minimum :: Ord a => Refined p a -> a #

sum :: Num a => Refined p a -> a #

product :: Num a => Refined p a -> a #

(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) Source #

Since: 0.4

Instance details

Defined in Refined

Methods

arbitrary :: Gen (Refined p a) #

shrink :: Refined p a -> [Refined p a] #

(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source #

Since: 0.4

Instance details

Defined in Refined

(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # 
Instance details

Defined in Refined

(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source #

Since: 0.4

Instance details

Defined in Refined

(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source #

Since: 0.6.3

Instance details

Defined in Refined

(Read x, Predicate p x) => Read (Refined p x) Source #

This instance makes sure to check the refinement.

Since: 0.1.0.0

Instance details

Defined in Refined

Show x => Show (Refined p x) Source #

Since: 0.1.0.0

Instance details

Defined in Refined.Unsafe.Type

Methods

showsPrec :: Int -> Refined p x -> ShowS #

show :: Refined p x -> String #

showList :: [Refined p x] -> ShowS #

NFData x => NFData (Refined p x) Source #

Since: 0.5

Instance details

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined p x -> () #

Eq x => Eq (Refined p x) Source #

Since: 0.1.0.0

Instance details

Defined in Refined.Unsafe.Type

Methods

(==) :: Refined p x -> Refined p x -> Bool #

(/=) :: Refined p x -> Refined p x -> Bool #

Ord x => Ord (Refined p x) Source #

Since: 0.1.0.0

Instance details

Defined in Refined.Unsafe.Type

Methods

compare :: Refined p x -> Refined p x -> Ordering #

(<) :: Refined p x -> Refined p x -> Bool #

(<=) :: Refined p x -> Refined p x -> Bool #

(>) :: Refined p x -> Refined p x -> Bool #

(>=) :: Refined p x -> Refined p x -> Bool #

max :: Refined p x -> Refined p x -> Refined p x #

min :: Refined p x -> Refined p x -> Refined p x #

Hashable x => Hashable (Refined p x) Source #

Since: 0.6.3

Instance details

Defined in Refined.Unsafe.Type

Methods

hashWithSalt :: Int -> Refined p x -> Int #

hash :: Refined p x -> Int #

Creation

refine :: forall p x. Predicate p x => x -> Either RefineException (Refined p x) Source #

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

Since: 0.1.0.0

refine_ :: forall p x. Predicate p x => x -> Either RefineException x Source #

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

refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) Source #

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

Since: 0.2.0.0

refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x) Source #

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

Since: 0.2.0.0

refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x) Source #

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

Since: 0.2.0.0

refineEither :: forall p x. Predicate p x => x -> Either (Refined (Not p) x) (Refined p x) Source #

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

refineTH :: forall p x m. (Predicate p x, Lift x, Quote m, MonadFail m) => x -> 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.

Since: 0.1.0.0

refineTH_ :: forall p x m. (Predicate p x, Lift x, Quote m, MonadFail m) => x -> Code m x Source #

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

Since: 0.4.4

Consumption

unrefine :: Refined p x -> x Source #

Extracts the refined value.

Since: 0.1.0.0

Predicate

class Typeable p => Predicate p x where Source #

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

Since: 0.1.0.0

Methods

validate :: Proxy p -> x -> Maybe RefineException Source #

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.

Instances

Instances details
Integral x => Predicate Even x Source #

Since: 0.4.2

Instance details

Defined in Refined

Predicate IdPred x Source #

Since: 0.3.0.0

Instance details

Defined in Refined

RealFloat x => Predicate Infinite x Source #

Since: 0.5

Instance details

Defined in Refined

RealFloat x => Predicate NaN x Source #

Since: 0.5

Instance details

Defined in Refined

Integral x => Predicate Odd x Source #

Since: 0.4.2

Instance details

Defined in Refined

(Foldable t, Ord a) => Predicate Ascending (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Foldable t, Ord a) => Predicate Descending (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Integral x, KnownNat n) => Predicate (DivisibleBy n :: Type) x Source #

Since: 0.4.2

Instance details

Defined in Refined

(Eq x, Num x, KnownNat n) => Predicate (EqualTo n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

(Ord x, Num x, KnownNat n) => Predicate (From n :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

(Ord x, Num x, KnownNat n) => Predicate (LessThan n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

(Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n :: Type) x Source #

Since: 0.2.0.0

Instance details

Defined in Refined

KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeEqualTo n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

(Ord x, Num x, KnownNat n) => Predicate (To n :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

Methods

validate :: Proxy (To n) -> x -> Maybe RefineException Source #

(Foldable t, KnownNat n) => Predicate (SizeEqualTo n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Foldable t, KnownNat n) => Predicate (SizeGreaterThan n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Foldable t, KnownNat n) => Predicate (SizeLessThan n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

Methods

validate :: Proxy (FromTo mn mx) -> x -> Maybe RefineException Source #

(Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m :: Type) x Source #

Since: 0.4

Instance details

Defined in Refined

(Predicate p x, Typeable p, Typeable k) => Predicate (Not p :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (And l r :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Methods

validate :: Proxy (And l r) -> x -> Maybe RefineException Source #

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (Or l r :: Type) x Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

validate :: Proxy (Or l r) -> x -> Maybe RefineException Source #

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (Xor l r :: Type) x Source #

Since: 0.5

Instance details

Defined in Refined

Methods

validate :: Proxy (Xor l r) -> x -> Maybe RefineException Source #

reifyPredicate :: forall p a. Predicate p a => a -> Bool Source #

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

Since: 0.4.2.3

Logical predicates

data Not p Source #

The negation of a predicate.

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

Since: 0.1.0.0

Constructors

Not

Since: 0.4.2

Instances

Instances details
Generic1 (Not :: k -> Type) Source # 
Instance details

Defined in Refined

Associated Types

type Rep1 Not :: k -> Type #

Methods

from1 :: forall (a :: k0). Not a -> Rep1 Not a #

to1 :: forall (a :: k0). Rep1 Not a -> Not a #

(Predicate p x, Typeable p, Typeable k) => Predicate (Not p :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Generic (Not p) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (Not p) :: Type -> Type #

Methods

from :: Not p -> Rep (Not p) x #

to :: Rep (Not p) x -> Not p #

type Rep1 (Not :: k -> Type) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep1 (Not :: k -> Type) = D1 ('MetaData "Not" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: k -> Type))
type Rep (Not p) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (Not p) = D1 ('MetaData "Not" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: Type -> Type))

data And l r Source #

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

Constructors

And

Since: 0.4.2

Instances

Instances details
Generic1 (And l :: k1 -> Type) Source # 
Instance details

Defined in Refined

Associated Types

type Rep1 (And l) :: k -> Type #

Methods

from1 :: forall (a :: k). And l a -> Rep1 (And l) a #

to1 :: forall (a :: k). Rep1 (And l) a -> And l a #

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (And l r :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Methods

validate :: Proxy (And l r) -> x -> Maybe RefineException Source #

Generic (And l r) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (And l r) :: Type -> Type #

Methods

from :: And l r -> Rep (And l r) x #

to :: Rep (And l r) x -> And l r #

type Rep1 (And l :: k1 -> Type) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep1 (And l :: k1 -> Type) = D1 ('MetaData "And" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: k1 -> Type))
type Rep (And l r) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (And l r) = D1 ('MetaData "And" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: Type -> Type))

type (&&) = And infixr 3 Source #

The conjunction of two predicates.

Since: 0.2.0.0

data Or l r Source #

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

Constructors

Or

Since: 0.4.2

Instances

Instances details
Generic1 (Or l :: k1 -> Type) Source # 
Instance details

Defined in Refined

Associated Types

type Rep1 (Or l) :: k -> Type #

Methods

from1 :: forall (a :: k). Or l a -> Rep1 (Or l) a #

to1 :: forall (a :: k). Rep1 (Or l) a -> Or l a #

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (Or l r :: Type) x Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

validate :: Proxy (Or l r) -> x -> Maybe RefineException Source #

Generic (Or l r) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (Or l r) :: Type -> Type #

Methods

from :: Or l r -> Rep (Or l r) x #

to :: Rep (Or l r) x -> Or l r #

type Rep1 (Or l :: k1 -> Type) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep1 (Or l :: k1 -> Type) = D1 ('MetaData "Or" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: k1 -> Type))
type Rep (Or l r) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (Or l r) = D1 ('MetaData "Or" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: Type -> Type))

type (||) = Or infixr 2 Source #

The disjunction of two predicates.

Since: 0.2.0.0

data Xor l r Source #

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

Constructors

Xor

Since: 0.5

Instances

Instances details
Generic1 (Xor l :: k1 -> Type) Source # 
Instance details

Defined in Refined

Associated Types

type Rep1 (Xor l) :: k -> Type #

Methods

from1 :: forall (a :: k). Xor l a -> Rep1 (Xor l) a #

to1 :: forall (a :: k). Rep1 (Xor l) a -> Xor l a #

(Predicate l x, Predicate r x, Typeable l, Typeable r, Typeable k) => Predicate (Xor l r :: Type) x Source #

Since: 0.5

Instance details

Defined in Refined

Methods

validate :: Proxy (Xor l r) -> x -> Maybe RefineException Source #

Generic (Xor l r) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (Xor l r) :: Type -> Type #

Methods

from :: Xor l r -> Rep (Xor l r) x #

to :: Rep (Xor l r) x -> Xor l r #

type Rep1 (Xor l :: k1 -> Type) Source #

Since: 0.5

Instance details

Defined in Refined

type Rep1 (Xor l :: k1 -> Type) = D1 ('MetaData "Xor" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Xor" 'PrefixI 'False) (U1 :: k1 -> Type))
type Rep (Xor l r) Source #

Since: 0.5

Instance details

Defined in Refined

type Rep (Xor l r) = D1 ('MetaData "Xor" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Xor" 'PrefixI 'False) (U1 :: Type -> Type))

Identity predicate

data IdPred Source #

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

Constructors

IdPred

Since: 0.4.2

Instances

Instances details
Generic IdPred Source # 
Instance details

Defined in Refined

Associated Types

type Rep IdPred :: Type -> Type #

Methods

from :: IdPred -> Rep IdPred x #

to :: Rep IdPred x -> IdPred #

Predicate IdPred x Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep IdPred Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep IdPred = D1 ('MetaData "IdPred" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "IdPred" 'PrefixI 'False) (U1 :: Type -> Type))

Numeric predicates

data LessThan (n :: Nat) Source #

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

Constructors

LessThan

Since: 0.4.2

Instances

Instances details
n <= m => Weaken (LessThan n :: Type) (LessThan m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (LessThan n) x -> Refined (LessThan m) x Source #

n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (LessThan n) x -> Refined (To m) x Source #

(Ord x, Num x, KnownNat n) => Predicate (LessThan n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Generic (LessThan n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (LessThan n) :: Type -> Type #

Methods

from :: LessThan n -> Rep (LessThan n) x #

to :: Rep (LessThan n) x -> LessThan n #

type Rep (LessThan n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (LessThan n) = D1 ('MetaData "LessThan" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "LessThan" 'PrefixI 'False) (U1 :: Type -> Type))

data GreaterThan (n :: Nat) Source #

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

Constructors

GreaterThan

Since: 0.4.2

Instances

Instances details
m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (GreaterThan n) x -> Refined (From m) x Source #

m <= n => Weaken (GreaterThan n :: Type) (GreaterThan m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Generic (GreaterThan n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (GreaterThan n) :: Type -> Type #

Methods

from :: GreaterThan n -> Rep (GreaterThan n) x #

to :: Rep (GreaterThan n) x -> GreaterThan n #

type Rep (GreaterThan n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (GreaterThan n) = D1 ('MetaData "GreaterThan" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "GreaterThan" 'PrefixI 'False) (U1 :: Type -> Type))

data From (n :: Nat) Source #

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

Constructors

From

Since: 0.4.2

Instances

Instances details
m <= n => Weaken (From n :: Type) (From m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (From n) x -> Refined (From m) x Source #

m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (GreaterThan n) x -> Refined (From m) x Source #

p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (From p) x Source #

(Ord x, Num x, KnownNat n) => Predicate (From n :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

Generic (From n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (From n) :: Type -> Type #

Methods

from :: From n -> Rep (From n) x #

to :: Rep (From n) x -> From n #

type Rep (From n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (From n) = D1 ('MetaData "From" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "From" 'PrefixI 'False) (U1 :: Type -> Type))

data To (n :: Nat) Source #

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

Constructors

To

Since: 0.4.2

Instances

Instances details
n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (LessThan n) x -> Refined (To m) x Source #

n <= m => Weaken (To n :: Type) (To m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (To n) x -> Refined (To m) x Source #

m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (To q) x Source #

(Ord x, Num x, KnownNat n) => Predicate (To n :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

Methods

validate :: Proxy (To n) -> x -> Maybe RefineException Source #

Generic (To n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (To n) :: Type -> Type #

Methods

from :: To n -> Rep (To n) x #

to :: Rep (To n) x -> To n #

type Rep (To n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (To n) = D1 ('MetaData "To" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "To" 'PrefixI 'False) (U1 :: Type -> Type))

data FromTo (mn :: Nat) (mx :: Nat) Source #

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

Constructors

FromTo

Since: 0.4.2

Instances

Instances details
p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (From p) x Source #

m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (To q) x Source #

(p <= n, m <= q) => Weaken (FromTo n m :: Type) (FromTo p q :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (FromTo p q) x Source #

(Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx :: Type) x Source #

Since: 0.1.2

Instance details

Defined in Refined

Methods

validate :: Proxy (FromTo mn mx) -> x -> Maybe RefineException Source #

Generic (FromTo mn mx) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (FromTo mn mx) :: Type -> Type #

Methods

from :: FromTo mn mx -> Rep (FromTo mn mx) x #

to :: Rep (FromTo mn mx) x -> FromTo mn mx #

type Rep (FromTo mn mx) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (FromTo mn mx) = D1 ('MetaData "FromTo" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "FromTo" 'PrefixI 'False) (U1 :: Type -> Type))

data 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.

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

Since: 0.4

Constructors

NegativeFromTo

Since: 0.4.2

Instances

Instances details
(Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m :: Type) x Source #

Since: 0.4

Instance details

Defined in Refined

Generic (NegativeFromTo n m) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (NegativeFromTo n m) :: Type -> Type #

Methods

from :: NegativeFromTo n m -> Rep (NegativeFromTo n m) x #

to :: Rep (NegativeFromTo n m) x -> NegativeFromTo n m #

type Rep (NegativeFromTo n m) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (NegativeFromTo n m) = D1 ('MetaData "NegativeFromTo" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "NegativeFromTo" 'PrefixI 'False) (U1 :: Type -> Type))

data EqualTo (n :: Nat) Source #

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

Constructors

EqualTo

Since: 0.4.2

Instances

Instances details
(Eq x, Num x, KnownNat n) => Predicate (EqualTo n :: Type) x Source #

Since: 0.1.0.0

Instance details

Defined in Refined

Generic (EqualTo n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (EqualTo n) :: Type -> Type #

Methods

from :: EqualTo n -> Rep (EqualTo n) x #

to :: Rep (EqualTo n) x -> EqualTo n #

type Rep (EqualTo n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (EqualTo n) = D1 ('MetaData "EqualTo" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "EqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

data NotEqualTo (n :: Nat) Source #

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

Constructors

NotEqualTo

Since: 0.4.2

Instances

Instances details
(Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n :: Type) x Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Generic (NotEqualTo n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (NotEqualTo n) :: Type -> Type #

Methods

from :: NotEqualTo n -> Rep (NotEqualTo n) x #

to :: Rep (NotEqualTo n) x -> NotEqualTo n #

type Rep (NotEqualTo n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (NotEqualTo n) = D1 ('MetaData "NotEqualTo" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "NotEqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

data Odd Source #

A Predicate ensuring that the value is odd.

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

Since: 0.4.2

Constructors

Odd

Since: 0.4.2

Instances

Instances details
Generic Odd Source # 
Instance details

Defined in Refined

Associated Types

type Rep Odd :: Type -> Type #

Methods

from :: Odd -> Rep Odd x #

to :: Rep Odd x -> Odd #

Integral x => Predicate Odd x Source #

Since: 0.4.2

Instance details

Defined in Refined

type Rep Odd Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep Odd = D1 ('MetaData "Odd" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Odd" 'PrefixI 'False) (U1 :: Type -> Type))

data Even Source #

A Predicate ensuring that the value is even.

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

Since: 0.4.2

Constructors

Even

Since: 0.4.2

Instances

Instances details
Generic Even Source # 
Instance details

Defined in Refined

Associated Types

type Rep Even :: Type -> Type #

Methods

from :: Even -> Rep Even x #

to :: Rep Even x -> Even #

Integral x => Predicate Even x Source #

Since: 0.4.2

Instance details

Defined in Refined

type Rep Even Source #

Since: 0.4.2

Instance details

Defined in Refined

type Rep Even = D1 ('MetaData "Even" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Even" 'PrefixI 'False) (U1 :: Type -> Type))

data DivisibleBy (n :: Nat) Source #

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

Constructors

DivisibleBy

Since: 0.4.2

Instances

Instances details
(Integral x, KnownNat n) => Predicate (DivisibleBy n :: Type) x Source #

Since: 0.4.2

Instance details

Defined in Refined

Generic (DivisibleBy n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (DivisibleBy n) :: Type -> Type #

Methods

from :: DivisibleBy n -> Rep (DivisibleBy n) x #

to :: Rep (DivisibleBy n) x -> DivisibleBy n #

type Rep (DivisibleBy n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (DivisibleBy n) = D1 ('MetaData "DivisibleBy" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "DivisibleBy" 'PrefixI 'False) (U1 :: Type -> Type))

data NaN Source #

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

Constructors

NaN

Since: 0.5

Instances

Instances details
Generic NaN Source # 
Instance details

Defined in Refined

Associated Types

type Rep NaN :: Type -> Type #

Methods

from :: NaN -> Rep NaN x #

to :: Rep NaN x -> NaN #

RealFloat x => Predicate NaN x Source #

Since: 0.5

Instance details

Defined in Refined

type Rep NaN Source #

Since: 0.5

Instance details

Defined in Refined

type Rep NaN = D1 ('MetaData "NaN" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "NaN" 'PrefixI 'False) (U1 :: Type -> Type))

data Infinite Source #

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

Constructors

Infinite

Since: 0.5

Instances

Instances details
Generic Infinite Source # 
Instance details

Defined in Refined

Associated Types

type Rep Infinite :: Type -> Type #

Methods

from :: Infinite -> Rep Infinite x #

to :: Rep Infinite x -> Infinite #

RealFloat x => Predicate Infinite x Source #

Since: 0.5

Instance details

Defined in Refined

type Rep Infinite Source #

Since: 0.5

Instance details

Defined in Refined

type Rep Infinite = D1 ('MetaData "Infinite" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Infinite" 'PrefixI 'False) (U1 :: Type -> Type))

type Positive = GreaterThan 0 Source #

A Predicate ensuring that the value is greater than zero.

Since: 0.1.0.0

type NonPositive = To 0 Source #

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

Since: 0.1.2

type Negative = LessThan 0 Source #

A Predicate ensuring that the value is less than zero.

Since: 0.1.0.0

type NonNegative = From 0 Source #

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

Since: 0.1.2

type ZeroToOne = FromTo 0 1 Source #

An inclusive range of values from zero to one.

Since: 0.1.0.0

type NonZero = NotEqualTo 0 Source #

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

Since: 0.2.0.0

Foldable predicates

Size predicates

data SizeLessThan (n :: Nat) Source #

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

Constructors

SizeLessThan

Since: 0.4.2

Instances

Instances details
n <= m => Weaken (SizeLessThan n :: Type) (SizeLessThan m :: Type) Source #

Since: 0.8.1

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeLessThan n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

(Foldable t, KnownNat n) => Predicate (SizeLessThan n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Generic (SizeLessThan n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (SizeLessThan n) :: Type -> Type #

Methods

from :: SizeLessThan n -> Rep (SizeLessThan n) x #

to :: Rep (SizeLessThan n) x -> SizeLessThan n #

type Rep (SizeLessThan n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (SizeLessThan n) = D1 ('MetaData "SizeLessThan" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "SizeLessThan" 'PrefixI 'False) (U1 :: Type -> Type))

data SizeGreaterThan (n :: Nat) Source #

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

Constructors

SizeGreaterThan

Since: 0.4.2

Instances

Instances details
m <= n => Weaken (SizeGreaterThan n :: Type) (SizeGreaterThan m :: Type) Source #

Since: 0.8.1

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeGreaterThan n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

(Foldable t, KnownNat n) => Predicate (SizeGreaterThan n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Generic (SizeGreaterThan n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (SizeGreaterThan n) :: Type -> Type #

type Rep (SizeGreaterThan n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (SizeGreaterThan n) = D1 ('MetaData "SizeGreaterThan" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "SizeGreaterThan" 'PrefixI 'False) (U1 :: Type -> Type))

data SizeEqualTo (n :: Nat) Source #

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

Constructors

SizeEqualTo

Since: 0.4.2

Instances

Instances details
KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeEqualTo n :: Type) ByteString Source #

Since: 0.5

Instance details

Defined in Refined

KnownNat n => Predicate (SizeEqualTo n :: Type) Text Source #

Since: 0.5

Instance details

Defined in Refined

(Foldable t, KnownNat n) => Predicate (SizeEqualTo n :: Type) (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Generic (SizeEqualTo n) Source # 
Instance details

Defined in Refined

Associated Types

type Rep (SizeEqualTo n) :: Type -> Type #

Methods

from :: SizeEqualTo n -> Rep (SizeEqualTo n) x #

to :: Rep (SizeEqualTo n) x -> SizeEqualTo n #

type Rep (SizeEqualTo n) Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep (SizeEqualTo n) = D1 ('MetaData "SizeEqualTo" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "SizeEqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

type Empty = SizeEqualTo 0 Source #

A Predicate ensuring that the type is empty.

Since: 0.5

type NonEmpty = SizeGreaterThan 0 Source #

A Predicate ensuring that the type is non-empty.

Since: 0.2.0.0

Ordering predicates

data Ascending Source #

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

Constructors

Ascending

Since: 0.4.2

Instances

Instances details
Generic Ascending Source # 
Instance details

Defined in Refined

Associated Types

type Rep Ascending :: Type -> Type #

(Foldable t, Ord a) => Predicate Ascending (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

type Rep Ascending Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep Ascending = D1 ('MetaData "Ascending" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Ascending" 'PrefixI 'False) (U1 :: Type -> Type))

data Descending Source #

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

Constructors

Descending

Since: 0.4.2

Instances

Instances details
Generic Descending Source # 
Instance details

Defined in Refined

Associated Types

type Rep Descending :: Type -> Type #

(Foldable t, Ord a) => Predicate Descending (t a) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

type Rep Descending Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep Descending = D1 ('MetaData "Descending" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) (C1 ('MetaCons "Descending" 'PrefixI 'False) (U1 :: Type -> Type))

Weakening

class Weaken from to 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.

Since: 0.2.0.0

Minimal complete definition

Nothing

Methods

weaken :: Refined from x -> Refined to x Source #

Since: 0.2.0.0

Instances

Instances details
m <= n => Weaken (From n :: Type) (From m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (From n) x -> Refined (From m) x Source #

m <= n => Weaken (GreaterThan n :: Type) (From m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (GreaterThan n) x -> Refined (From m) x Source #

m <= n => Weaken (GreaterThan n :: Type) (GreaterThan m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

n <= m => Weaken (LessThan n :: Type) (LessThan m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (LessThan n) x -> Refined (LessThan m) x Source #

n <= m => Weaken (LessThan n :: Type) (To m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (LessThan n) x -> Refined (To m) x Source #

m <= n => Weaken (SizeGreaterThan n :: Type) (SizeGreaterThan m :: Type) Source #

Since: 0.8.1

Instance details

Defined in Refined

n <= m => Weaken (SizeLessThan n :: Type) (SizeLessThan m :: Type) Source #

Since: 0.8.1

Instance details

Defined in Refined

n <= m => Weaken (To n :: Type) (To m :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (To n) x -> Refined (To m) x Source #

p <= n => Weaken (FromTo n m :: Type) (From p :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (From p) x Source #

m <= q => Weaken (FromTo n m :: Type) (To q :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (To q) x Source #

(p <= n, m <= q) => Weaken (FromTo n m :: Type) (FromTo p q :: Type) Source #

Since: 0.2.0.0

Instance details

Defined in Refined

Methods

weaken :: Refined (FromTo n m) x -> Refined (FromTo p q) x Source #

andLeft :: 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

Since: 0.2.0.0

andRight :: 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

Since: 0.2.0.0

leftOr :: 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)

Since: 0.2.0.0

rightOr :: 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)

Since: 0.2.0.0

weakenAndLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a Source #

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

weakenAndRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a Source #

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

weakenOrLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a Source #

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

weakenOrRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a Source #

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

Strengthening

strengthen :: forall p p' x. (Predicate p x, Predicate p' x) => Refined p x -> Either RefineException (Refined (p && p') x) Source #

Strengthen a refinement by composing it with another.

Since: 0.4.2.2

Error handling

RefineException

data RefineException Source #

An exception encoding the way in which a Predicate failed.

Since: 0.2.0.0

Constructors

RefineNotException !TypeRep

A RefineException for failures involving the Not predicate.

Since: 0.2.0.0

RefineAndException !TypeRep !(These RefineException RefineException)

A RefineException for failures involving the And predicate.

Since: 0.2.0.0

RefineOrException !TypeRep !RefineException !RefineException

A RefineException for failures involving the Or predicate.

Since: 0.2.0.0

RefineXorException !TypeRep !(Maybe (RefineException, RefineException))

A RefineException for failures involving the Xor predicate.

Since: 0.5

RefineSomeException !TypeRep !SomeException

A RefineException for failures involving all other predicates with custom exception.

Since: 0.5

RefineOtherException !TypeRep !Text

A RefineException for failures involving all other predicates.

Since: 0.2.0.0

Instances

Instances details
Exception RefineException Source #

Encode a RefineException for use with Control.Exception.

Note: Equivalent to displayRefineException.

Since: 0.2.0.0

Instance details

Defined in Refined

Generic RefineException Source # 
Instance details

Defined in Refined

Associated Types

type Rep RefineException :: Type -> Type #

Show RefineException Source #

Note: Equivalent to displayRefineException.

Since: 0.2.0.0

Instance details

Defined in Refined

type Rep RefineException Source #

Since: 0.3.0.0

Instance details

Defined in Refined

type Rep RefineException = D1 ('MetaData "RefineException" "Refined" "refined-0.8.1-GdGOxvI4Xw22hmwlQhjdzi" 'False) ((C1 ('MetaCons "RefineNotException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep)) :+: (C1 ('MetaCons "RefineAndException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep) :*: S1 ('MetaSel ('Just "_RefineException_andChild") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (These RefineException RefineException))) :+: C1 ('MetaCons "RefineOrException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep) :*: (S1 ('MetaSel ('Just "_RefineException_orLChild") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 RefineException) :*: S1 ('MetaSel ('Just "_RefineException_orRChild") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 RefineException))))) :+: (C1 ('MetaCons "RefineXorException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep) :*: S1 ('MetaSel ('Just "_RefineException_children") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (RefineException, RefineException)))) :+: (C1 ('MetaCons "RefineSomeException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep) :*: S1 ('MetaSel ('Just "_RefineException_Exception") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SomeException)) :+: C1 ('MetaCons "RefineOtherException" 'PrefixI 'True) (S1 ('MetaSel ('Just "_RefineException_typeRep") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeRep) :*: S1 ('MetaSel ('Just "_RefineException_message") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)))))

displayRefineException :: 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

Since: 0.2.0.0

validate helpers

throwRefineOtherException Source #

Arguments

:: TypeRep

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

-> Text

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

-> Maybe RefineException 

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

throwRefineSomeException Source #

Arguments

:: TypeRep

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

-> SomeException

A custom exception.

-> Maybe RefineException 

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

success :: Maybe RefineException Source #

An implementation of validate that always succeeds.

Examples

Expand
  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

Orphan instances

(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) Source #

Since: 0.4

Instance details

Methods

arbitrary :: Gen (Refined p a) #

shrink :: Refined p a -> [Refined p a] #

(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source #

Since: 0.4

Instance details

(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # 
Instance details

(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source #

Since: 0.4

Instance details

(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source #

Since: 0.6.3

Instance details

(Read x, Predicate p x) => Read (Refined p x) Source #

This instance makes sure to check the refinement.

Since: 0.1.0.0

Instance details