Reference
Auto-generated API reference from nix-effects source.

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 provided, .check = decide(kernelType, v) && guard(v). The guard is NOT part of the kernel — it handles constraints the kernel can't express (e.g., x >= 0 for Nat).
  • 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 = decide(kernelType, v) AND predicate(v). The base type's kernelType provides the kernel backing; the predicate is a runtime-only guard 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
←DependentLinear→