Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- newtype Refined p x = Refined 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)
- 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 IdPred
- 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 NegativeFromTo (n :: Nat) (m :: Nat)
- 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
- (|>) :: a -> (a -> b) -> b
- (.>) :: (a -> b) -> (b -> c) -> a -> c
- pretty :: Pretty a => a -> Doc ann

`Refined`

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

,
ensuring that it satisfies a type-level predicate `p`

.

Refined x |

## Instances

Foldable (Refined p) Source # | |

Defined in Refined.Internal 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) Source # | |

Ord x => Ord (Refined p x) Source # | |

Defined in Refined.Internal | |

(Read x, Predicate p x) => Read (Refined p x) Source # | This instance makes sure to check the refinement. |

Show x => Show (Refined p x) Source # | |

Lift x => Lift (Refined p x) Source # | |

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

(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source # | |

Defined in Refined.Orphan.Aeson | |

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

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

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:

`>>>`

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

Here's an example of an invalid value:

`>>>`

<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`$$(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

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

.

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

# Logical predicates

The negation of a predicate.

The conjunction of two predicates.

The disjunction of two predicates.

# Identity predicate

A predicate which is satisfied for all types.

# Numeric predicates

data LessThan (n :: Nat) Source #

A `Predicate`

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

data GreaterThan (n :: Nat) Source #

A `Predicate`

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

## Instances

Generic (GreaterThan n) Source # | |

Defined in Refined.Internal type Rep (GreaterThan n) :: Type -> Type # 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 # | |

Defined in Refined.Internal | |

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

Defined in Refined.Internal | |

m <= n => Weaken (GreaterThan n) (GreaterThan m) Source # | |

Defined in Refined.Internal weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x Source # | |

type Rep (GreaterThan n) Source # | |

Defined in Refined.Internal |

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

A `Predicate`

ensuring that the value is within an inclusive range.

## Instances

Generic (FromTo mn mx) Source # | |

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

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

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

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

type Rep (FromTo mn mx) Source # | |

data EqualTo (n :: Nat) Source #

A `Predicate`

ensuring that the value is equal to the specified
type-level number `n`

.

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

Defined in Refined.Internal type Rep (NotEqualTo n) :: Type -> Type # 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 # | |

Defined in Refined.Internal | |

type Rep (NotEqualTo n) Source # | |

Defined in Refined.Internal |

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 NonNegative = From 0 Source #

A `Predicate`

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

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

Defined in Refined.Internal type Rep (NegativeFromTo n m) :: Type -> Type # 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 # | |

Defined in Refined.Internal | |

type Rep (NegativeFromTo n m) Source # | |

Defined in Refined.Internal |

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

Defined in Refined.Internal type Rep (SizeLessThan n) :: Type -> Type # from :: SizeLessThan n -> Rep (SizeLessThan n) x # to :: Rep (SizeLessThan n) x -> SizeLessThan n # | |

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

Defined in Refined.Internal | |

type Rep (SizeLessThan n) Source # | |

Defined in Refined.Internal |

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

Defined in Refined.Internal type Rep (SizeGreaterThan n) :: Type -> Type # from :: SizeGreaterThan n -> Rep (SizeGreaterThan n) x # to :: Rep (SizeGreaterThan n) x -> SizeGreaterThan n # | |

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

Defined in Refined.Internal | |

type Rep (SizeGreaterThan n) Source # | |

Defined in Refined.Internal |

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

Defined in Refined.Internal type Rep (SizeEqualTo n) :: Type -> Type # from :: SizeEqualTo n -> Rep (SizeEqualTo n) x # to :: Rep (SizeEqualTo n) x -> SizeEqualTo n # | |

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

Defined in Refined.Internal | |

type Rep (SizeEqualTo n) Source # | |

Defined in Refined.Internal |

# IsList predicates

data Descending Source #

## Instances

Generic Descending Source # | |

Defined in Refined.Internal type Rep Descending :: Type -> Type # from :: Descending -> Rep Descending x # to :: Rep Descending x -> Descending # | |

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

Defined in Refined.Internal | |

type Rep Descending Source # | |

Defined in Refined.Internal |

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

Nothing

## Instances

n <= m => Weaken (To n) (To m) Source # | |

m <= n => Weaken (From n) (From m) Source # | |

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

Defined in Refined.Internal | |

m <= n => Weaken (GreaterThan n) (GreaterThan m) Source # | |

Defined in Refined.Internal weaken :: Refined (GreaterThan n) x -> Refined (GreaterThan m) x Source # | |

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

n <= m => Weaken (LessThan n) (LessThan m) Source # | |

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

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

(p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) 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.

RefineNotException !TypeRep | A |

RefineAndException !TypeRep !(These RefineException RefineException) | A |

RefineOrException !TypeRep !RefineException !RefineException | A |

RefineOtherException !TypeRep !(Doc Void) | A |

## Instances

displayRefineException :: RefineException -> Doc ann Source #

Display a `RefineException`

as a `Doc`

ann

`RefineT`

and `RefineM`

A monad transformer that adds

s to other monads.`RefineException`

The

and `pure`

functions yield computations that produce
the given value, while `return`

sequences two subcomputations, exiting
on the first `>>=`

.`RefineException`

## Instances

MonadTrans RefineT Source # | |

Defined in Refined.Internal | |

Monad m => MonadError RefineException (RefineT m) Source # | |

Defined in Refined.Internal throwError :: RefineException -> RefineT m a # catchError :: RefineT m a -> (RefineException -> RefineT m a) -> RefineT m a # | |

Monad m => Monad (RefineT m) Source # | |

Functor m => Functor (RefineT m) Source # | |

MonadFix m => MonadFix (RefineT m) Source # | |

Defined in Refined.Internal | |

Monad m => Applicative (RefineT m) Source # | |

Generic1 (RefineT m :: Type -> Type) Source # | |

Generic (RefineT m a) Source # | |

type Rep1 (RefineT m :: Type -> Type) Source # | |

Defined in Refined.Internal | |

type Rep (RefineT m a) Source # | |

Defined in Refined.Internal type Rep (RefineT m a) = D1 (MetaData "RefineT" "Refined.Internal" "refined-0.4.1-EYHUGtdk1BQEdvdCeXV31J" 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)

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

,
yielding an `RefineM`

a

.`Either`

`RefineException`

a

This is just defined as

.`runIdentity`

`.`

`runRefineT`

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

One can use

inside of a monadic
context to begin processing a `throwRefine`

.`RefineException`

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

A handler function to handle previous

s
and return to normal execution. A common idiom is:`RefineException`

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

handler

where the action functions can call

. Note that
handler and the do-block must have the same return type.`throwRefine`

throwRefineOtherException Source #

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

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

Helper function, stolen from the `flow`

package.