Foundation

Type system foundation: Type constructor, check, validate, make, refine.

check

Check whether a value inhabits a type. Returns bool.

make

Validate a value and return it, or throw on failure.

mkType

Create a type from its kernel representation.

A nix-effects type is defined by its kernelType — an HOAS type tree representing the type in the MLTT kernel. All fields are derived:

• .check = decide(kernelType, v) — the decision procedure
• .universe = checkTypeLevel(kernelType) — computed universe level
• .kernelCheck = same as .check
• .prove = kernel proof checking for HOAS terms

Arguments:

• name — Human-readable type name
• kernelType — HOAS type tree (required — this IS the type)
• guard — Optional runtime predicate for refinement types. When present, .check = kernelDecide(v) && guard(v) (conjunction — kernel catches structural errors, guard handles residual constraints). The guard handles constraints the kernel can't express (e.g., x >= 0).
• verify — Optional custom verifier (self → value → Computation). When null (default), validate is auto-derived by wrapping check in a typeCheck effect. Supply a custom verify for types that decompose checking (e.g. Sigma sends separate effects for fst and snd for blame tracking).
• description — Documentation string (default = name)
• universe — Optional universe level override. When null (default), computed from checkTypeLevel(kernelType). Use when the kernelType is a fallback (e.g., H.function_ for Pi) that doesn't capture the real universe level.
• approximate — When true, the kernelType is a sound but lossy approximation (e.g., H.function_ for Pi, H.any for Sigma). Suppresses _kernel, kernelCheck, and prove on the result, since the kernel representation doesn't precisely capture this type. The kernelType is still used internally for universe computation.

refine

Narrow a type with an additional predicate. Creates a refinement type whose check = kernelDecide(v) ∧ guard(v) (conjunction). The base type's kernel provides structural checking; the guard handles the refinement predicate the kernel cannot express. Grounded in Freeman & Pfenning (1991) "Refinement Types for ML" and Rondon et al. (2008) "Liquid Types".

validate

Standalone effectful validation with explicit context string.

Sends a typeCheck effect with the given type, value, and context. The handler receives { type, context, value } and determines the response: throw, collect error, log, or offer restarts.

For typical use, prefer type.validate (auto-derived by mkType, uses the type's name as context). This 3-arg form is for cases where a custom context string is needed.

validate : Type → Value → String → Computation Bool