# Dependent


Dependent contracts: Pi (Π), Sigma (Σ), Certified, Vector, DepRecord.
Grounded in Martin-Löf (1984) "Intuitionistic Type Theory".

## `Certified`

Subset type `Σ(x:A).P(x)` with `P(x)` a mere proposition. The witness
is an inhabitant of `P(x)`, not the host Bool. Two formers, one type:

- decidable `predicate` (a `reflect` KernelPred) → `P x = KT.P(decide t x)`
  (`Unit`/`Void` ≡ `KT.El t`); witness is the Unit inhabitant (`null`),
  synthesized by `certify`. `_kernelSufficient = true`; `_kernel = El t`.
- general `{ family; bridge; }` (`family : A → U`, or a `mkPropFamily`
  bundle passed as `family`) → `P x = squash(family x)`, proof
  irrelevance definitional; witness is `squashIntro` of a checked HOAS
  proof supplied to `certifyProof v p`. `_kernelSufficient = false`.

A predicate that is neither (a raw host lambda) yields no proof, so it is
not a `Certified` — construction throws. For an un-proven runtime guard
use `fx.types.refinement.refined`.

Construction:

- `.certify v` — decidable: pure, fail-closed, synthesizes the witness.
- `.certifyProof v p` — general: checks `p : family(v)`, then truncates.
- `.certifyE v` — decidable effectful dual (sends `typeCheck` on failure).
- `.certifyProofE v p` — general effectful dual (sends `typeCheck` on failure).
- `.check` / `.validate` — inherited from Sigma (pair check / effectful intro).
- `.prove term` — checks a term against the genuine subset `_kernel`.

Membership decides component-wise: `.check`/`.validate` ride a structural
`Σ x:A. Unit` kernelType (host-decidable without normalizing), with the
predicate decided at the concrete fst; `_kernel` exposes the real `El t`.

## `DepRecord`

Dependent record type built on nested Sigma.

Schema is an ordered list of `{ name; type; }` where `type` can be:

- A Type (static field)
- A function (`partial-record → Type`) for dependent fields

Isomorphic to nested Sigma types:

```
{ a : A, b : B(a) }              ≅  Σ(a:A).B(a)
{ a : A, b : B(a), c : C(a,b) }  ≅  Σ(a:A).Σ(b:B(a)).C(a,b)
```

Values are nested Sigma pairs:

```nix
{ fst = a; snd = { fst = b; snd = c; }; }
```

Inherits from Sigma: `.validate` (effectful), `.proj1`, `.proj2`,
`.pair`, `.pairE`, `.curry`, `.uncurry`.

Use `.pack` to convert flat attrset → nested Sigma value.
Use `.unpack` to convert nested Sigma value → flat attrset.

## `Pi`

Dependent function type `Π(x:A).B(x)`.

Arguments:

- `domain` — Type A
- `codomain` — A-value → Type (type family B indexed by domain values)
- `universe` — Universe level (explicit parameter — see below)
- `name` — optional display name

== Higher-order contract with algebraic effects ==

Pi is a HIGHER-ORDER CONTRACT (Findler & Felleisen 2002). Higher-order
contracts check function values differently from data values: a data
contract is verified immediately and completely, but a function contract
is verified incrementally at each application site. This is the
standard, correct strategy for function contracts — not a deficit.

The (Specification, Guard, Verifier) triple for Pi:

```
Guard (check):       builtins.isFunction — the immediate first-order
                     part of the contract. Soundly rejects non-functions.
Verifier (validate): effectful guard (auto-derived, 1 arg) — wraps
                     the guard in a typeCheck effect for blame tracking.
Elimination (checkAt): deferred contract check (2 args) — verifies a
                     specific application f(arg) by sending typeCheck
                     effects for both domain (arg : A) and codomain
                     (f(arg) : B(arg)).
```

This is precisely the Findler-Felleisen decomposition: the immediate
part (`isFunction`) is checked at introduction; the deferred part
(domain + codomain) is checked at each elimination site via `checkAt`.

== Adequacy ==

```
check f ⟺ all typeCheck effects in (validate f) pass
```

Both `check` and `validate` verify the introduction form (is it a function?).
`checkAt` verifies individual applications — the deferred contract.

== Universe level ==

Universe level is an explicit parameter. In MLTT, the level is computed
as `max(i, sup_{a:A} level(B(a)))` by inspecting the syntax of B.
For types with explicit kernelType, the kernel computes and verifies
levels via checkTypeLevel. The explicit universe parameter provides
the level for the surface API's `.universe` field.

== MLTT rule mapping ==

```
Formation:          Pi { domain, codomain, universe }
Introduction check: .check (guard: isFunction)
Introduction verify: .validate (effectful guard, auto-derived)
Elimination:        .apply (pure), .checkAt (effectful, deferred contract)
Computation:        β-reduction (Nix evaluation)
```

Operations:

