Dependent type

A type that may mention values, so that a vector's length can appear in its type and a function can promise to return a vector one element longer than its argument. Type checking then involves evaluating terms, which is why languages with dependent types usually double as proof assistants.

A dependent type may mention values, so the length of a vector can live in its type and a function's result type can be computed from its arguments. Concatenation gets the signature it always should have had:

append : Vec α m \to Vec α n \to Vec α (m + n)

Function types generalise to dependent products, written $Π_{x : A} B (x)$ , where the result type $B (x)$ may refer to the argument. Under the Curry-Howard correspondence a universally quantified proposition is exactly such a type, and its proof is exactly a term of that type, which is why languages with dependent types double as proof assistants.

In Lean 4: the type checker verifies the arithmetic in the type, not just the code.

def append : {a : Type} -> {m n : Nat} -> Vector a m -> Vector a n -> Vector a (m + n)
  | _, _, Vector.nil,       ys => ys
  | _, _, Vector.cons x xs, ys => Vector.cons x (append xs ys)

The price is that type checking now involves evaluation, so type equality is decided up to computation and error messages are about unsolved goals rather than mismatched constructors.