Foundation

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

bind

bind: re-export of fx.kernel.bind for dependent contract modules.

Re-export of fx.kernel.bind.

check

check: predicate that asks whether value inhabits type; returns the type's guarded kernel decision as a Bool, never throws.

check : Type -> Value -> Bool

Check whether a value inhabits a type. Pure — returns a Bool. The dual of make, which throws on failure.

defEq

defEq: definitional equality on types; true iff the kernel-conversion judgment Γ ⊢ A._kernel ≡ B._kernel holds under β/η/ι/μ reduction.

defEq : Type -> Type -> Bool

Definitional equality on types. This is the type-theoretic equality that decides when two type expressions denote the same type:

conv 0 (eval [] (elab A._kernel)) (eval [] (elab B._kernel))

Strictly stronger than meta-language == on _kernel: Nix == only coincides with conv when the encoding contains no closures. After the description-backed migration of Record/Variant/Certified, (H.datatype …).T carries Pi-binder closures and per-call fresh thunks; == on those kernels is no longer a sound proxy for type equality. defEq is the correct predicate.

Grounded in Martin-Löf (1984), section 6, and standard NbE conversion (Abel et al. 2007).

make

make: assert-and-return; runs type.check on the value, returning it on success or throwing a nix-effects type error on failure.

make : Type -> Value -> Value

Validate a value and return it, or throw on failure. The throwing dual of check.

mkType

mkType: foundation type constructor; builds a nix-effects type from a kernel HOAS representation plus optional guard/verify/universe/approximate flags.

mkType : { name, kernelType ? null, guard ? null, verify ? null, description ? name, universe ? null, approximate ? false } -> Type

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 → path → value → Computation). path is a list of fx.diag.positions Position records describing the structural descent from the validation root (e.g. [(P.Field "a") (P.Field "b")] for a nested field, [(P.Elem 0) (P.Field "mtu")] for a list element's field). 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. Record sends separate effects per field 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.

pure

pure: re-export of fx.kernel.pure for dependent contract modules.

Re-export of fx.kernel.pure.

refine

refine: narrow a base type with an extra predicate; returns a refined Type whose check conjoins kernel decision with the supplied guard.

refine : Type -> (Value -> Bool) -> Type

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".

send

send: re-export of fx.kernel.send for dependent contract modules.

Re-export of fx.kernel.send.

validate

validate: emit a standalone typeCheck effect with an explicit context string for ad-hoc validation; prefer type.validate unless overriding context.

validate : Type -> Value -> String -> Computation Bool

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.