Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Refined p x
- refine :: forall p x. Predicate p x => x -> Either String (Refined p x)
- refineTH :: forall p x. (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))
- unrefine :: Refined p x -> x
- class Predicate p x where
- data Not r
- data And l r
- data Or l r
- data LessThan n
- data GreaterThan n
- data EqualTo n
- type Positive = GreaterThan 0
- type Negative = LessThan 0
- type ZeroToOne = And (Not (LessThan 0)) (Not (GreaterThan 1))
Documentation
A refinement type,
which wraps a value of type x
,
ensuring that it satisfies a type-level predicate p
.
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 ivalid 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.
Predicate Interface
class Predicate p x where Source
A class which defines a runtime interpretation of
a type-level predicate p
for type x
.
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.
(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
A logical conjunction predicate, composed of two other predicates.
A logical disjunction predicate, composed of two other predicates.
Numeric
A predicate, which ensures that a value is less than the specified type-level number.
data GreaterThan n Source
A predicate, which ensures that a value is greater than the specified type-level number.
(Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x |
A predicate, which ensures that a value equals to the specified type-level number.
type Positive = GreaterThan 0 Source
A predicate, which ensures that the value is greater than zero.