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:

{ 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":

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:

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.