refined-0.1.1.0: Refinement types with static and runtime checking

Safe HaskellNone
LanguageHaskell2010

Refined

Contents

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) 
(Data p, Data x) => Data (Refined p x) 
Ord x => Ord (Refined p x) 
(Read x, Predicate p x) => Read (Refined p x) 
Show x => Show (Refined p x) 
Generic (Refined p x) 
Lift x => Lift (Refined p x) 
Typeable (* -> * -> *) Refined 
type Rep (Refined p x) 

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

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

refineTH :: forall p x. (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 
(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x 
(Ord x, Num x, KnownNat n) => Predicate (LessThan n) x 
Predicate r x => Predicate (Not r) x 
(Predicate l x, Predicate r x) => Predicate (Or l r) x 
(Predicate l x, Predicate r x) => Predicate (And l r) x 

Standard Predicates

Logical

data Not r Source

A logical negation of a predicate.

Instances

Predicate r x => Predicate (Not r) x 

data And l r Source

A logical conjunction predicate, composed of two other predicates.

Instances

(Predicate l x, Predicate r x) => Predicate (And l r) x 

data Or l r Source

A logical disjunction predicate, composed of two other predicates.

Instances

(Predicate l x, Predicate r x) => Predicate (Or l r) x 

Numeric

data LessThan n Source

A predicate, which ensures that a value is less than the specified type-level number.

Instances

(Ord x, Num x, KnownNat n) => Predicate (LessThan n) x 

data GreaterThan n Source

A predicate, which ensures that a value is greater than the specified type-level number.

Instances

(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x 

data EqualTo n Source

A predicate, which ensures that a value equals to the specified type-level number.

Instances

(Ord x, Num x, KnownNat n) => Predicate (EqualTo n) x 

type Positive = GreaterThan 0 Source

A predicate, which ensures that the value is greater than zero.

type Negative = LessThan 0 Source

A predicate, which ensures that the value is less than zero.

type ZeroToOne = And (Not (LessThan 0)) (Not (GreaterThan 1)) Source

A range of values from zero to one, including both.