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 typesignature where the typechecker 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 datatype 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