Dependent sorts in practice

Disclaimer. The content of this page is largely LM-generated. It was written as a stopgap to make the panproto system legible while we work through the book verifying and editing the content by hand. When a chapter has been verified or edited by a human, the parts that were verified or edited will be noted at the head of the chapter.

The GATs chapter said, abstractly, that a sort may be indexed by an earlier sort’s inhabitants. This chapter pins down what that buys the working engineer, using the simply-typed lambda calculus as a worked example, and shows how panproto-gat typechecks a theory that exercises every dependent-sort feature the engine supports.

The point of the example is not that panproto is a type-theory engine; it is that the same dependent-sort machinery the engine uses to keep track of domain and codomain in a category protocol, or source and target vertex kinds in a graph schema, is expressive enough to encode a system programmers already recognise. If the machinery handles STLC, it handles the smaller dependencies that arise in ordinary protocols without strain.

STLC as a GAT

The theory has three sorts. The context sort $Ctx$ and the type sort $Ty$ are global. The term sort $Tm (Γ, A)$ is parameterised by a context and a type: it stands for the collection of closed terms in context $Γ$ at type $A$ . A term in the empty context at type $int \to int$ is a different inhabitant from a term in a one-binding context at the same type, and the indexing records the difference.

The operations are familiar:

arrow    : (A : Ty, B : Ty) -> Ty
extend   : (G : Ctx, A : Ty) -> Ctx
emptyCtx : () -> Ctx
var_zero : (G : Ctx, A : Ty) -> Tm(extend(G, A), A)
lam      : (G, A, B, body : Tm(extend(G, A), B)) -> Tm(G, arrow(A, B))
app      : (G, A, B, f : Tm(G, arrow(A, B)), x : Tm(G, A)) -> Tm(G, B)
subst    : (G, A, B, body : Tm(extend(G, A), B), x : Tm(G, A)) -> Tm(G, B)

Every output sort references the input parameters explicitly: var_zero lives in the extended context with the fresh variable’s type on the right; lam lives in the original context at the arrow type; app lives in the original context at the range. The meta-theoretic invariants that would require a side condition in an extrinsic presentation (e.g., “the source of the substitution matches the context of the body”) are structural in this presentation, because the sort itself names the context.

There is one equation, the $β$ -law stated as a rewrite between two already-well-typed terms:

app(G, A, B, lam(G, A, B, body), x)  =  subst(G, A, B, body, x)

The equation typechecks because both sides have the same output sort, $Tm (Γ, B)$ , under a single inferred variable context. There is no metavariable capture to worry about, because the substitution is itself a named operation in the signature rather than a primitive of the meta-language. A type-theorist will recognise this as a “formal” or “explicit” substitution presentation, due ultimately to Martin-Löf (1984) and elaborated categorically by Dybjer (1996); the categorical story of the same encoding is worked out in depth by Hofmann (1997).

What `panproto-gat` does with this

The typechecker in panproto_gat::typecheck accepts the theory as stated. For each operation, it walks the signature accumulating a substitution from input parameter names to concrete argument terms; the expected sort for each argument is the declared input sort under that substitution, and the inferred output sort of the application is the declared output sort under the final substitution. For the $β$ equation specifically, it runs Robinson unification over the two sides’ sort expressions, yielding a single context assignment that types both halves to the same $Tm (Γ, B)$ .

Concretely, applying app to a well-chosen argument tuple reduces to a substitution computation. Take f with context-declared sort $Tm (Γ, arrow (A, B))$ and x with sort $Tm (Γ, A)$ : the typechecker instantiates G := Γ, A := A, B := B, f := f, x := x, and the output sort is $Tm (Γ, B)$ . Give x the wrong sort — say $Tm (Γ, B)$ when app expects $Tm (Γ, A)$ — and the typechecker rejects the application with an ArgTypeMismatch error that pins the failure to the specific argument position.

The integration test at tests/integration/tests/stlc_gat.rs exercises exactly this flow, end to end, including the $β$ equation and a deliberate ill-typed rejection.

Implicit type arguments

The signature listed above is the canonical one, and it is the signature the typechecker accepts. It is also awkward to write at a use site. A working developer wants app(f, x), not app(G, A, B, f, x): the three context-and-type arguments are recoverable from the sorts of f and x by unification, and asking the user to spell them out is redundant.

The 0.37 release added an Implicit::Yes tag on each operation input, which marks a parameter as recoverable at the call site rather than supplied explicitly. The STLC fixture marks G, A, B implicit on lam, app, and subst, and the signatures now read

lam      : (G, A, B {implicit}, body : Tm(extend(G, A), B)) -> Tm(G, arrow(A, B))
app      : (G, A, B {implicit}, f : Tm(G, arrow(A, B)), x : Tm(G, A)) -> Tm(G, B)
subst    : (G, A, B {implicit}, body : Tm(extend(G, A), B), x : Tm(G, A)) -> Tm(G, B)

with an associated convention that the three implicit positions are filled by unifying the explicit argument sorts against the declared input sorts. A call app(f, x) typechecks by solving $Tm (Γ, arrow (A, B))$ for $Γ$ , $A$ , $B$ given f’s sort and $Tm (Γ, A)$ for the same three given x’s sort; the two solutions agree, the implicit inputs are bound, and the output sort $Tm (Γ, B)$ is returned. The original five-argument spelling is still legal, which matters for backward compatibility: every theory that passed 0.36 continues to pass 0.37 without edits.

