Safe Haskell	None
Language	Haskell2010

Refined

Contents

Predicate Interface
Standard Predicates
- Logical
- Numeric

Synopsis

Documentation

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

Eq x => Eq (Refined p x) Source
(Data p, Data x) => Data (Refined p x) Source
Ord x => Ord (Refined p x) Source
(Read x, Predicate p x) => Read (Refined p x) Source
Show x => Show (Refined p x) Source
Generic (Refined p x) Source
Lift x => Lift (Refined p x) Source
type Rep (Refined p x) Source

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

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

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

Constructs a Refined value with checking at compile-time using Template Haskell. E.g.,

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

unrefine :: Refined p x -> x Source

Extracts the refined value.

Predicate Interface

class Predicate p x where Source

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

Methods

validate :: p -> x -> Maybe String Source

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

Instances

(Ord x, Num x, KnownNat n) => Predicate (EqualTo n) x Source
(Ord x, Num x, KnownNat n) => Predicate (To n) x Source
(Ord x, Num x, KnownNat n) => Predicate (From n) x Source
(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x Source
(Ord x, Num x, KnownNat n) => Predicate (LessThan n) x Source
Predicate r x => Predicate (Not r) x Source
(Ord x, Num x, KnownNat mn, KnownNat mx, (<=) mn mx) => Predicate (FromTo mn mx) x Source
(Predicate l x, Predicate r x) => Predicate (Or l r) x Source
(Predicate l x, Predicate r x) => Predicate (And l r) x Source