refined-0.4: Refinement types with static and runtime checking

Safe HaskellNone
LanguageHaskell2010

Refined

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/

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.

Synopsis

Refined

data Refined p x Source #

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

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.

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.

Re-Exports

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

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