Safe Haskell	None
Language	Haskell98

Ditto.Proof

Contents

Description

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 err a b = Proof {
- proofFunction :: a -> m (Either err b)
- proofNewInitialValue :: a -> b
}
prove :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> Proof m error a b -> Form m input error view b
transformEitherM :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> (a -> m (Either error b)) -> (a -> b) -> Form m input error view b
transformEither :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> (a -> Either error b) -> (a -> b) -> Form m input error view b
notNullProof :: Monad m => error -> Proof m error [a] [a]
decimal :: (Monad m, Eq i, Num i) => (String -> error) -> i -> Proof m error String i
signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> i -> Proof m error String i
realFrac :: (Monad m, RealFrac a) => (String -> error) -> a -> Proof m error String a
realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> a -> Proof m error String a

Documentation

data Proof m err 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:

Constructors

Proof
Fields proofFunction :: a -> m (Either err b) function which provides the proof proofNewInitialValue :: a -> b

prove :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> Proof m error a b -> Form m input error view b Source #

apply a Proof to a Form

transformations (proofs minus the proof).

transformEitherM :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> (a -> m (Either error b)) -> (a -> b) -> Form m input error view b Source #

transform the Form result using a monadic Either function.

transformEither :: (Monad m, Monoid view, FormError input error) => Form m input error view a -> (a -> Either error b) -> (a -> b) -> Form m input error view b Source #

transform the Form result using an Either function.

notNullProof :: Monad m => error -> Proof m error [a] [a] Source #

prove that a list is not empty

Arguments

:: (Monad m, Eq i, Num i)
=> (String -> error)	create an error message (`String` is the value that did not parse)
-> i
-> Proof m error String i

read an unsigned number in decimal notation

signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> i -> Proof m error String i Source #

read signed decimal number

realFrac :: (Monad m, RealFrac a) => (String -> error) -> a -> Proof m error String a Source #

read RealFrac number

read a signed RealFrac number