refined-0.4: Refinement types with static and runtime checking

Safe HaskellNone
LanguageHaskell2010

Refined.Internal

Contents

Description

In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.

This library allows one to capture the idea of a refinement type using the Refined type. A Refined p x wraps a value of type x, ensuring that it satisfies a type-level predicate p.

A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/

Synopsis

Refined

newtype Refined p x Source #

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

Constructors

Refined x 
Instances
Foldable (Refined p) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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

This instance makes sure to check the refinement.

Instance details

Defined in Refined.Internal

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

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) Source # 
Instance details

Defined in Refined.Internal

Methods

lift :: Refined p x -> Q Exp #

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

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) Source # 
Instance details

Defined in Refined.Orphan.Aeson

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

Defined in Refined.Orphan.Aeson

Creation

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

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

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

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

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

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

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

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

refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (Refined p x)) Source #

Constructs a Refined value at compile-time using -XTemplateHaskell.

For example:

>>> $$(refineTH 23) :: Refined Positive Int
Refined 23

Here's an example of an invalid value:

>>> $$(refineTH 0) :: Refined Positive Int
<interactive>:6:4:
    Value is not greater than 0
    In the Template Haskell splice $$(refineTH 0)
    In the expression: $$(refineTH 0) :: Refined Positive Int
    In an equation for ‘it’:
        it = $$(refineTH 0) :: Refined Positive Int

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/

Consumption

unrefine :: Refined p x -> x Source #

Extracts the refined value.

Predicate

class Typeable p => Predicate p x where Source #

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

Methods

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

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

Instances
Predicate IdPred x Source # 
Instance details

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

(Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Ord x, Num x, KnownNat n) => Predicate (To n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Ord x, Num x, KnownNat n) => Predicate (From n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Ord x, Num x, KnownNat n) => Predicate (LessThan n) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Predicate p x, Typeable p) => Predicate (Not p) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Ord x, Num x, KnownNat n, KnownNat m, n <= m) => Predicate (NegativeFromTo n m) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

Methods

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

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (Or l r) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

(Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (And l r) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

Logical predicates

data Not p Source #

The negation of a predicate.

Instances
Generic (Not p) Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (Not p) Source # 
Instance details

Defined in Refined.Internal

type Rep (Not p) = D1 (MetaData "Not" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)
type Rep1 Not Source # 
Instance details

Defined in Refined.Internal

type Rep1 Not = D1 (MetaData "Not" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data And l r Source #

The conjunction of two predicates.

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

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) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

type Rep1 (And l :: Type -> Type) = D1 (MetaData "And" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)
type Rep (And l r) Source # 
Instance details

Defined in Refined.Internal

type Rep (And l r) = D1 (MetaData "And" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

type (&&) = And infixr 3 Source #

The conjunction of two predicates.

data Or l r Source #

The disjunction of two predicates.

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

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) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

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

Defined in Refined.Internal

type Rep1 (Or l :: Type -> Type) = D1 (MetaData "Or" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)
type Rep (Or l r) Source # 
Instance details

Defined in Refined.Internal

type Rep (Or l r) = D1 (MetaData "Or" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

type (||) = Or infixr 2 Source #

The disjunction of two predicates.

Identity predicate

data IdPred Source #

A predicate which is satisfied for all types.

Instances
Generic IdPred Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep IdPred Source # 
Instance details

Defined in Refined.Internal

type Rep IdPred = D1 (MetaData "IdPred" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

Numeric predicates

data LessThan (n :: Nat) Source #

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

Instances
Generic (LessThan n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

n <= m => Weaken (LessThan n) (To m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

n <= m => Weaken (LessThan n) (LessThan m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (LessThan n) Source # 
Instance details

Defined in Refined.Internal

type Rep (LessThan n) = D1 (MetaData "LessThan" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data GreaterThan (n :: Nat) Source #

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

Instances
Generic (GreaterThan n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (GreaterThan n) (From m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (GreaterThan n) (GreaterThan m) Source # 
Instance details

Defined in Refined.Internal

type Rep (GreaterThan n) Source # 
Instance details

Defined in Refined.Internal

type Rep (GreaterThan n) = D1 (MetaData "GreaterThan" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data From (n :: Nat) Source #

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

Instances
Generic (From n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (From n) (From m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (GreaterThan n) (From m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

p <= n => Weaken (FromTo n m) (From p) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (From n) Source # 
Instance details

Defined in Refined.Internal

type Rep (From n) = D1 (MetaData "From" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data To (n :: Nat) Source #

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

Instances
Generic (To n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

n <= m => Weaken (To n) (To m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

n <= m => Weaken (LessThan n) (To m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= q => Weaken (FromTo n m) (To q) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (To n) Source # 
Instance details

Defined in Refined.Internal

type Rep (To n) = D1 (MetaData "To" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

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

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

Instances
Generic (FromTo mn mx) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= q => Weaken (FromTo n m) (To q) Source # 
Instance details

Defined in Refined.Internal

Methods

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

p <= n => Weaken (FromTo n m) (From p) Source # 
Instance details

Defined in Refined.Internal

Methods

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

(p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (FromTo mn mx) Source # 
Instance details

Defined in Refined.Internal

type Rep (FromTo mn mx) = D1 (MetaData "FromTo" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data EqualTo (n :: Nat) Source #

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

Instances
Generic (EqualTo n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (EqualTo n) Source # 
Instance details

Defined in Refined.Internal

type Rep (EqualTo n) = D1 (MetaData "EqualTo" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data NotEqualTo (n :: Nat) Source #

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

Instances
Generic (NotEqualTo n) Source # 
Instance details

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (NotEqualTo n) Source # 
Instance details

Defined in Refined.Internal

type Rep (NotEqualTo n) = D1 (MetaData "NotEqualTo" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

type Positive = GreaterThan 0 Source #

A Predicate ensuring that the value is greater than zero.

type NonPositive = To 0 Source #

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

type Negative = LessThan 0 Source #

A Predicate ensuring that the value is less than zero.

type NonNegative = From 0 Source #

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

type ZeroToOne = FromTo 0 1 Source #

An inclusive range of values from zero to one.

type NonZero = NotEqualTo 0 Source #

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

data NegativeFromTo (n :: Nat) (m :: Nat) Source #

A Predicate ensuring that the value is greater or equal than a negative number specified as a type-level (positive) number n and less than a type-level (positive) number m.

Instances
Generic (NegativeFromTo n m) Source # 
Instance details

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, n <= m) => Predicate (NegativeFromTo n m) x Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (NegativeFromTo n m) Source # 
Instance details

Defined in Refined.Internal

type Rep (NegativeFromTo n m) = D1 (MetaData "NegativeFromTo" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

Foldable predicates

data SizeLessThan (n :: Nat) Source #

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

Instances
Generic (SizeLessThan n) Source # 
Instance details

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) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (SizeLessThan n) Source # 
Instance details

Defined in Refined.Internal

type Rep (SizeLessThan n) = D1 (MetaData "SizeLessThan" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data SizeGreaterThan (n :: Nat) Source #

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

Instances
Generic (SizeGreaterThan n) Source # 
Instance details

Defined in Refined.Internal

Associated Types

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

(Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (SizeGreaterThan n) Source # 
Instance details

Defined in Refined.Internal

type Rep (SizeGreaterThan n) = D1 (MetaData "SizeGreaterThan" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data SizeEqualTo (n :: Nat) Source #

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

Instances
Generic (SizeEqualTo n) Source # 
Instance details

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) Source # 
Instance details

Defined in Refined.Internal

Methods

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

type Rep (SizeEqualTo n) Source # 
Instance details

Defined in Refined.Internal

type Rep (SizeEqualTo n) = D1 (MetaData "SizeEqualTo" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

type NonEmpty = SizeGreaterThan 0 Source #

A Predicate ensuring that the Foldable is non-empty.

IsList predicates

data Ascending Source #

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

Instances
Generic Ascending Source # 
Instance details

Defined in Refined.Internal

Associated Types

type Rep Ascending :: Type -> Type #

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

Defined in Refined.Internal

Methods

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

type Rep Ascending Source # 
Instance details

Defined in Refined.Internal

type Rep Ascending = D1 (MetaData "Ascending" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

data Descending Source #

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

Instances
Generic Descending Source # 
Instance details

Defined in Refined.Internal

Associated Types

type Rep Descending :: Type -> Type #

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

Defined in Refined.Internal

Methods

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

type Rep Descending Source # 
Instance details

Defined in Refined.Internal

type Rep Descending = D1 (MetaData "Descending" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) (V1 :: Type -> Type)

Weakening

class Weaken from to where Source #

A typeclass containing "safe" conversions between refined predicates where the target is weaker than the source: that is, all values that satisfy the first predicate will be 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 Source #

Instances
n <= m => Weaken (To n) (To m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (From n) (From m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (GreaterThan n) (From m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= n => Weaken (GreaterThan n) (GreaterThan m) Source # 
Instance details

Defined in Refined.Internal

n <= m => Weaken (LessThan n) (To m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

n <= m => Weaken (LessThan n) (LessThan m) Source # 
Instance details

Defined in Refined.Internal

Methods

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

m <= q => Weaken (FromTo n m) (To q) Source # 
Instance details

Defined in Refined.Internal

Methods

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

p <= n => Weaken (FromTo n m) (From p) Source # 
Instance details

Defined in Refined.Internal

Methods

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

(p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) Source # 
Instance details

Defined in Refined.Internal

Methods

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

andLeft :: Refined (And l r) x -> Refined l x Source #

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

instance Weaken (And l r) l

andRight :: Refined (And l r) x -> Refined r x Source #

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

instance Weaken (And l r) r

leftOr :: Refined l x -> Refined (Or l r) x Source #

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

instance Weaken l (Or l r)

rightOr :: Refined r x -> Refined (Or l r) x Source #

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

instance Weaken r (Or l r)

Error handling

RefineException

data RefineException Source #

An exception encoding the way in which a Predicate failed.

Constructors

RefineNotException !TypeRep !RefineException

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 Source # 
Instance details

Defined in Refined.Internal

Generic RefineException Source # 
Instance details

Defined in Refined.Internal

Associated Types

type Rep RefineException :: Type -> Type #

Exception RefineException Source #

Encode a RefineException for use with Control.Exception.

Instance details

Defined in Refined.Internal

Pretty RefineException Source #

Pretty-print a RefineException.

Instance details

Defined in Refined.Internal

Monad m => MonadError RefineException (RefineT m) Source # 
Instance details

Defined in Refined.Internal

type Rep RefineException Source # 
Instance details

Defined in Refined.Internal

type Rep RefineException = D1 (MetaData "RefineException" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" False) ((C1 (MetaCons "RefineNotException" PrefixI True) (S1 (MetaSel (Just "_RefineException_typeRep") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 TypeRep) :*: S1 (MetaSel (Just "_RefineException_notChild") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 RefineException)) :+: 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)))))

RefineT and RefineM

data RefineT m a Source #

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 Source # 
Instance details

Defined in Refined.Internal

Methods

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

Monad m => MonadError RefineException (RefineT m) Source # 
Instance details

Defined in Refined.Internal

Monad m => Monad (RefineT m) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Refined.Internal

Methods

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

Monad m => Applicative (RefineT m) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Refined.Internal

type Rep1 (RefineT m :: Type -> Type) = D1 (MetaData "RefineT" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" True) (C1 (MetaCons "RefineT" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 (ExceptT RefineException m))))
type Rep (RefineT m a) Source # 
Instance details

Defined in Refined.Internal

type Rep (RefineT m a) = D1 (MetaData "RefineT" "Refined.Internal" "refined-0.4-1Ly2nnRfmnJ9IeL6JEZ6Q" 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) Source #

The inverse of RefineT.

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

Map the unwrapped computation using the given function.

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

type RefineM a = RefineT Identity a Source #

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

refineM :: Either RefineException a -> RefineM a Source #

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

runRefineM :: RefineM a -> Either RefineException a Source #

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

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

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

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.

(|>) :: a -> (a -> b) -> b infixl 0 Source #

Helper function, stolen from the flow package.

(.>) :: (a -> b) -> (b -> c) -> a -> c infixl 9 Source #

Helper function, stolen from the flow package.

Re-Exports

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

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