Albite

Dependent types

A dependent type is one that depends on a value. This is the feature the whole proof system rests on: without it, a type could not mention the things a proposition needs to talk about.

The idea

In most languages, types and values live in separate worlds. List<Nat> is parameterised by a type, and there is no way to write “a list of length 3” — 3 is a value and types cannot see it.

Dependent types remove that barrier. Eq<Nat, 2 + 2, 4> is the clearest example you have already seen: it is a type, and two of its three arguments are values. The proposition could not be expressed otherwise, because the whole content of the claim lives in those values.

That is the entire mechanism behind Curry-Howard here. A proposition is a statement about particular things; encoding propositions as types therefore requires types that can mention particular things.

What Albite supports today

The core calculus is a dependent type theory, and the surface syntax exposes:

  • Equality types — Eq<T, a, b>, the proposition that a equals b at type T, with refl as its proof
  • The equality combinators — sym, trans, cong, subst
  • Dependent elimination — natind and natrec take a motive, a function from a value to the type of the result, which is what lets the result type vary with the input

The motive is where dependency becomes concrete. In:

natind(|k: Nat| Eq<Nat, 0, 0>, refl, fn(k: Nat, ih: Eq<Nat, 0, 0>) => ih, 0)

the first argument |k: Nat| Eq<Nat, 0, 0> is a function from a value to a type. That is a dependent type in the most literal sense — feed it a number, get back a proposition. See Induction over naturals.

Where it stops

Being straight about the current stage, since “dependently typed” invites the assumption that a Lean or Idris feature set is present:

  • No indexed families. You cannot yet write a length-indexed vector Vec<T, n> where the length is part of the type and the constructors enforce it. This is the canonical dependent-types example and it is on the roadmap for v2.1, not available now.
  • No refinement types — no { n: Nat | n > 0 }. Also v2.1.
  • No universe hierarchy yet. Stratified Type 0 : Type 1 : …, which rules out Girard’s paradox, is a v2.0 item. Until it lands, the type theory is not known to be consistent in the way a mature assistant’s is.
  • Tactics are young. Since 2.0-beta, theorem … by { … } builds a proof step by step; this manual still writes proof terms explicitly.

So: the dependent machinery is genuinely there and genuinely checked by a small kernel, and it is enough for equality proofs and induction over naturals. It is not yet enough to encode invariants in your data structures, which is what most people mean when they ask whether a language has dependent types.