Refined

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 p, Data x) => 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-ELkNaTsTAeUF2AJYUJxHAV" 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

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

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

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

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 mx

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

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.