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. The kernel compiles this syntax to de Bruijn indices.

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: data/Nat.rec takes type-level when the motive returns a natural number.

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 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.

Strict positivity

A recursive occurrence must be an entire constructor field. Any other [:self] fails with :kernel/non-strictly-positive, including a field of type A -> self:

(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 pins for native arithmetic.

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. The kernel type-checks every generated type before it accepts the block. The formal rules are in The calculus.