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/

Refined type

data Refined (p :: k) x

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

Since: 0.1.0.0

Instances

Lift x => Lift (Refined p x :: Type)

Since: 0.1.0.0

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)

Since: 0.2

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)

Since: 0.4

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)

Since: 0.4

Defined in Refined

Methods

parseJSON :: Value -> Parser (Refined p a)

parseJSONList :: Value -> Parser [Refined p a]

(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a)

Defined in Refined

Methods

fromJSONKey :: FromJSONKeyFunction (Refined p a)

fromJSONKeyList :: FromJSONKeyFunction [Refined p a]

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

Since: 0.4

Defined in Refined

Methods

toJSON :: Refined p a -> Value

toEncoding :: Refined p a -> Encoding

toJSONList :: [Refined p a] -> Value

toEncodingList :: [Refined p a] -> Encoding

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

Since: 0.6.3

Defined in Refined

Methods

toJSONKey :: ToJSONKeyFunction (Refined p a)

toJSONKeyList :: ToJSONKeyFunction [Refined p a]

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

This instance makes sure to check the refinement.

Since: 0.1.0.0

Defined in Refined

Methods

readsPrec :: Int -> ReadS (Refined p x)

readList :: ReadS [Refined p x]

readPrec :: ReadPrec (Refined p x)

readListPrec :: ReadPrec [Refined p x]

Show x => Show (Refined p x)

Since: 0.1.0.0

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)

Since: 0.5

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined p x -> ()

Eq x => Eq (Refined p x)

Since: 0.1.0.0

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)

Since: 0.1.0.0

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)

Since: 0.6.3

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)

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

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)

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)

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)

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)

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)

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

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

Extracts the refined value.

Since: 0.1.0.0

Refined1 type

data Refined1 (p :: k) f x

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

The predicate is applied over the functor f. Thus, we may safely recover various Functory instances, because no matter what you do to the values inside the functor, the predicate may not be invalidated.

Instances

Lift (f a) => Lift (Refined1 p f a :: Type)

Defined in Refined.Unsafe.Type

Methods

lift :: Quote m => Refined1 p f a -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> Code m (Refined1 p f a)

