Inductive types

You declare an inductive type as a block: a map with the type, its parameters and its constructors. kernel/add-inductive-block (source) checks the block and adds the type, one constructor per case and a recursor in one step.

Declare a block

rainbow.data.inductive declares data/Nat with two constructors (source):

(def zero [:zero])
(def type-level [:succ zero])

(def nat-spec
  {:block/schema-version 1
   :block/alias 'data/Nat
   :block/universes []
   :block/parameters []
   :block/sort-level type-level
   :block/constructors
   [{:constructor/alias 'data/zero :constructor/fields []}
    {:constructor/alias 'data/succ
     :constructor/fields [{:field/name 'predecessor :field/type [:self]}]}]})

:block/universes is a vector of distinct symbols, :block/parameters a vector of {:parameter/name ... :parameter/type ...}, and :block/sort-level the level of the universe the type lives in. :block/constructors must not be empty. A field is {:field/name symbol :field/type ast}, and [:self] as a field type is a recursive occurrence.

A field can depend on earlier fields, never on later ones. Field names must be distinct and must not reuse a parameter name (:kernel/invalid-constructor-fields). The kernel compiles this syntax to de Bruijn indices.

A block declares exactly one type. There are no mutual inductives, no nested ones (a field of type [:app List [:self]] is rejected) and no indexed families.

What the kernel generates

Adding nat-spec creates four declarations, shown with names in place of ids and indices:

data/Nat      : Sort 1
data/zero     : Nat
data/succ     : Nat -> Nat
data/Nat.rec  : (motive : Nat -> Sort m)
                -> motive zero
                -> ((predecessor : Nat) -> motive predecessor -> motive (succ predecessor))
                -> (target : Nat)
                -> motive target

The recursor <alias>.rec takes the parameters, the motive, one case per constructor and the target. A case gets the constructor’s fields, each [:self] field followed by its result. The recursor adds one universe parameter, _rainbow_motive_universe (the m above), so the motive can return a type in any universe (the name is reserved and cannot be a block’s own universe parameter): data/Nat.rec takes type-level when the motive returns a natural number. Propositions are the exception, below.

A recursor applied to a constructor reduces to the matching case (iota reduction). rainbow.data.inductive checks this with the identity recursion on 2:

(def nat-step (term/lambda-term nat
                                (term/lambda-term nat
                                                  (apply* successor (term/bound 0)))))
(apply* nat-rec nat-motive zero-term nat-step two)

kernel/normalize reduces it to succ (succ zero) in 7 steps. A recursor turns a literal such as [:nat 2] into succ [:nat 1].

Parameters

data/List has one parameter, the element type (source):

(def U [:param 'u])

(def list-spec
  {:block/schema-version 1
   :block/alias 'data/List
   :block/universes ['u]
   :block/parameters
   [{:parameter/name 'A :parameter/type [:sort U]}]
   :block/sort-level U
   :block/constructors
   [{:constructor/alias 'data/nil :constructor/fields []}
    {:constructor/alias 'data/cons
     :constructor/fields [{:field/name 'head :field/type [:var 'A]}
                          {:field/name 'tail :field/type [:self]}]}]})

Parameters lead every generated type: data/List : (A : Sort u) -> Sort u and data/cons : (A : Sort u) -> A -> List A -> List A. Each constructor returns the type applied to exactly the parameters, so blocks have no indices.

list/length in the same file calls the recursor directly. data/List.rec takes two levels here, [U type-level]:

(app (constant-form 'data/List.rec [U type-level])
     'A
     (lambda [['ignored (list-of U 'A)]]
             (constant-form 'data/Nat []))
     (constant-form 'data/zero [])
     (lambda [['head 'A]
              ['tail (list-of U 'A)]
              ['induction-hypothesis (constant-form 'data/Nat [])]]
             (app (constant-form 'data/succ [])
                  'induction-hypothesis))
     'xs)

To get the motive and case goals built for you, use the induction tactic, shown in The REPL and tactics.

Field universes

A field that is not [:self] must live in a universe no higher than the type’s own, for every value of the universe parameters. The comparison is sound but may be incomplete: the kernel can refuse a field whose bound it cannot prove. A type in Sort 1 with a field of type Sort 1 is refused, because that field lives in Sort 2:

(kernel/add-inductive-block (environment/empty-environment)
  {:block/schema-version 1 :block/alias 'bad/U :block/universes [] :block/parameters []
   :block/sort-level [:succ [:zero]]
   :block/constructors
   [{:constructor/alias 'bad/mk
     :constructor/fields [{:field/name 'A :field/type [:sort [:succ [:zero]]]}]}]})
;=> {:status :rejected,
;    :error {:constructor 0, :field A, :field-level [:succ [:succ [:zero]]],
;            :sort-level [:succ [:zero]], :error/category :kernel/field-universe-too-large},
;    :message "Constructor field lives in a universe above the inductive type's sort"}

Propositions get no exception: a block in [:sort [:zero]] with a field in a larger universe is refused too.

Eliminating a proposition

A recursor of a type with two or more constructors can return something above Prop only when the type is not a proposition. Otherwise a function could tell two proofs of one proposition apart, which contradicts the proof-irrelevance axiom. For a block in [:sort [:zero]] with two constructors, the recursor at level [:zero] checks, and at [:succ [:zero]] it fails with :kernel/large-elimination-from-prop. A proposition with one constructor can still be eliminated into any universe.

data/Sum, data/Option and data/List are propositions when their universe arguments are 0, so their recursors are restricted there; data/Product has one constructor and is not restricted. When the answer depends on a universe parameter, the kernel records the requirement on the declaration that uses the recursor and checks it wherever that declaration is used.

Recursive occurrences

A recursive occurrence must be an entire constructor field. Any other [:self] in a field type fails with :kernel/non-strictly-positive, including a field of type A -> self; [:self] in a parameter type fails with :kernel/malformed-block-type. This is stricter than the strict positivity of Lean or Rocq: since a field of type A -> T is rejected, infinitely branching types cannot be declared.

(kernel/add-inductive-block (environment/empty-environment)
  {:block/schema-version 1 :block/alias 'bad/T :block/universes [] :block/parameters []
   :block/sort-level [:succ [:zero]]
   :block/constructors
   [{:constructor/alias 'bad/mk
     :constructor/fields [{:field/name 'f :field/type [:pi [['x [:sort [:zero]]]] [:self]]}]}]})
;=> {:status :rejected,
;    :error {:constructor 0, :field ..., :error/category :kernel/non-strictly-positive},
;    :message "Recursive occurrence must be an entire constructor field"}

Ids

Block and member ids are computed from the spec with names replaced by positions (Content addressing). So data/Nat gets sha256:3506a443... in an empty environment, in the corpus checkpoints and in the kernel’s pin that types natural-number literals.

Before 1.1.0, binder numbering restarted at every nested Pi, so “earlier kernels could conflate distinct field types and accept an axiom-free proof of False” (trusted base). The nested inductive-binder identity repair changes content ids only for affected blocks. No shipped declaration depended on the defect, and the default checkpoint replays to the same environment id (CHANGELOG). Replay anything checked before the repair: “a pre-repair pass is not a soundness clearance”.

Members enter together. kernel/add-declaration refuses a lone block member (:kernel/standalone-block-member), and add-inductive-block refuses a block whose aliases already exist, or whose supplied :rainbow/id does not match (:kernel/forged-inductive-block-id). The kernel type-checks every generated type before it accepts the block, and gives each member the axioms of the constants in its type, so a theorem using a constructor whose field has a postulated type reports that axiom (CHANGELOG). The formal rules are in The calculus.