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/

This module only provides safe constructions of Refined values, safe meaning that the refinement predicate holds, and the construction of the Refined value is total.

If you can manually prove that the refinement predicate holds, or you do not necessarily care about this definition of safety, use the module Refined.Unsafe.

Refined

data Refined p x

A refinement type, which wraps a value of type x, ensuring that it satisfies a type-level predicate p.

Instances

Foldable (Refined p)

Defined in Refined.Internal

Methods

fold :: Monoid m => Refined p m -> 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

Eq x => Eq (Refined p x)

Defined in Refined.Internal

Methods

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

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

Ord x => Ord (Refined p x)

Defined in Refined.Internal

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

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

This instance makes sure to check the refinement.

Defined in Refined.Internal

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)

Defined in Refined.Internal

Methods

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

show :: Refined p x -> String

showList :: [Refined p x] -> ShowS

Lift x => Lift (Refined p x)

Defined in Refined.Internal

Methods

lift :: Refined p x -> Q Exp

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

Defined in Refined.Orphan.QuickCheck

Methods

arbitrary :: Gen (Refined p a)

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

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

Defined in Refined.Orphan.Aeson

Methods

toJSON :: Refined p a -> Value

toEncoding :: Refined p a -> Encoding

toJSONList :: [Refined p a] -> Value

toEncodingList :: [Refined p a] -> Encoding

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

Defined in Refined.Orphan.Aeson

Methods

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

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

Creation

refine :: Predicate p x => x -> Either RefineException (Refined p x)

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

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.

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.

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.

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.

refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (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

If it's not evident, 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.

It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/

refineTH_ :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp x)

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

Consumption

unrefine :: Refined p x -> x

Extracts the refined value.

Predicate

class Typeable p => Predicate p x where

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

Methods

validate :: Monad m => p -> x -> RefineT m ()

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

Instances

Integral x => Predicate Even x

Defined in Refined.Internal

Methods

validate :: Monad m => Even -> x -> RefineT m ()

Integral x => Predicate Odd x

Defined in Refined.Internal

Methods

validate :: Monad m => Odd -> x -> RefineT m ()

Predicate IdPred x

Defined in Refined.Internal

Methods

validate :: Monad m => IdPred -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => Descending -> t a -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => Ascending -> t a -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => DivisibleBy n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => NotEqualTo n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => EqualTo n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => To n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => From n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => GreaterThan n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => LessThan n -> x -> RefineT m ()

(Predicate p x, Typeable p) => Predicate (Not p) x

Defined in Refined.Internal

Methods

validate :: Monad m => Not p -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => SizeEqualTo n -> t a -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => SizeGreaterThan n -> t a -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => SizeLessThan n -> t a -> RefineT m ()

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

Defined in Refined.Internal

Methods

validate :: Monad m0 => NegativeFromTo n m -> x -> RefineT m0 ()

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

Defined in Refined.Internal

Methods

validate :: Monad m => FromTo mn mx -> x -> RefineT m ()

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (Or l r) x

Defined in Refined.Internal

Methods

validate :: Monad m => Or l r -> x -> RefineT m ()

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (And l r) x

Defined in Refined.Internal

Methods

validate :: Monad m => And l r -> x -> RefineT m ()

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

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

Logical predicates

data Not p

The negation of a predicate.

>>> isRight (refine @(Not NonEmpty) @[Int] [])
True

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

Constructors

Not

Instances

Generic (Not p)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

Generic1 Not

Defined in Refined.Internal

Associated Types

type Rep1 Not :: k -> Type

Methods

from1 :: Not a -> Rep1 Not a

to1 :: Rep1 Not a -> Not a

(Predicate p x, Typeable p) => Predicate (Not p) x

Defined in Refined.Internal

Methods

validate :: Monad m => Not p -> x -> RefineT m ()

type Rep (Not p)

Defined in Refined.Internal

type Rep (Not p) = D1 (MetaData "Not" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "Not" PrefixI False) (U1 :: Type -> Type))

type Rep1 Not

Defined in Refined.Internal

type Rep1 Not = D1 (MetaData "Not" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

And

Instances

Generic1 (And l :: Type -> Type)

Defined in Refined.Internal

Associated Types

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

Methods

from1 :: And l a -> Rep1 (And l) a

to1 :: Rep1 (And l) a -> And l a

Generic (And l r)

Defined in Refined.Internal

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

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (And l r) x

Defined in Refined.Internal

Methods

validate :: Monad m => And l r -> x -> RefineT m ()

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

Defined in Refined.Internal

type Rep1 (And l :: Type -> Type) = D1 (MetaData "And" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "And" PrefixI False) (U1 :: Type -> Type))

type Rep (And l r)

Defined in Refined.Internal

type Rep (And l r) = D1 (MetaData "And" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "And" PrefixI False) (U1 :: Type -> Type))

