data-checked-0.3: Type-indexed runtime-checked properties

Safe HaskellSafe-Inferred

Data.Checked.Strict

Description

A version of Checked that requires client code to provide a non-bottom value of the property index type to use trust* functions.

Synopsis

Documentation

data Checked p v Source

Wrapper-evidence for property p.

Instances

trustThat :: p -> v -> Checked p vSource

Use when the property can be deduced without a runtime check. Note that p is evaluated to WHNF, so you can't use undefined.

trustMap :: p -> (v -> v) -> Checked p v -> Checked p vSource

Apply a fuction that preserves the property to the checked value. Note that p is evaluated to WHNF, so you can't use undefined.

checked :: Checked p v -> vSource

Unwrap the checked value.

class Property p v whereSource

Methods

holds :: p -> v -> BoolSource

Test if the property holds for the given value. The first argument is supposed to be ignored.

maybeHolds :: Property p v => p -> v -> Maybe vSource

Return Just v if p holds and Nothing overwise.

check :: forall p v. Property p v => v -> Maybe (Checked p v)Source

Wrap the value if the property holds.

relax :: Checked p v -> Checked p vSource

Rewrap a value into the less strict Checked type.