# 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 → fuel → path → value → Computation`).
  `fuel` is the native-recursion budget: recursive verifiers
  descend natively while it is positive and defer the sub-walk
  via a `deriveBounce` effect when it runs out, keeping deep
  structures stack-safe. Non-recursive verifiers ignore it.
  `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. When null (default), the level
  is computed from `checkTypeLevel(kernelType)`. The computed level is
  total: `.universe` throws — rather than fabricating a level — when
  the kernel type is not a type, depends on a term, or is
  level-polymorphic. A supplied `universe` is enforced against the
  kernel minimum: it may over-approximate it (e.g. for a fallback
  `kernelType`) but under-approximation is inconsistent and throws, and
  it cannot pin a level on a type that has none.
- `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".

## `refineGuard`

_refineGuard: build a refinement type's guard slot from a base type and a predicate; a KernelPred witness yields a kernel-derived (authoritative) guard composed with the base's witness, a raw predicate stays an opaque lambda conjoined with `base.check`._

```
refineGuard : Type -> (Value -> Bool | KernelPred) -> (Value -> Bool | KernelPred)
```

Shared by `refine` and `refinement.refined` so both compose guards identically. A `KernelPred` predicate is threaded through (and `andKP`-composed with `base._kernelPred`); a raw predicate becomes `v: base.check v && predicate v`.

## `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.