Dependent functions: Pi types

A dependent function allows its result type to mention an accepted argument. This connects a runtime or compile-time input with a fact preserved by the result.

The basic form

(n:Nat) -> Vec(a,n)

The binder n is in scope to the right of the arrow. A declaration might be:

function replicate[a:Type](n:Nat, item:a) : Vec(a,n) = ...;

Calling replicate(Succ(Z), "x") substitutes that accepted argument term for n in the result type.

Substitution is semantic

Application does not merely erase a binder name. It performs capture-avoiding substitution of the checked argument, including an explicit coercion when subsumption was used. This matters for indexed data and nominal subtyping: dependent results must describe the value actually accepted by the function.

Dependency and runtime relevance

A binder appearing in a result type is not automatically erased. Relevance is decided per binder:

• a type-only parameter can usually disappear at runtime;
• a value controlling runtime computation must remain;
• erased evidence can still justify checked elaboration.

“Dependent” and “compile-time only” are therefore different concepts.

Ordinary arrows are Pi types too

Int -> String

is a non-dependent Pi type: the result does not name the input. The common syntax stays concise while the dependent form adds a binder only when needed.

Multiple dependent binders

(rows:Nat) -> (cols:Nat) -> Matrix(Float64,rows,cols)

Each binder scopes over what follows. Function parameter lists preserve the same n-ary telescope structure rather than compiling to nested pairs.

Totality boundary

Computation used to establish type equality must terminate. Runtime functions may be generally recursive, but an unchecked non-total computation cannot be silently normalized by the type checker.

Dependent APIs are most useful when they expose a fact callers already care about—dimensions, lengths, protocol states, capabilities—not when they merely move incidental values into types.

Common mistakes

Dependency does not imply erasure, and runtime recursion does not imply that the checker may normalize the function. Preserve the accepted, possibly coerced, argument when reasoning about a dependent result.

Recap

A Pi binder scopes over its result and application substitutes the checked argument capture-safely. Ordinary arrows are the concise non-dependent case.

Normative details: Language Reference §4.3.