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.