- `.checkAt f arg` — deferred contract check at elimination site
- `.apply arg` — pure elimination: compute codomain type B(arg)
- `.compose f other` — compose Pi types (requires witness function)
- `.domain` — the domain type A
- `.codomain` — the type family B

## `Sigma`

Dependent pair type `Σ(x:A).B(x)`.

Arguments:

- `fst` — Type A (type of the first component)
- `snd` — A-value → Type (type family for the second component)
- `universe` — Universe level (explicit parameter)
- `name` — optional display name
- `kernelType` — optional explicit HOAS kernel form (see below)

Values are `{ fst; snd; }` where `fst : A` and `snd : B(fst)`.

== Kernel form: explicit vs. approximate ==

`snd : A-value → Type` lives at the Nix-meta level — it operates on
Nix values. The kernel form `H.sigma name fst._kernel (a: ...)`
needs a closure operating on **HOAS variables**, not Nix values.
The two categories disagree:

```
snd          : NixVal → Type        (surface, Nix-meta)
kernel snd   : HoasVar → HoasType   (kernel, HOAS-level)
```

For genuinely-dependent `snd` (e.g., `x: if x > 0 then Int else String`),
`snd` cannot be applied to an HOAS variable — the test on the variable
would crash. So the library does not attempt automatic derivation;
omitting `kernelType` produces `_kernel = H.any` with `approximate =
true`. Downstream consumers that take Sigma through `elaborateType`
recover the structure at the surface→kernel boundary; consumers that
use `_kernel` directly (kernel walkers, the generic `deriveCheck`
dispatcher) see `H.any`.

Pass `kernelType` explicitly when you need the kernel form to **be** a
Sigma — for example when piping the Type into another datatype
constructor whose kernel walker dispatches on `_htag == "sigma"`:

```nix
Prod = Sigma {
  fst = Int;
  snd = _: String;
  universe = 0;
  kernelType = H.sigma "x" Int._kernel (_: String._kernel);
};
```

For the non-dependent case (snd ignores its argument) the explicit
form is mechanical and could in principle be derived; the library
treats both cases uniformly to keep the dependent/non-dependent
distinction out of the surface API.

== First-order contract — guard is exact ==

Sigma is a FIRST-ORDER CONTRACT: both components are concrete data,
so the contract is checked immediately and completely. The guard
(`check`) IS full membership — there is no over-approximation.

```
Guard (check):    fst:A ∧ snd:B(fst) — exact. G = ⟦Σ(x:A).B(x)⟧.
Verifier (verify): decomposed effectful check — sends separate
                  typeCheck effects for fst and snd for blame tracking.
```

This contrasts with Pi where the guard over-approximates (`isFunction`)
because functions are higher-order. Sigma pairs are data — the
dependent relationship (snd's type depends on fst's value) can be
fully verified because both values are available.

Adequacy:

```
T.check v ⟺ all typeCheck effects in T.validate v pass
```

Under the all-pass handler. The guard is exact and the decomposed
verifier sends individual `typeCheck` effects per component — the all-pass
handler's boolean state tracks whether all passed. Totality: if the input
is structurally malformed (not an attrset, missing `fst`/`snd`), verify falls
back to a single `typeCheck` for the whole type — failure goes through the
effect system, never crashes Nix.

Universe level is an explicit parameter (computing
`sup_{a:A} snd(a).universe` requires evaluating the type family on
all domain values, same as Pi).

== MLTT rule mapping ==

```
Formation:    Sigma { fst, snd, universe }
Introduction: .check (exact guard), .validate (effectful, decomposed)
Elimination:  .proj1 (π₁), .proj2 (π₂)
Computation:  π₁(a,b) ≡ a, π₂(a,b) ≡ b
```

Operations:

- `.proj1 pair` — first projection π₁
- `.proj2 pair` — second projection π₂
- `.pair a b` — smart constructor (throws on invalid)
- `.validate v` — effectful: decomposed typeCheck effects for blame
- `.pairE a b` — effectful smart constructor
- `.pullback f g` — contravariant predicate pullback (see below)
- `.curry` / `.uncurry` — standard Sigma adjunction
- `.fstType` — the type A
- `.sndFamily` — the type family B

## `Vector`

Length-indexed list type family, built on Pi.

```
Vector(A) = Π(n:Nat).{xs : List(A) | |xs| = n}
```

This is the correct Martin-Löf encoding: Vector IS a Pi type.
It inherits `.validate` (effectful), `.compose`, `.apply`, `.domain`, `.codomain`
from Pi.

Usage:

```nix
Vector elemType           # the Pi type family (Nat → SizedList)
(Vector elemType).apply 3 # specific type for length 3
```

## `mkPropFamily`

Bundle a propositional `family` (`A → U`) with its `bridge` into one
handle for `Certified`'s general former. Pass it via the `family`
argument: `Certified { base; family = mkPropFamily { family; bridge; }; }`.
The two-argument `{ family; bridge; }` form remains valid.