Safe Haskell | None |
---|---|
Language | Haskell98 |
This module defines the Proof
type, some proofs, and some helper functions.
A Proof
does three things:
- verifies that the input value meets some criteria
- optionally transforms the input value to another value while preserving that criteria
- puts the proof name in type-signature where the type-checker can use it
Synopsis
- data Proof m error proof a b = Proof {
- proofName :: proof
- proofFunction :: a -> m (Either error b)
- prove :: Monad m => Form m input error view q a -> Proof m error proof a b -> Form m input error view proof b
- transform :: Monad m => Form m input error view anyProof a -> Proof m error proof a b -> Form m input error view () b
- transformEitherM :: Monad m => Form m input error view anyProof a -> (a -> m (Either error b)) -> Form m input error view () b
- transformEither :: Monad m => Form m input error view anyProof a -> (a -> Either error b) -> Form m input error view () b
- data NotNull = NotNull
- notNullProof :: Monad m => error -> Proof m error NotNull [a] [a]
- data Decimal = Decimal
- data RealFractional = RealFractional
- data Signed a = Signed a
- decimal :: (Monad m, Eq i, Num i) => (String -> error) -> Proof m error Decimal String i
- signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i
- realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error RealFractional String a
- realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a
Documentation
data Proof m error proof a b Source #
A Proof
attempts to prove something about a value.
If successful, it can also transform the value to a new value. The proof should hold for the new value as well.
Generally, each Proof
has a unique data-type associated with it
which names the proof, such as:
data NotNull = NotNull
Proof | |
|
prove :: Monad m => Form m input error view q a -> Proof m error proof a b -> Form m input error view proof b Source #
transformations (proofs minus the proof).
transform :: Monad m => Form m input error view anyProof a -> Proof m error proof a b -> Form m input error view () b Source #
transformEitherM :: Monad m => Form m input error view anyProof a -> (a -> m (Either error b)) -> Form m input error view () b Source #
transformEither :: Monad m => Form m input error view anyProof a -> (a -> Either error b) -> Form m input error view () b Source #
Various Proofs
notNullProof :: Monad m => error -> Proof m error NotNull [a] [a] Source #
prove that a list is not empty
:: (Monad m, Eq i, Num i) | |
=> (String -> error) | create an error message ( |
-> Proof m error Decimal String i |
read an unsigned number in decimal notation
signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i Source #
read signed decimal number