Refinement

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

allOf

allOf: conjoin a list of predicates into one that holds when every member holds; the empty list yields a constant true.

allOf : [(Value -> Bool)] -> Value -> Bool

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

anyOf

anyOf: disjoin a list of predicates into one that holds when any member holds; the empty list yields a constant false.

anyOf : [(Value -> Bool)] -> Value -> Bool

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

inRange

inRange: factory predicate asserting that a numeric value lies within [lo, hi]; both endpoints are inclusive.

inRange : Number -> Number -> Number -> Bool

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

matching

matching: factory predicate that holds when a value is a string fully matched by the supplied regex pattern; non-strings are rejected.

matching : String -> String -> Bool

Predicate factory: (matching pattern) s = s matches regex pattern. Full-match semantics — anchor not needed.

negate

negate: flip a predicate's polarity; negate p accepts exactly the values p rejects, and vice versa.

negate : (Value -> Bool) -> Value -> Bool

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

nonEmpty

nonEmpty: predicate asserting that a string or list has at least one element/character; values of other types are rejected.

nonEmpty : (String | List) -> Bool

Predicate: string or list is non-empty. Rejects non-string/non-list inputs.

nonNegative

nonNegative: predicate asserting that a numeric value is greater than or equal to zero; accepts zero, rejects negatives.

nonNegative : Number -> Bool

Predicate: value >= 0. Zero accepted.

positive

positive: predicate asserting that a numeric value is strictly greater than zero; rejects zero, negatives, and non-numerics by extension.

positive : Number -> Bool

Predicate: value > 0. Strict — zero is rejected.

refined

refined: build a named refinement type narrowing base with an extra predicate; the resulting type's check conjoins kernel decision with the guard.

refined : String -> Type -> (Value -> Bool) -> Type

Create a named refinement type. The supplied predicate runs in addition to the base type's check — kernel handles structural validation, the predicate handles residual constraints.