Text.Reform.Proof

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

Documentation

data Proof m error proof a b

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

Constructors

Proof

Fields

• proofName :: proof

  name of the thing to prove

• proofFunction :: a -> m (Either error b)

  function which provides the proof

prove :: Monad m => Form m input error view q a -> Proof m error proof a b -> Form m input error view proof b

apply a Proof to a Form

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

transform a Form using a Proof, and the replace the proof with ().

This is useful when you want just want classic digestive-functors behaviour.

transformEitherM :: Monad m => Form m input error view anyProof a -> (a -> m (Either error b)) -> Form m input error view () b

transform the Form result using a monadic Either function.

transformEither :: Monad m => Form m input error view anyProof a -> (a -> Either error b) -> Form m input error view () b

transform the Form result using an Either function.

Various Proofs

data NotNull

proof that a list is not empty

Constructors

NotNull

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

prove that a list is not empty

data Decimal

proof that a String is a decimal number

Constructors

Decimal

data RealFractional

proof that a String is a Real/Fractional number

Constructors

RealFractional

data Signed a

proof that a number is also (allowed to be) signed

Constructors

Signed a

decimal

Arguments

:: (Monad m, Eq i, Num i)

=> (String -> error)

create an error message (String is the value that did not parse)

-> 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

read signed decimal number

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

read RealFrac number

realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a

read a signed RealFrac number