Families and branches

An Alpha family defines a set of related values. A constructor is one way to build a value in that family. A branch is the checked case for one constructor when a program eliminates—or consumes—a family value.

The design comes from inductive families in dependent type theory, not from a runtime class hierarchy. The closest foundational reference is Peter Dybjer's Inductive Families.

A family defines the valid shapes

family Tree : Type 0
constructor Leaf
field unrestricted leafValue : Nat
constructor Fork
recursive unrestricted leftTree
recursive unrestricted rightTree
end-family

This declaration says that a Tree is either:

• a Leaf carrying one natural-number field; or
• a Fork carrying two recursive trees.

field introduces ordinary data. recursive introduces a strictly positive occurrence of the family being defined. Alpha checks declaration order, uniqueness, telescope formation, positivity, result indices, and the types of fields.

Constructors build values

def oneLeaf : (family Tree) =
  (constructor Tree Leaf (succ zero))

Construction names both the family and constructor. That explicitness lets the checker validate the complete constructor telescope instead of accepting an untyped tag and payload.

Elimination consumes values

An eliminator states four things:

1. which family is being consumed;
2. the motive, or result type for every possible family value;
3. the scrutinee; and
4. one branch for every constructor, in declaration order.

(eliminate
  Tree
  (lambda unrestricted current : (family Tree) . Nat)
  tree
  (branch Leaf value . (succ zero))
  (branch Fork left right leftSize rightSize .
    (nat-add leftSize rightSize)))

The motive above is constant: every tree produces a Nat. A dependent motive may mention the current value or its indices, allowing each constructor branch to return evidence specialized to the exact case.

What a branch receives

A branch begins with a constructor name, continues with the binders prescribed by that constructor, then uses . to separate binders from its result:

(branch Constructor binder ... . body)

Each ordinary field contributes its value. Each recursive field contributes two binders:

• the recursive value; and
• the induction result obtained by eliminating that recursive value with the same motive.

That is why the Fork branch above receives left, right, leftSize, and rightSize. Branch arity is derived from the checked family declaration; it is not guessed from visual field count.

Why branches are exhaustive and ordered

Alpha requires exactly one branch per constructor, in constructor order. There is no unchecked default branch. This preserves a direct correspondence between declaration and eliminator:

• adding a constructor makes existing consumers incomplete;
• omitting, duplicating, or reordering a branch is an error;
• branch binders must match the constructor telescope; and
• every branch result must satisfy the motive specialized to that constructor.

This is useful for syntax trees, typed intermediate representations, protocol evidence, validated records, and recursive data whose consumers must remain complete as the definition evolves.

Indexed families

Indices make the valid constructor result part of the type. A vector skeleton can say that VNil produces length zero while VCons produces a successor length:

family Vec : Type 0
index unrestricted length : Nat
constructor VNil
result zero
constructor VCons
field unrestricted prior : Nat
recursive unrestricted tail
recursive-index prior
result (succ prior)
end-family

An eliminator over this family learns which index is possible in each branch. The motive is the bridge between the scrutinee's index and the evidence or value that each branch must produce.

Family versus record

A record is the single-constructor case optimized for named construction and projection. A family can have zero, one, or many constructors, can be indexed, and can be recursive. Use a family when the alternatives or index relationship are meaningful; use record syntax when the value is one named product shape.

Common mistakes

• Missing or reordered branch: branch coverage no longer matches declaration order.
• Wrong arity: a recursive field needs both its value and induction-result binder.
• Weak motive: a constant result type may discard the index relationship needed by a proof.
• Quantity violation: branch bodies remain subject to erased, affine, linear, and unrestricted use.
• Fabricated emptiness: an uninhabited family does not permit constructing arbitrary evidence.

For the normative rules, see Specification: indexed families and elimination. For more examples, see the Language guide and the maintained Std.List source.