Violet

← Docs

Inductive types

Syntax

\data T [params] : [indices ->] 𝓤
  | ctor1 : ...
  | ...
  | ctorn : ...

Example: Nat

\data Nat : 𝓤
  | zero : Nat
  | suc : Nat -> Nat

Example: indexed family Vec

\import nat

\data Vec (A : 𝓤) : Nat -> 𝓤
  | nil : Vec A zero
  | cons : {n : Nat} -> A -> Vec A n -> Vec A (Nat/suc n)

Parameters vs. indices

Parameters appear before : and are fixed across the whole family — every constructor returns T params. Indices appear after : and may differ per constructor; each constructor specifies which index value its result has.

In Vec below, A is a parameter (every cell of a given Vec has the same element type), while the Nat after : is an index — nil returns a Vec A zero, while cons returns a Vec A (suc n).

Generated eliminator

The distinction shows up in the eliminator the compiler generates. The parameter A is bound once at the top and shared by every cases — while the index n is quantified per case (when invoke motive) and at the point of use:

Vec/elim :
  (A : 𝓤)                                              # parameter: bound once
  (n : Nat)                                            # index: different in different cases
  (target : Vec A n)
  (motive : (m : Nat) -> Vec A m -> 𝓤)
  (case-nil : motive zero nil)
  (case-cons : {n : Nat} -> (a : A) -> (v : Vec A n) -> motive n v -> motive (suc n) (cons a v))
  -> motive n target

See also