Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

Predicates

Intended for qualified import.

## Synopsis

- data Predicate :: [Type] -> Type
- data Expr
- prettyExpr :: Expr -> String
- data Fn a b
- fn :: Show b => (Var, a -> b) -> Fn a b
- fnWith :: (Var, b -> String, a -> b) -> Fn a b
- transparent :: (a -> b) -> Fn a b
- alwaysPass :: Predicate xs
- alwaysFail :: Predicate xs
- unary :: (a -> Bool) -> (Expr -> Err) -> Predicate '[a]
- binary :: (a -> b -> Bool) -> (Expr -> Expr -> Err) -> Predicate [a, b]
- satisfies :: (Var, a -> Bool) -> Predicate '[a]
- relatedBy :: (Var, a -> b -> Bool) -> Predicate [a, b]
- dot :: Predicate (x ': xs) -> Fn y x -> Predicate (y ': xs)
- split :: Predicate (x' ': (y' ': xs)) -> (Fn x x', Fn y y') -> Predicate (x ': (y ': xs))
- on :: Predicate (x ': (x ': xs)) -> Fn y x -> Predicate (y ': (y ': xs))
- flip :: Predicate (x ': (y ': zs)) -> Predicate (y ': (x ': zs))
- matchEither :: Predicate (a ': xs) -> Predicate (b ': xs) -> Predicate (Either a b ': xs)
- matchBool :: Predicate xs -> Predicate xs -> Predicate (Bool ': xs)
- eval :: Predicate '[] -> Either Err ()
- (.$) :: Show x => Predicate (x ': xs) -> (Var, x) -> Predicate xs
- at :: Predicate (x ': xs) -> (Expr, String, x) -> Predicate xs
- eq :: Eq a => Predicate [a, a]
- ne :: Eq a => Predicate [a, a]
- lt :: Ord a => Predicate [a, a]
- le :: Ord a => Predicate [a, a]
- gt :: Ord a => Predicate [a, a]
- ge :: Ord a => Predicate [a, a]
- towards :: forall a. (Show a, Ord a, Num a) => a -> Predicate [a, a]
- expect :: (Show a, Eq a) => a -> Predicate '[a]
- between :: (Show a, Ord a) => a -> a -> Predicate '[a]
- even :: Integral a => Predicate '[a]
- odd :: Integral a => Predicate '[a]
- elem :: Eq a => Predicate [[a], a]
- pairwise :: forall a. Show a => Predicate [a, a] -> Predicate '[[a]]

# Documentation

data Predicate :: [Type] -> Type Source #

N-ary predicate

A predicate of type

Predicate '[Int, Bool, Char, ..]

is essentially a function `Int -> Bool -> Char -> .. -> Bool`

, along with
some metadata about that function that allows us to render it in a human
readable way. In particular, we construct an `Expr`

for the values that the
predicate has been applied to.

# Expressions

Simple expression language

The internal details of this type are (currently) not exposed.

prettyExpr :: Expr -> String Source #

# Functions

transparent :: (a -> b) -> Fn a b Source #

Function that should not be visible in any rendered failure

Consider these two predicates:

p1, p2 :: Predicate '[Char, Char] p1 = P.eq `P.on` (P.fn "ord" ord) p2 = P.eq `P.on` (P.transparent ord)

Both of these compare two characters on their codepoints (through `ord`

), but
they result in different failures. The first would give us something like

(ord x) /= (ord y) x : 'a' y : 'b' ord x: 97 ord y: 98

whereas the second might give us something like

x /= y x: 'a' y: 'b'

which of these is more useful is of course application dependent.

# Construction

alwaysPass :: Predicate xs Source #

Constant `True`

alwaysFail :: Predicate xs Source #

Constant `False`

:: (a -> Bool) | The predicate proper |

-> (Expr -> Err) | Error message, given |

-> Predicate '[a] |

Unary predicate

This is essentially a function `a -> Bool`

; see `Predicate`

for detailed
discussion.

:: (a -> b -> Bool) | The predicate proper |

-> (Expr -> Expr -> Err) | Error message, given |

-> Predicate [a, b] |

Binary predicate

This is essentially a function `a -> b -> Bool`

; see `Predicate`

for detailed
discussion.

# Auxiliary construction

relatedBy :: (Var, a -> b -> Bool) -> Predicate [a, b] Source #

Specialization of `binary`

for relations

# Combinators

dot :: Predicate (x ': xs) -> Fn y x -> Predicate (y ': xs) Source #

Function composition (analogue of `(.)`

)

split :: Predicate (x' ': (y' ': xs)) -> (Fn x x', Fn y y') -> Predicate (x ': (y ': xs)) Source #

Analogue of 'Control.Arrow.(***)'

matchEither :: Predicate (a ': xs) -> Predicate (b ': xs) -> Predicate (Either a b ': xs) Source #

Match on the argument, and apply whichever predicate is applicable.

:: Predicate xs | Predicate to evaluate if the condition is true |

-> Predicate xs | Predicate to evaluate if the condition is false |

-> Predicate (Bool ': xs) |

Conditional

This is a variation on `choose`

that provides no evidence for which branch is
taken.

# Evaluation and partial evaluation

(.$) :: Show x => Predicate (x ': xs) -> (Var, x) -> Predicate xs Source #

Infix version of `at`

Typical usage example:

assert $ P.relatedBy ("equiv", equiv) .$ ("x", x) .$ ("y", y)

# Specific predicates

towards :: forall a. (Show a, Ord a, Num a) => a -> Predicate [a, a] Source #

Check that values get closed to the specified target