Foldable f => Foldable (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

fold :: Monoid m => Refined1 p f m -> m

foldMap :: Monoid m => (a -> m) -> Refined1 p f a -> m

foldMap' :: Monoid m => (a -> m) -> Refined1 p f a -> m

foldr :: (a -> b -> b) -> b -> Refined1 p f a -> b

foldr' :: (a -> b -> b) -> b -> Refined1 p f a -> b

foldl :: (b -> a -> b) -> b -> Refined1 p f a -> b

foldl' :: (b -> a -> b) -> b -> Refined1 p f a -> b

foldr1 :: (a -> a -> a) -> Refined1 p f a -> a

foldl1 :: (a -> a -> a) -> Refined1 p f a -> a

toList :: Refined1 p f a -> [a]

null :: Refined1 p f a -> Bool

length :: Refined1 p f a -> Int

elem :: Eq a => a -> Refined1 p f a -> Bool

maximum :: Ord a => Refined1 p f a -> a

minimum :: Ord a => Refined1 p f a -> a

sum :: Num a => Refined1 p f a -> a

product :: Num a => Refined1 p f a -> a

Traversable f => Traversable (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Refined1 p f a -> f0 (Refined1 p f b)

sequenceA :: Applicative f0 => Refined1 p f (f0 a) -> f0 (Refined1 p f a)

mapM :: Monad m => (a -> m b) -> Refined1 p f a -> m (Refined1 p f b)

sequence :: Monad m => Refined1 p f (m a) -> m (Refined1 p f a)

Functor f => Functor (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

fmap :: (a -> b) -> Refined1 p f a -> Refined1 p f b

(<$) :: a -> Refined1 p f b -> Refined1 p f a

Show (f x) => Show (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

showsPrec :: Int -> Refined1 p f x -> ShowS

show :: Refined1 p f x -> String

showList :: [Refined1 p f x] -> ShowS

NFData (f x) => NFData (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined1 p f x -> ()

Eq (f x) => Eq (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

(==) :: Refined1 p f x -> Refined1 p f x -> Bool

(/=) :: Refined1 p f x -> Refined1 p f x -> Bool

Ord (f x) => Ord (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

compare :: Refined1 p f x -> Refined1 p f x -> Ordering

(<) :: Refined1 p f x -> Refined1 p f x -> Bool

(<=) :: Refined1 p f x -> Refined1 p f x -> Bool

(>) :: Refined1 p f x -> Refined1 p f x -> Bool

(>=) :: Refined1 p f x -> Refined1 p f x -> Bool

max :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x

min :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x

Hashable (f x) => Hashable (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

hashWithSalt :: Int -> Refined1 p f x -> Int

hash :: Refined1 p f x -> Int

Creation

refine1 :: forall p f x. Predicate1 p f => f x -> Either RefineException (Refined1 p f x)

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

Since: 0.1.0.0

Consumption

unrefine1 :: Refined1 p f x -> f x

Extracts the refined value.

Predicate

class (Typeable p, Typeable k) => Predicate (p :: k) x where

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

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.

Note that due to GHC's type variable order rules, this function has an implicit kind in position 1, which makes TypeApplications awkward. Use validate' for nicer behaviour.

Instances

Integral x => Predicate Even x

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy Even -> x -> Maybe RefineException

Predicate IdPred x

Since: 0.3.0.0

Defined in Refined

Methods

validate :: Proxy IdPred -> x -> Maybe RefineException

RealFloat x => Predicate Infinite x

Since: 0.5

Defined in Refined

Methods

validate :: Proxy Infinite -> x -> Maybe RefineException

RealFloat x => Predicate NaN x

Since: 0.5

Defined in Refined

Methods

validate :: Proxy NaN -> x -> Maybe RefineException

Integral x => Predicate Odd x

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy Odd -> x -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy Ascending -> t a -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy Descending -> t a -> Maybe RefineException

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

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy (DivisibleBy n) -> x -> Maybe RefineException

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (EqualTo n) -> x -> Maybe RefineException

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

Since: 0.1.2

Defined in Refined

Methods

validate :: Proxy (From n) -> x -> Maybe RefineException

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (GreaterThan n) -> x -> Maybe RefineException

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (LessThan n) -> x -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (NotEqualTo n) -> x -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> Text -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> Text -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> Text -> Maybe RefineException

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

Since: 0.1.2

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> t a -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> t a -> Maybe RefineException

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

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> t a -> Maybe RefineException

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

Since: 0.1.2

Defined in Refined

Methods

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

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

Since: 0.4

Defined in Refined

Methods

validate :: Proxy (NegativeFromTo n m) -> x -> Maybe RefineException

Predicate p x => Predicate (Not p :: Type) x

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (Not p) -> x -> Maybe RefineException

(Predicate l x, Predicate r x) => Predicate (And l r :: Type) x

Since: 0.1.0.0

Defined in Refined

Methods

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

(Predicate l x, Predicate r x) => Predicate (Or l r :: Type) x

Since: 0.2.0.0

Defined in Refined

Methods

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

(Predicate l x, Predicate r x) => Predicate (Xor l r :: Type) x

Since: 0.5

Defined in Refined

Methods

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

validate' :: forall {k} p x. Predicate (p :: k) x => Proxy p -> x -> Maybe RefineException

Check the value x according to the predicate p, producing an error RefineException if the value does not satisfy.

Same as validate but with more convenient type variable order for a better TypeApplications experience.

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

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

Since: 0.4.2.3

Predicate1

class (Typeable p, Typeable k) => Predicate1 (p :: k) f where

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

The inner type may not be inspected. If you find yourself needing to add constraints to it, you want Predicate.

Methods

validate1 :: Proxy p -> f a -> Maybe RefineException

Check the value f a according to the predicate p, producing an error RefineException if the value does not satisfy.

Note: validate1 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.

Note that due to GHC's type variable order rules, this function has an implicit kind in position 1, which makes TypeApplications awkward. Use validate1' for nicer behaviour.

Instances

(Foldable t, KnownNat n) => Predicate1 (SizeEqualTo n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeEqualTo n) -> t a -> Maybe RefineException

(Foldable t, KnownNat n) => Predicate1 (SizeGreaterThan n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeGreaterThan n) -> t a -> Maybe RefineException

(Foldable t, KnownNat n) => Predicate1 (SizeLessThan n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeLessThan n) -> t a -> Maybe RefineException

validate1' :: forall {k} p f a. Predicate1 (p :: k) f => Proxy p -> f a -> Maybe RefineException

Check the value f a according to the predicate p, producing an error RefineException if the value does not satisfy.

Same as validate1 but with more convenient type variable order for a better TypeApplications experience.

Logical predicates

data Not p

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

Generic1 (Not :: k -> Type)

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 => Predicate (Not p :: Type) x

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (Not p) -> x -> Maybe RefineException

Generic (Not p)

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)

Since: 0.3.0.0

Defined in Refined

type Rep1 (Not :: k -> Type) = D1 ('MetaData "Not" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: k -> Type))

type Rep (Not p)

Since: 0.3.0.0

Defined in Refined

type Rep (Not p) = D1 ('MetaData "Not" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: Type -> Type))

data And l r

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

Generic1 (And l :: k1 -> Type)

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) => Predicate (And l r :: Type) x

Since: 0.1.0.0

Defined in Refined

Methods

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

Generic (And l r)

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)

Since: 0.3.0.0

Defined in Refined

type Rep1 (And l :: k1 -> Type) = D1 ('MetaData "And" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: k1 -> Type))

type Rep (And l r)

Since: 0.3.0.0

Defined in Refined

type Rep (And l r) = D1 ('MetaData "And" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: Type -> Type))

type (&&) = And infixr 3

The conjunction of two predicates.

Since: 0.2.0.0

data Or l r

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

Generic1 (Or l :: k1 -> Type)

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) => Predicate (Or l r :: Type) x

Since: 0.2.0.0

Defined in Refined

Methods

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

Generic (Or l r)

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)

Since: 0.3.0.0

Defined in Refined

type Rep1 (Or l :: k1 -> Type) = D1 ('MetaData "Or" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: k1 -> Type))

type Rep (Or l r)

Since: 0.3.0.0

Defined in Refined

type Rep (Or l r) = D1 ('MetaData "Or" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: Type -> Type))

type (||) = Or infixr 2

The disjunction of two predicates.

Since: 0.2.0.0

data Xor l r

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

Generic1 (Xor l :: k1 -> Type)

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) => Predicate (Xor l r :: Type) x

Since: 0.5

Defined in Refined

Methods

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

Generic (Xor l r)

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)

Since: 0.5

Defined in Refined

type Rep1 (Xor l :: k1 -> Type) = D1 ('MetaData "Xor" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Xor" 'PrefixI 'False) (U1 :: k1 -> Type))

type Rep (Xor l r)

Since: 0.5

Defined in Refined

type Rep (Xor l r) = D1 ('MetaData "Xor" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Xor" 'PrefixI 'False) (U1 :: Type -> Type))

Identity predicate

data IdPred

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

Generic IdPred

Defined in Refined

Associated Types

type Rep IdPred :: Type -> Type

Methods

from :: IdPred -> Rep IdPred x

to :: Rep IdPred x -> IdPred

Predicate IdPred x

Since: 0.3.0.0

Defined in Refined

Methods

validate :: Proxy IdPred -> x -> Maybe RefineException

type Rep IdPred

Since: 0.3.0.0

Defined in Refined

type Rep IdPred = D1 ('MetaData "IdPred" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "IdPred" 'PrefixI 'False) (U1 :: Type -> Type))

Numeric predicates

data LessThan (n :: Nat)

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (LessThan n) -> x -> Maybe RefineException

Generic (LessThan n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (LessThan n) = D1 ('MetaData "LessThan" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "LessThan" 'PrefixI 'False) (U1 :: Type -> Type))

data GreaterThan (n :: Nat)

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (GreaterThan n) -> x -> Maybe RefineException

Generic (GreaterThan n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (GreaterThan n) = D1 ('MetaData "GreaterThan" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "GreaterThan" 'PrefixI 'False) (U1 :: Type -> Type))

data From (n :: Nat)

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

m <= n => Weaken (From n :: Type) (From m :: Type)

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.1.2

Defined in Refined

Methods

validate :: Proxy (From n) -> x -> Maybe RefineException

Generic (From n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (From n) = D1 ('MetaData "From" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "From" 'PrefixI 'False) (U1 :: Type -> Type))

data To (n :: Nat)

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.1.2

Defined in Refined

Methods

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

Generic (To n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (To n) = D1 ('MetaData "To" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "To" 'PrefixI 'False) (U1 :: Type -> Type))

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

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.1.2

Defined in Refined

Methods

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

Generic (FromTo mn mx)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (FromTo mn mx) = D1 ('MetaData "FromTo" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "FromTo" 'PrefixI 'False) (U1 :: Type -> Type))

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

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

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

Since: 0.4

Defined in Refined

Methods

validate :: Proxy (NegativeFromTo n m) -> x -> Maybe RefineException

Generic (NegativeFromTo n m)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (NegativeFromTo n m) = D1 ('MetaData "NegativeFromTo" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "NegativeFromTo" 'PrefixI 'False) (U1 :: Type -> Type))

data EqualTo (n :: Nat)

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

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

Since: 0.1.0.0

Defined in Refined

Methods

validate :: Proxy (EqualTo n) -> x -> Maybe RefineException

Generic (EqualTo n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (EqualTo n) = D1 ('MetaData "EqualTo" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "EqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

data NotEqualTo (n :: Nat)

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

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (NotEqualTo n) -> x -> Maybe RefineException

Generic (NotEqualTo n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (NotEqualTo n) = D1 ('MetaData "NotEqualTo" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "NotEqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

data Odd

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

Generic Odd

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

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy Odd -> x -> Maybe RefineException

type Rep Odd

Since: 0.3.0.0

Defined in Refined

type Rep Odd = D1 ('MetaData "Odd" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Odd" 'PrefixI 'False) (U1 :: Type -> Type))

data Even

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

Generic Even

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

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy Even -> x -> Maybe RefineException

type Rep Even

Since: 0.4.2

Defined in Refined

type Rep Even = D1 ('MetaData "Even" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Even" 'PrefixI 'False) (U1 :: Type -> Type))

data DivisibleBy (n :: Nat)

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

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

Since: 0.4.2

Defined in Refined

Methods

validate :: Proxy (DivisibleBy n) -> x -> Maybe RefineException

Generic (DivisibleBy n)

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)

Since: 0.3.0.0

Defined in Refined

type Rep (DivisibleBy n) = D1 ('MetaData "DivisibleBy" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "DivisibleBy" 'PrefixI 'False) (U1 :: Type -> Type))

data NaN

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

Generic NaN

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy NaN -> x -> Maybe RefineException

type Rep NaN

Since: 0.5

Defined in Refined

type Rep NaN = D1 ('MetaData "NaN" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "NaN" 'PrefixI 'False) (U1 :: Type -> Type))

data Infinite

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

Generic Infinite

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy Infinite -> x -> Maybe RefineException

type Rep Infinite

Since: 0.5

Defined in Refined

type Rep Infinite = D1 ('MetaData "Infinite" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Infinite" 'PrefixI 'False) (U1 :: Type -> Type))

type Positive = GreaterThan 0

A Predicate ensuring that the value is greater than zero.

Since: 0.1.0.0

type NonPositive = To 0

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

Since: 0.1.2

type Negative = LessThan 0

A Predicate ensuring that the value is less than zero.

Since: 0.1.0.0

type NonNegative = From 0

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

Since: 0.1.2

type ZeroToOne = FromTo 0 1

An inclusive range of values from zero to one.

Since: 0.1.0.0

type NonZero = NotEqualTo 0

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

Since: 0.2.0.0

Foldable predicates

Size predicates

data SizeLessThan (n :: Nat)

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

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

Since: 0.8.1

Defined in Refined

Methods

weaken :: Refined (SizeLessThan n) x -> Refined (SizeLessThan m) x

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> Text -> Maybe RefineException

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

Defined in Refined

Methods

validate :: Proxy (SizeLessThan n) -> t a -> Maybe RefineException

Generic (SizeLessThan n)

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

(Foldable t, KnownNat n) => Predicate1 (SizeLessThan n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeLessThan n) -> t a -> Maybe RefineException

type Rep (SizeLessThan n)

Since: 0.3.0.0

Defined in Refined

type Rep (SizeLessThan n) = D1 ('MetaData "SizeLessThan" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "SizeLessThan" 'PrefixI 'False) (U1 :: Type -> Type))

data SizeGreaterThan (n :: Nat)

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

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

Since: 0.8.1

Defined in Refined

Methods

weaken :: Refined (SizeGreaterThan n) x -> Refined (SizeGreaterThan m) x

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> Text -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (SizeGreaterThan n) -> t a -> Maybe RefineException

Generic (SizeGreaterThan n)

Defined in Refined

Associated Types

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

Methods

from :: SizeGreaterThan n -> Rep (SizeGreaterThan n) x

to :: Rep (SizeGreaterThan n) x -> SizeGreaterThan n

(Foldable t, KnownNat n) => Predicate1 (SizeGreaterThan n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeGreaterThan n) -> t a -> Maybe RefineException

type Rep (SizeGreaterThan n)

Since: 0.3.0.0

Defined in Refined

type Rep (SizeGreaterThan n) = D1 ('MetaData "SizeGreaterThan" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "SizeGreaterThan" 'PrefixI 'False) (U1 :: Type -> Type))

data SizeEqualTo (n :: Nat)

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

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException

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

Since: 0.5

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> Text -> Maybe RefineException

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy (SizeEqualTo n) -> t a -> Maybe RefineException

Generic (SizeEqualTo n)

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

(Foldable t, KnownNat n) => Predicate1 (SizeEqualTo n :: Type) (t :: TYPE LiftedRep -> Type)

Defined in Refined

Methods

validate1 :: forall (a :: k). Proxy (SizeEqualTo n) -> t a -> Maybe RefineException

type Rep (SizeEqualTo n)

Since: 0.3.0.0

Defined in Refined

type Rep (SizeEqualTo n) = D1 ('MetaData "SizeEqualTo" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "SizeEqualTo" 'PrefixI 'False) (U1 :: Type -> Type))

type Empty = SizeEqualTo 0

A Predicate ensuring that the type is empty.

Since: 0.5

type NonEmpty = SizeGreaterThan 0

A Predicate ensuring that the type is non-empty.

Since: 0.2.0.0

Ordering predicates

data Ascending

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

Generic Ascending

Defined in Refined

Associated Types

type Rep Ascending :: Type -> Type

Methods

from :: Ascending -> Rep Ascending x

to :: Rep Ascending x -> Ascending

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy Ascending -> t a -> Maybe RefineException

type Rep Ascending

Since: 0.3.0.0

Defined in Refined

type Rep Ascending = D1 ('MetaData "Ascending" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Ascending" 'PrefixI 'False) (U1 :: Type -> Type))

data Descending

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

Generic Descending

Defined in Refined

Associated Types

type Rep Descending :: Type -> Type

Methods

from :: Descending -> Rep Descending x

to :: Rep Descending x -> Descending

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

Since: 0.2.0.0

Defined in Refined

Methods

validate :: Proxy Descending -> t a -> Maybe RefineException

type Rep Descending

Since: 0.3.0.0

Defined in Refined

type Rep Descending = D1 ('MetaData "Descending" "Refined" "refined1-0.9.0-inplace" 'False) (C1 ('MetaCons "Descending" 'PrefixI 'False) (U1 :: Type -> Type))

Weakening

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

Since: 0.2.0.0

Minimal complete definition

Nothing

Methods

weaken :: Refined from x -> Refined to x

Since: 0.2.0.0

Instances

m <= n => Weaken (From n :: Type) (From m :: Type)

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.8.1

Defined in Refined

Methods

weaken :: Refined (SizeGreaterThan n) x -> Refined (SizeGreaterThan m) x

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

Since: 0.8.1

Defined in Refined

Methods

weaken :: Refined (SizeLessThan n) x -> Refined (SizeLessThan m) x

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

Defined in Refined

Methods

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

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

Since: 0.2.0.0

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

Since: 0.2.0.0

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

Since: 0.2.0.0

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

Since: 0.2.0.0

weakenAndLeft :: Weaken from to => Refined (And from x) a -> 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)

Since: 0.8.1.0

weakenAndRight :: Weaken from to => Refined (And x from) a -> 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)

Since: 0.8.1.0

weakenOrLeft :: Weaken from to => Refined (And from x) a -> 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)

Since: 0.8.1.0

weakenOrRight :: Weaken from to => Refined (And x from) a -> 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)

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)

Strengthen a refinement by composing it with another.

Since: 0.4.2.2

Error handling

RefineException

data RefineException

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

Exception RefineException

Encode a RefineException for use with Control.Exception.

Note: Equivalent to displayRefineException.

Since: 0.2.0.0

Defined in Refined

Methods

toException :: RefineException -> SomeException

fromException :: SomeException -> Maybe RefineException

displayException :: RefineException -> String

Generic RefineException

Defined in Refined

Associated Types

type Rep RefineException :: Type -> Type

Methods

from :: RefineException -> Rep RefineException x

to :: Rep RefineException x -> RefineException

Show RefineException

Note: Equivalent to displayRefineException.

Since: 0.2.0.0

Defined in Refined

Methods

showsPrec :: Int -> RefineException -> ShowS

show :: RefineException -> String

showList :: [RefineException] -> ShowS

type Rep RefineException

Since: 0.3.0.0

Defined in Refined

type Rep RefineException = D1 ('MetaData "RefineException" "Refined" "refined1-0.9.0-inplace" '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

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

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

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

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

Orphan instances

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

Since: 0.4

Methods

arbitrary :: Gen (Refined p a)

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

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

Since: 0.4

Methods

parseJSON :: Value -> Parser (Refined p a)

parseJSONList :: Value -> Parser [Refined p a]

(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a)

Methods

fromJSONKey :: FromJSONKeyFunction (Refined p a)

fromJSONKeyList :: FromJSONKeyFunction [Refined p a]

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

Since: 0.4

Methods

toJSON :: Refined p a -> Value

toEncoding :: Refined p a -> Encoding

toJSONList :: [Refined p a] -> Value

toEncodingList :: [Refined p a] -> Encoding

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

Since: 0.6.3

Methods

toJSONKey :: ToJSONKeyFunction (Refined p a)

toJSONKeyList :: ToJSONKeyFunction [Refined p a]

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

This instance makes sure to check the refinement.

Since: 0.1.0.0

Methods

readsPrec :: Int -> ReadS (Refined p x)

readList :: ReadS [Refined p x]

readPrec :: ReadPrec (Refined p x)

readListPrec :: ReadPrec [Refined p x]