Safe Haskell  None 

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
 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 bSource
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 () bSource
transformEitherM :: Monad m => Form m input error view anyProof a > (a > m (Either error b)) > Form m input error view () bSource
transformEither :: Monad m => Form m input error view anyProof a > (a > Either error b) > Form m input error view () bSource
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 iSource
read signed decimal number
realFrac :: (Monad m, RealFrac a) => (String > error) > Proof m error RealFractional String aSource
read RealFrac
number
realFracSigned :: (Monad m, RealFrac a) => (String > error) > Proof m error (Signed RealFractional) String aSource
read a signed RealFrac
number