| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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/
Synopsis
- data Refined p x
- refine :: Predicate p x => x -> Either RefineException (Refined p x)
- refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
- refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)
- refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x)
- unsafeRefine :: Predicate p x => x -> Refined p x
- refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))
- unrefine :: Refined p x -> x
- class Typeable p => Predicate p x where
- data Not p
- data And l r
- type (&&) = And
- data Or l r
- type (||) = Or
- data LessThan (n :: Nat)
- data GreaterThan (n :: Nat)
- data From (n :: Nat)
- data To (n :: Nat)
- data FromTo (mn :: Nat) (mx :: Nat)
- data EqualTo (n :: Nat)
- data NotEqualTo (n :: Nat)
- type Positive = GreaterThan 0
- type NonPositive = To 0
- type Negative = LessThan 0
- type NonNegative = From 0
- type ZeroToOne = FromTo 0 1
- type NonZero = NotEqualTo 0
- data SizeLessThan (n :: Nat)
- data SizeGreaterThan (n :: Nat)
- data SizeEqualTo (n :: Nat)
- type NonEmpty = SizeGreaterThan 0
- data Ascending
- data Descending
- class Weaken from to where
- andLeft :: Refined (And l r) x -> Refined l x
- andRight :: Refined (And l r) x -> Refined r x
- leftOr :: Refined l x -> Refined (Or l r) x
- rightOr :: Refined r x -> Refined (Or l r) x
- data RefineException
- displayRefineException :: RefineException -> Doc ann
- data RefineT m a
- runRefineT :: RefineT m a -> m (Either RefineException a)
- mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b
- type RefineM a = RefineT Identity a
- refineM :: Either RefineException a -> RefineM a
- runRefineM :: RefineM a -> Either RefineException a
- throwRefine :: Monad m => RefineException -> RefineT m a
- catchRefine :: Monad m => RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a
- throwRefineOtherException :: Monad m => TypeRep -> Doc Void -> RefineT m a
Refined
A refinement type, which wraps a value of type x,
ensuring that it satisfies a type-level predicate p.
The only ways that this library provides to construct
a value of type Refined are with the 'refine-' family
of functions, because the use of the newtype constructor
gets around the checking of the predicate. This restriction
on the user makes unrefine safe.
If you would really like to
construct a Refined value without checking the predicate,
use unsafeCoerce.
Instances
| Foldable (Refined p) # | |
Defined in Refined 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] # 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 # | |
| Eq x => Eq (Refined p x) # | |
| Ord x => Ord (Refined p x) # | |
Defined in Refined | |
| (Read x, Predicate p x) => Read (Refined p x) # | |
| Show x => Show (Refined p x) # | |
| Lift x => Lift (Refined p x) # | |
Creation
refine :: Predicate p x => x -> Either RefineException (Refined p x) #
A smart constructor of a Refined value.
Checks the input value at runtime.
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) #
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x) #
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.
unsafeRefine :: Predicate p x => x -> Refined p x #
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 IntRefined 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.
Consumption
Predicate
class Typeable p => Predicate p x where #
A typeclass which defines a runtime interpretation of
a type-level predicate p for type x.
Minimal complete definition
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
| (IsList t, Ord (Item t)) => Predicate Descending t # | |
| (IsList t, Ord (Item t)) => Predicate Ascending t # | |
| (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x # | |
| (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x # | |
| (Ord x, Num x, KnownNat n) => Predicate (To n) x # | |
| (Ord x, Num x, KnownNat n) => Predicate (From n) x # | |
| (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x # | |
| (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x # | |
| (Predicate p x, Typeable p) => Predicate (Not p) x # | |
| (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) # | |
| (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) # | |
| (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) # | |
| (Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx) x # | |
| (Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (Or l r) x # | |
| (Predicate l x, Predicate r x, Typeable l, Typeable r) => Predicate (And l r) x # | |
Logical predicates
The negation of a predicate.
The conjunction of two predicates.
The disjunction of two predicates.
Numeric predicates
A Predicate ensuring that the value is less than the
specified type-level number.
data GreaterThan (n :: Nat) #
A Predicate ensuring that the value is greater than the
specified type-level number.
Instances
| (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x # | |
| m <= n => Weaken (GreaterThan n) (From m) # | |
| m <= n => Weaken (GreaterThan n) (GreaterThan m) # | |
Defined in Refined Methods weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x # | |
A Predicate ensuring that the value is greater than or equal to the
specified type-level number.
A Predicate ensuring that the value is less than or equal to the
specified type-level number.
data FromTo (mn :: Nat) (mx :: Nat) #
A Predicate ensuring that the value is within an inclusive range.
A Predicate ensuring that the value is equal to the specified
type-level number n.
data NotEqualTo (n :: Nat) #
A Predicate ensuring that the value is not equal to the specified
type-level number n.
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 NonNegative = From 0 #
A Predicate ensuring that the value is greater than or equal to zero.
type NonZero = NotEqualTo 0 #
A Predicate ensuring that the value is not equal to zero.
Foldable predicates
data SizeLessThan (n :: Nat) #
data SizeGreaterThan (n :: Nat) #
data SizeEqualTo (n :: Nat) #
type NonEmpty = SizeGreaterThan 0 #
IsList predicates
data Descending #
Weakening
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.
Instances
| n <= m => Weaken (To n) (To m) # | |
| m <= n => Weaken (From n) (From m) # | |
| m <= n => Weaken (GreaterThan n) (From m) # | |
| m <= n => Weaken (GreaterThan n) (GreaterThan m) # | |
Defined in Refined Methods weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x # | |
| n <= m => Weaken (LessThan n) (To m) # | |
| n <= m => Weaken (LessThan n) (LessThan m) # | |
| m <= q => Weaken (FromTo n m) (To q) # | |
| p <= n => Weaken (FromTo n m) (From p) # | |
| (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) # | |
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)
Error handling
RefineException
data RefineException #
An exception encoding the way in which a Predicate failed.
Constructors
| RefineNotException !TypeRep | A |
| RefineAndException !TypeRep !(These RefineException RefineException) | A |
| RefineOrException !TypeRep !RefineException !RefineException | A |
| RefineOtherException !TypeRep !(Doc Void) | A |
Instances
displayRefineException :: RefineException -> Doc ann #
Display a RefineException as a Doc ann
RefineT and RefineM
A monad transformer that adds RefineException
The purereturn>>=RefineException
Instances
| MonadTrans RefineT # | |
| Monad m => MonadError RefineException (RefineT m) # | |
Defined in Refined Methods throwError :: RefineException -> RefineT m a # catchError :: RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a # | |
| Monad m => Monad (RefineT m) # | |
| Functor m => Functor (RefineT m) # | |
| MonadFix m => MonadFix (RefineT m) # | |
| Monad m => Applicative (RefineT m) # | |
| Generic1 (RefineT m :: * -> *) # | |
| Generic (RefineT m a) # | |
| type Rep1 (RefineT m :: * -> *) # | |
Defined in Refined | |
| type Rep (RefineT m a) # | |
runRefineT :: RefineT m a -> m (Either RefineException a) #
The inverse of RefineT
mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b #
Map the unwrapped computation using the given function.
runRefineT(mapRefineTf m) = f (runRefineTm)
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 aEither RefineException a
This is just defined as runIdentity . runRefineT
throwRefine :: Monad m => RefineException -> RefineT m a #
One can use throwRefineRefineException
catchRefine :: Monad m => RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a #
A handler function to handle previous RefineException
do { action1; action2; action3 } `catchRefine' handlerwhere the action functions can call throwRefine
Arguments
| :: Monad m | |
| => TypeRep | The |
| -> Doc Void | A |
| -> 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.