type (&&) = And infixr 3

The conjunction of two predicates.

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

Constructors

Or

Instances

Generic1 (Or l :: Type -> Type)

Defined in Refined.Internal

Associated Types

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

Methods

from1 :: Or l a -> Rep1 (Or l) a

to1 :: Rep1 (Or l) a -> Or l a

Generic (Or l r)

Defined in Refined.Internal

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

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (Or l r) x

Defined in Refined.Internal

Methods

validate :: Monad m => Or l r -> x -> RefineT m ()

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

Defined in Refined.Internal

type Rep1 (Or l :: Type -> Type) = D1 (MetaData "Or" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "Or" PrefixI False) (U1 :: Type -> Type))

type Rep (Or l r)

Defined in Refined.Internal

type Rep (Or l r) = D1 (MetaData "Or" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "Or" PrefixI False) (U1 :: Type -> Type))

type (||) = Or infixr 2

The disjunction of two predicates.

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

Constructors

IdPred

Instances

Generic IdPred

Defined in Refined.Internal

Associated Types

type Rep IdPred :: Type -> Type

Methods

from :: IdPred -> Rep IdPred x

to :: Rep IdPred x -> IdPred

Predicate IdPred x

Defined in Refined.Internal

Methods

validate :: Monad m => IdPred -> x -> RefineT m ()

type Rep IdPred

Defined in Refined.Internal

