Refinement

Refinement types and predicate combinators. Grounded in Freeman & Pfenning (1991) and Rondon et al. (2008).

allOf

Combine predicates with conjunction: (allOf [p1 p2]) v = p1 v && p2 v.

anyOf

Combine predicates with disjunction: (anyOf [p1 p2]) v = p1 v || p2 v.

inRange

Predicate factory: (inRange lo hi) v = lo <= v <= hi.

matching

Predicate factory: (matching pattern) s = s matches regex pattern.

negate

Negate a predicate: (negate p) v = !(p v).

nonEmpty

Predicate: string or list is non-empty.

nonNegative

Predicate: value >= 0.

positive

Predicate: value > 0.

refined

Create a named refinement type.

refined : string -> Type -> (value -> bool) -> Type