# Refinement Refinement types and predicate combinators. Grounded in Freeman & Pfenning (1991) and Rondon et al. (2008). ## `allOf` _allOf: conjoin a list of predicates. A non-empty list of all-KernelPred members folds into one KernelPred (the conjoined refinement internalizes); any raw lambda, or an empty list, yields a plain conjoined guard that holds when every member holds (empty = constant `true`)._ ``` allOf : [(KernelPred | (Value -> Bool))] -> (KernelPred | (Value -> Bool)) ``` Combine predicates with conjunction: `(allOf [p1 p2]) v = p1 v && p2 v`. All-KernelPred input folds to a KernelPred so the refinement internalizes; a raw-lambda member demotes to a plain guard. Empty list returns constant `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`. ## `eqInt` _eqInt: kernel-internalizing factory predicate `x == k` over Int; internalizes into the kernel `ktype`._ ``` eqInt : Int -> KernelPred ``` KernelPred witness factory over the signed-int carrier deciding `x == k`. ## `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. ## `inRangeInt` _inRangeInt: kernel-internalizing factory predicate `lo <= x <= hi` over Int; both endpoints inclusive, internalizes into the kernel `ktype`._ ``` inRangeInt : Int -> Int -> KernelPred ``` KernelPred witness factory over the signed-int carrier deciding `lo <= x <= hi`. ## `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. ## `nonEmptyStr` _nonEmptyStr: kernel-internalizing refinement predicate deciding String non-emptiness via the host-backed `strLen` (`1 <= length x`). As the predicate of `refined`/`refine` it internalizes into the kernel `ktype`, unlike the raw `nonEmpty` which also covers the list carrier._ ``` nonEmptyStr : KernelPred ``` KernelPred witness over the string carrier deciding `length x >= 1` through `strLen`. Use in place of `nonEmpty` on String to internalize the refinement (non-null `.ktype`). ## `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. ## `nonNegativeInt` _nonNegativeInt: kernel-internalizing refinement predicate `x >= 0` over Int; internalizes into the kernel `ktype` when used with `refined`/`refine`._ ``` nonNegativeInt : KernelPred ``` KernelPred witness over the signed-int carrier deciding `x >= 0`. ## `oneOfStr` _oneOfStr: kernel-internalizing factory predicate deciding membership in a fixed String literal set, via the kernel's decidable `strEq`; a singleton list is equality-against-literal. As the predicate of `refined`/`refine` it internalizes into the kernel `ktype`. Decides by literal equality — substring/match stay outside the kernel._ ``` oneOfStr : [String] -> KernelPred ``` KernelPred witness factory over the string carrier deciding `x ∈ {lits…}` as a strEq disjunction. Unlike `matching` (a raw lambda needing string introspection the kernel lacks), this internalizes. ## `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. ## `positiveInt` _positiveInt: kernel-internalizing refinement predicate `x > 0` over Int; as the predicate of `refined`/`refine` it yields a type whose check is kernel-decided and whose `.ktype` is non-null._ ``` positiveInt : KernelPred ``` KernelPred witness over the signed-int carrier deciding `x > 0`. Unlike `positive` (a raw lambda), this internalizes into the kernel `ktype`. ## `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.