type Rep IdPred = D1 (MetaData "IdPred" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

LessThan

Instances

Generic (LessThan n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => LessThan n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

type Rep (LessThan n)

Defined in Refined.Internal

type Rep (LessThan n) = D1 (MetaData "LessThan" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

GreaterThan

Instances

Generic (GreaterThan n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => GreaterThan n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

type Rep (GreaterThan n)

Defined in Refined.Internal

type Rep (GreaterThan n) = D1 (MetaData "GreaterThan" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

From

Instances

Generic (From n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => From n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

type Rep (From n)

Defined in Refined.Internal

type Rep (From n) = D1 (MetaData "From" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

To

Instances

Generic (To n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => To n -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

type Rep (To n)

Defined in Refined.Internal

type Rep (To n) = D1 (MetaData "To" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

FromTo

Instances

Generic (FromTo mn mx)

Defined in Refined.Internal

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => FromTo mn mx -> x -> RefineT m ()

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

type Rep (FromTo mn mx)

Defined in Refined.Internal

type Rep (FromTo mn mx) = D1 (MetaData "FromTo" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

NegativeFromTo

Instances

Generic (NegativeFromTo n m)

Defined in Refined.Internal

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

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

Defined in Refined.Internal

Methods

validate :: Monad m0 => NegativeFromTo n m -> x -> RefineT m0 ()

type Rep (NegativeFromTo n m)

Defined in Refined.Internal

type Rep (NegativeFromTo n m) = D1 (MetaData "NegativeFromTo" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

EqualTo

Instances

Generic (EqualTo n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => EqualTo n -> x -> RefineT m ()

type Rep (EqualTo n)

Defined in Refined.Internal

type Rep (EqualTo n) = D1 (MetaData "EqualTo" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

NotEqualTo

Instances

Generic (NotEqualTo n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => NotEqualTo n -> x -> RefineT m ()

type Rep (NotEqualTo n)

Defined in Refined.Internal

type Rep (NotEqualTo n) = D1 (MetaData "NotEqualTo" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

Odd

Instances

Generic Odd

Defined in Refined.Internal

Associated Types

type Rep Odd :: Type -> Type

Methods

from :: Odd -> Rep Odd x

to :: Rep Odd x -> Odd

Integral x => Predicate Odd x

Defined in Refined.Internal

Methods

validate :: Monad m => Odd -> x -> RefineT m ()

type Rep Odd

Defined in Refined.Internal

type Rep Odd = D1 (MetaData "Odd" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

Even

Instances

Generic Even

Defined in Refined.Internal

Associated Types

type Rep Even :: Type -> Type

Methods

from :: Even -> Rep Even x

to :: Rep Even x -> Even

Integral x => Predicate Even x

Defined in Refined.Internal

Methods

validate :: Monad m => Even -> x -> RefineT m ()

type Rep Even

Defined in Refined.Internal

type Rep Even = D1 (MetaData "Even" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

DivisibleBy

Instances

Generic (DivisibleBy n)

Defined in Refined.Internal

Associated Types

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

Methods

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

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

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

Defined in Refined.Internal

Methods

validate :: Monad m => DivisibleBy n -> x -> RefineT m ()

type Rep (DivisibleBy n)

Defined in Refined.Internal

type Rep (DivisibleBy n) = D1 (MetaData "DivisibleBy" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "DivisibleBy" PrefixI False) (U1 :: Type -> Type))

type Positive = GreaterThan 0

A Predicate ensuring that the value is greater than zero.

type NonPositive = To 0

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

type Negative = LessThan 0

A Predicate ensuring that the value is less than zero.

type NonNegative = From 0

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

type ZeroToOne = FromTo 0 1

An inclusive range of values from zero to one.

type NonZero = NotEqualTo 0

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

Foldable predicates

data SizeLessThan (n :: Nat)

A Predicate ensuring that the Foldable 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

Constructors

SizeLessThan

Instances

Generic (SizeLessThan n)

Defined in Refined.Internal

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) => Predicate (SizeLessThan n) (t a)

Defined in Refined.Internal

Methods

validate :: Monad m => SizeLessThan n -> t a -> RefineT m ()

type Rep (SizeLessThan n)

Defined in Refined.Internal

type Rep (SizeLessThan n) = D1 (MetaData "SizeLessThan" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "SizeLessThan" PrefixI False) (U1 :: Type -> Type))

data SizeGreaterThan (n :: Nat)

A Predicate ensuring that the Foldable 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

Constructors

SizeGreaterThan

Instances

Generic (SizeGreaterThan n)

Defined in Refined.Internal

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) => Predicate (SizeGreaterThan n) (t a)

Defined in Refined.Internal

Methods

validate :: Monad m => SizeGreaterThan n -> t a -> RefineT m ()

type Rep (SizeGreaterThan n)

Defined in Refined.Internal

type Rep (SizeGreaterThan n) = D1 (MetaData "SizeGreaterThan" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "SizeGreaterThan" PrefixI False) (U1 :: Type -> Type))

data SizeEqualTo (n :: Nat)

A Predicate ensuring that the Foldable 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

Constructors

SizeEqualTo

Instances

Generic (SizeEqualTo n)

Defined in Refined.Internal

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) => Predicate (SizeEqualTo n) (t a)

Defined in Refined.Internal

Methods

validate :: Monad m => SizeEqualTo n -> t a -> RefineT m ()

type Rep (SizeEqualTo n)

Defined in Refined.Internal

type Rep (SizeEqualTo n) = D1 (MetaData "SizeEqualTo" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" False) (C1 (MetaCons "SizeEqualTo" PrefixI False) (U1 :: Type -> Type))

type NonEmpty = SizeGreaterThan 0

A Predicate ensuring that the Foldable is non-empty.

IsList 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

Constructors

Ascending

Instances

Generic Ascending

Defined in Refined.Internal

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)

Defined in Refined.Internal

Methods

validate :: Monad m => Ascending -> t a -> RefineT m ()

type Rep Ascending

Defined in Refined.Internal

type Rep Ascending = D1 (MetaData "Ascending" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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

Constructors

Descending

Instances

Generic Descending

Defined in Refined.Internal

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)

Defined in Refined.Internal

Methods

validate :: Monad m => Descending -> t a -> RefineT m ()

type Rep Descending

Defined in Refined.Internal

type Rep Descending = D1 (MetaData "Descending" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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 guarunteed to satisy 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.

Minimal complete definition

Nothing

Methods

weaken :: Refined from x -> Refined to x

Instances

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

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

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

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)

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)

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.

strengthenM :: forall p p' x m. (Predicate p x, Predicate p' x, Monad m) => Refined p x -> RefineT m (Refined (p && p') x)

Strengthen a refinement by composing it with another inside of the RefineT monad.

Error handling

RefineException

data RefineException

An exception encoding the way in which a Predicate failed.

Constructors

RefineNotException !TypeRep

A RefineException for failures involving the Not predicate.

RefineAndException !TypeRep !(These RefineException RefineException)

A RefineException for failures involving the And predicate.

RefineOrException !TypeRep !RefineException !RefineException

A RefineException for failures involving the Or predicate.

RefineOtherException !TypeRep !(Doc Void)

A RefineException for failures involving all other predicates.

Instances

Show RefineException

Defined in Refined.Internal

Methods

showsPrec :: Int -> RefineException -> ShowS

show :: RefineException -> String

showList :: [RefineException] -> ShowS

Generic RefineException

Defined in Refined.Internal

Associated Types

type Rep RefineException :: Type -> Type

Methods

from :: RefineException -> Rep RefineException x

to :: Rep RefineException x -> RefineException

Exception RefineException

Encode a RefineException for use with Control.Exception.

Defined in Refined.Internal

Methods

toException :: RefineException -> SomeException

fromException :: SomeException -> Maybe RefineException

displayException :: RefineException -> String

Pretty RefineException

Pretty-print a RefineException.

Defined in Refined.Internal

Methods

pretty :: RefineException -> Doc ann

prettyList :: [RefineException] -> Doc ann

Monad m => MonadError RefineException (RefineT m)

Defined in Refined.Internal

Methods

throwError :: RefineException -> RefineT m a

catchError :: RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a

type Rep RefineException

Defined in Refined.Internal

type Rep RefineException = D1 (MetaData "RefineException" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" 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 "RefineOtherException" PrefixI True) (S1 (MetaSel (Just "_RefineException_typeRep") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 TypeRep) :*: S1 (MetaSel (Just "_RefineException_message") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Doc Void)))))

displayRefineException :: RefineException -> Doc ann

Display a RefineException as a Doc ann

RefineT and RefineM

data RefineT m a

A monad transformer that adds RefineExceptions to other monads.

The pure and return functions yield computations that produce the given value, while >>= sequences two subcomputations, exiting on the first RefineException.

Instances

MonadTrans RefineT

Defined in Refined.Internal

Methods

lift :: Monad m => m a -> RefineT m a

Monad m => MonadError RefineException (RefineT m)

Defined in Refined.Internal

Methods

throwError :: RefineException -> RefineT m a

catchError :: RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a

Monad m => Monad (RefineT m)

Defined in Refined.Internal

Methods

(>>=) :: RefineT m a -> (a -> RefineT m b) -> RefineT m b

(>>) :: RefineT m a -> RefineT m b -> RefineT m b

return :: a -> RefineT m a

fail :: String -> RefineT m a

Functor m => Functor (RefineT m)

Defined in Refined.Internal

Methods

fmap :: (a -> b) -> RefineT m a -> RefineT m b

(<$) :: a -> RefineT m b -> RefineT m a

MonadFix m => MonadFix (RefineT m)

Defined in Refined.Internal

Methods

mfix :: (a -> RefineT m a) -> RefineT m a

Monad m => Applicative (RefineT m)

Defined in Refined.Internal

Methods

pure :: a -> RefineT m a

(<*>) :: RefineT m (a -> b) -> RefineT m a -> RefineT m b

liftA2 :: (a -> b -> c) -> RefineT m a -> RefineT m b -> RefineT m c

(*>) :: RefineT m a -> RefineT m b -> RefineT m b

(<*) :: RefineT m a -> RefineT m b -> RefineT m a

Generic1 (RefineT m :: Type -> Type)

Defined in Refined.Internal

Associated Types

type Rep1 (RefineT m) :: k -> Type

Methods

from1 :: RefineT m a -> Rep1 (RefineT m) a

to1 :: Rep1 (RefineT m) a -> RefineT m a

Generic (RefineT m a)

Defined in Refined.Internal

Associated Types

type Rep (RefineT m a) :: Type -> Type

Methods

from :: RefineT m a -> Rep (RefineT m a) x

to :: Rep (RefineT m a) x -> RefineT m a

type Rep1 (RefineT m :: Type -> Type)

Defined in Refined.Internal

type Rep1 (RefineT m :: Type -> Type) = D1 (MetaData "RefineT" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" True) (C1 (MetaCons "RefineT" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 (ExceptT RefineException m))))

type Rep (RefineT m a)

Defined in Refined.Internal

type Rep (RefineT m a) = D1 (MetaData "RefineT" "Refined.Internal" "refined-0.4.4-7xXnhN9HJ7XByi1PQY08Xe" True) (C1 (MetaCons "RefineT" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ExceptT RefineException m a))))

runRefineT :: RefineT m a -> m (Either RefineException a)

The inverse of RefineT.

exceptRefine :: Monad m => Either RefineException a -> RefineT m a

Constructor for computations in the RefineT movie. (The inverse of runRefineT).

mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b

Map the unwrapped computation using the given function.

runRefineT (mapRefineT f m) = f (runRefineT m)

type RefineM a = RefineT Identity a

RefineM a is equivalent to RefineT Identity a for any type a.

refineM :: Either RefineException a -> RefineM a

Constructs a computation in the RefineM monad. (The inverse of runRefineM).

runRefineM :: RefineM a -> Either RefineException a

Run a monadic action of type RefineM a, yielding an Either RefineException a.

This is just defined as runIdentity . runRefineT.

throwRefine :: Monad m => RefineException -> RefineT m a

One can use throwRefine inside of a monadic context to begin processing a RefineException.

catchRefine :: Monad m => RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a

A handler function to handle previous RefineExceptions and return to normal execution. A common idiom is:

 do { action1; action2; action3 } `catchRefine' handler

where the action functions can call throwRefine. Note that handler and the do-block must have the same return type.

throwRefineOtherException

Arguments

:: Monad m

=> TypeRep

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

-> Doc Void

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

-> RefineT m a

A handler for a RefineException.

throwRefineOtherException is useful for defining what behaviour validate should have in the event of a predicate failure.

Re-Exports

pretty :: Pretty a => a -> Doc ann

>>> pretty 1 <+> pretty "hello" <+> pretty 1.234
1 hello 1.234