Safe Haskell	None
Language	Haskell2010

Refined

Contents

Predicate Interface
Standard Predicates
- Logical
- Numeric

Synopsis

Documentation

data Refined p x #

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) #
Methods (==) :: Refined p x -> Refined p x -> Bool # (/=) :: Refined p x -> Refined p x -> Bool #
(Data x, Data p) => Data (Refined p x) #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Refined p x -> c (Refined p x) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Refined p x) # toConstr :: Refined p x -> Constr # dataTypeOf :: Refined p x -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Refined p x)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Refined p x)) # gmapT :: (forall b. Data b => b -> b) -> Refined p x -> Refined p x # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Refined p x -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Refined p x -> r # gmapQ :: (forall d. Data d => d -> u) -> Refined p x -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Refined p x -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Refined p x -> m (Refined p x) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Refined p x -> m (Refined p x) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Refined p x -> m (Refined p x) #
Ord x => Ord (Refined p x) #
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) #
Methods readsPrec :: Int -> ReadS (Refined p x) # readList :: ReadS [Refined p x] # readPrec :: ReadPrec (Refined p x) # readListPrec :: ReadPrec [Refined p x] #
Show x => Show (Refined p x) #
Methods showsPrec :: Int -> Refined p x -> ShowS # show :: Refined p x -> String # showList :: [Refined p x] -> ShowS #
Generic (Refined p x) #
Associated Types type Rep (Refined p x) :: * -> * # Methods from :: Refined p x -> Rep (Refined p x) x # to :: Rep (Refined p x) x -> Refined p x #
Lift x => Lift (Refined p x) #
Methods lift :: Refined p x -> Q Exp #
type Rep (Refined p x) #
type Rep (Refined p x) = D1 * (MetaData "Refined" "Refined" "refined-0.1.2.1-Da35yIBiwn5CckyvfHksQ2" True) (C1 * (MetaCons "Refined" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * x)))

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

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

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 #

Extracts the refined value.

Predicate Interface

class Predicate p x where #

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

Minimal complete definition

validate

Methods

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

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 #
Methods validate :: EqualTo n -> x -> Maybe String #
(Ord x, Num x, KnownNat n) => Predicate (To n) x #
Methods validate :: To n -> x -> Maybe String #
(Ord x, Num x, KnownNat n) => Predicate (From n) x #
Methods validate :: From n -> x -> Maybe String #
(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x #
Methods validate :: GreaterThan n -> x -> Maybe String #
(Ord x, Num x, KnownNat n) => Predicate (LessThan n) x #
Methods validate :: LessThan n -> x -> Maybe String #
Predicate r x => Predicate (Not r) x #
Methods validate :: Not r -> x -> Maybe String #
(Ord x, Num x, KnownNat mn, KnownNat mx, (<=) mn mx) => Predicate (FromTo mn mx) x #
Methods validate :: FromTo mn mx -> x -> Maybe String #
(Predicate l x, Predicate r x) => Predicate (Or l r) x #
Methods validate :: Or l r -> x -> Maybe String #
(Predicate l x, Predicate r x) => Predicate (And l r) x #
Methods validate :: And l r -> x -> Maybe String #

Standard Predicates

Logical

data Not r #

A logical negation of a predicate.

Instances

Predicate r x => Predicate (Not r) x #
Methods validate :: Not r -> x -> Maybe String #

data And l r #

A logical conjunction predicate, composed of two other predicates.

Instances

(Predicate l x, Predicate r x) => Predicate (And l r) x #
Methods validate :: And l r -> x -> Maybe String #

data Or l r #

A logical disjunction predicate, composed of two other predicates.

Instances

(Predicate l x, Predicate r x) => Predicate (Or l r) x #
Methods validate :: Or l r -> x -> Maybe String #

Numeric

data LessThan (n :: Nat) #

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 #
Methods validate :: LessThan n -> x -> Maybe String #

data GreaterThan (n :: Nat) #

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 #
Methods validate :: GreaterThan n -> x -> Maybe String #

data From (n :: Nat) #

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

Instances

(Ord x, Num x, KnownNat n) => Predicate (From n) x #
Methods validate :: From n -> x -> Maybe String #

data To (n :: Nat) #

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

Instances

(Ord x, Num x, KnownNat n) => Predicate (To n) x #
Methods validate :: To n -> x -> Maybe String #

data FromTo (mn :: Nat) (mx :: Nat) #

A predicate, which ensures that a value is between or equal to either of the specified type-level numbers.

Instances

(Ord x, Num x, KnownNat mn, KnownNat mx, (<=) mn mx) => Predicate (FromTo mn mx) x #
Methods validate :: FromTo mn mx -> x -> Maybe String #

data EqualTo (n :: Nat) #

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 #
Methods validate :: EqualTo n -> x -> Maybe String #

type Positive = GreaterThan 0 #

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

type NonPositive = To 0 #

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

type Negative = LessThan 0 #

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

type NonNegative = From 0 #

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

type ZeroToOne = FromTo 0 1 #

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