reform-0.2.7.5: reform is a type-safe HTML form generation and validation library

Safe Haskell | Safe-Inferred
Language | Haskell2010

Text.Reform.Proof

Contents

- transformations (proofs minus the proof).
- Various Proofs

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

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

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

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

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

transform the `Form` result using an `Either` function.

# Various Proofs

data NotNull Source #

proof that a list is not empty

Constructors

NotNull |

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

prove that a list is not empty

data Decimal Source #

proof that a `String` is a decimal number

Constructors

Decimal |

data RealFractional Source #

proof that a `String` is a Real/Fractional number

Constructors

RealFractional |

data Signed a Source #

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

Constructors

Signed a |

decimal Source #

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

read signed decimal number

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

read `RealFrac` number

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

read a signed `RealFrac` number