The mechanism is not specific to STLC. Any operation whose early inputs are determined by the sorts of its later inputs is a candidate for implicit tagging, and the typical signature in a protocol theory has at least one such input. The reward is that the worked examples of Part IV now look the way the working developer would write them rather than the way the theory demands them.

Closed sorts and total case analysis

STLC has no closed sort in the 0.37 sense, because its type sort $Ty$ is open: a theory author can always extend the set of types by declaring a new ty_ operation. Protocol theories of practical interest, however, often do pick a fixed constructor list up front. A protocol that emits Stan programs from a statistical schema, for instance, carries a sort $Distr$ whose inhabitants are exactly the Stan distribution primitives ( $normal$ , $beta$ , $gamma$ , and the remaining few dozen), and that list does not grow.

Before 0.37 the emitter for such a protocol had to be a partial function: given a Distr it pattern-matched on the head name and fell through to an unreachable! clause the engine could not prove was never taken. With closed sorts and Term::Case, the same emitter is a total case expression. The sort declaration carries a SortClosure::Closed(vec!["normal", "beta", "gamma", ...]), the emitter is a Case whose branches cover exactly that list, and the typechecker verifies coverage at the declaration site rather than deferring the obligation to runtime. The unreachable! is gone and the engine can prove it was never needed.

The feature generalises. Any protocol whose theory picks a fixed constructor list for some sort — the SQL type system’s primitives, the Avro primitive-type set, the ATProto lexicon primitive list — is now expressible as a closed sort, and any transform that dispatches on that sort is now a total Case rather than a string-keyed lookup table. How panproto-gat represents dependent sorts states the typechecker conditions; this chapter’s purpose is to say that the feature applies to the protocols in Part IV and not only to the small inductive types.

Why this encoding sidesteps capture-avoiding substitution

The textbook concern with encoding $λ$ -calculus as an algebraic theory is that naive substitution captures free variables: substituting a term with a free x into a context that already binds x silently changes the term’s meaning. The usual remedies are de Bruijn indices, nominal sets, higher-order abstract syntax, or ad-hoc freshness side conditions. Each remedy has its own costs and complexities.

The encoding above pays a different price and sidesteps the problem entirely. There is no binder in the meta-language: lam takes a body whose sort names the extended context directly, and var_zero is an explicit variable-projection operation rather than a name that has to be compared structurally. Because the meta-language’s only operation on variables is the one the theory declares, capture is impossible: the engine never has the opportunity to alpha-rename anything. The $β$ rule’s right-hand side calls the declared subst operation, whose semantics are whatever the theory’s equations fix; no appeal to a meta-level substitution function is required.

The cost is that the theory has to carry an explicit extend / var_zero / subst triple, and the bookkeeping that a structural substitution would provide for free in a traditional presentation has to be stated as equations. For a language as small as STLC, this is a fair trade. For a full dependent type theory the same style scales up, at the price of more equations, as Dybjer (1996) and subsequent categories-with-families work up in detail.

What this unlocks for protocols

The machinery that makes STLC work is not STLC-specific. Any protocol whose sorts carry indexing — a relational schema where a column’s sort depends on its table, a graph schema where an edge’s sort depends on its source and target vertex kinds, a message schema where a field’s sort depends on a discriminator — uses the same mechanism. The GATs chapter (How panproto-gat represents dependent sorts) states the mechanism abstractly; this chapter is the worked case that makes the abstraction concrete.

The typical indexing depth for the protocols covered in Part IV is shallow (one or two parameters), far short of what STLC demands. Reading the STLC example is therefore a way of confirming that the engine is not near its limits when it handles the simpler cases; it is doing, in production, a much weaker version of what the worked example exercises.

Equality of signatures across theories

Parameter names inside an operation’s signature are local binders, not names a morphism is expected to preserve. Two theories can present the category’s identity morphism as id : (x : \mathrm{Ob}) \to \mathrm{Hom}(x, x) and id : (y : \mathrm{Ob}) \to \mathrm{Hom}(y, y) respectively and still be canonically isomorphic; a morphism between them that maps id to id is categorically well-formed, and check_morphism accepts it.

The mechanism is a positional alpha-rename. When comparing a domain operation f : (p_1, \ldots, p_n) \to T against its image f' : (q_1, \ldots, q_n) \to T' in the codomain, the checker builds the substitution $σ = {p_{i} \mapsto q_{i}}$ and compares T.subst(σ) against T' rather than T against T' directly. The same substitution is applied to each input sort and to any dependent sort-parameter blocks. Reordering parameter positions (say, swapping (x, y) for (y, x)) is not an alpha-rename and is correctly rejected; the invariance is purely in the choice of binder names, not in their arity or order. The helpers positional_param_rename and signatures_equivalent_modulo_param_rename expose the same comparison to callers that want to perform signature-equality checks outside of check_morphism; the colimit machinery uses them when merging two theories that share an operation name.

Keyboard shortcuts

panproto