Команда `#data`¶

Команда #data объявляет индуктивный тип: формирователь типа, его конструкторы и порождённые элиминаторы.

Синтаксис¶

#data <name> [uses (<vars>)] (<param>)* := <constructor> [| <constructor>]* (<elim-clause>)*
#data <name> [uses (<vars>)] (<param>)*

где конструктор имеет вид

<name> (<field>)*

а необязательная клауза переприписывания имеет вид

eliminate with <name> : <type>
compute with <name> : <type>

Описание¶

Объявление вводит формирователь типа, по одному обычному имени верхнего уровня на конструктор и два порождённых элиминатора: принцип индукции ind-<name> и его не зависимую версию rec-<name>. Все они живут в одном пространстве имён с остальными именами верхнего уровня, поэтому совпадение с существующим именем — ошибка. Вторая форма (без :=) объявляет пустое семейство.

Например:

#lang rzk-1
#data bool := false | true

#data coprod
  ( A B : U)
  :=
    inl (a : A)
  | inr (b : B)

порождает

#check ind-bool : (C : bool → U) → C false → C true → (b : bool) → C b
#check rec-coprod
  : ( A : U) → (B : U) → (C : U)
  → ( ( a : A) → C) → ((b : B) → C)
  → coprod A B → C

Аргументы элиминатора идут в порядке: параметры, мотив, по одному методу на конструктор (в порядке объявления), устраняемое значение. Вычисление определительное: элиминатор, применённый к конструктору точки, вычисляется в соответствующий метод, применённый к полям конструктора. Выражение match — нотация для элиминаторов, по одной ветви на конструктор.

Большие индуктивные типы

Поле конструктора, чей тип является вселенной или квантифицирует по ней (например, box (X : U)), делает тип большим. Поскольку в Rzk сейчас U : U, большой индуктивный тип — известный короткий путь к противоречию, поэтому объявление принимается с предупреждением.

Рекурсия поддерживается для непосредственно рекурсивных полей, то есть полей, чей тип — объявляемый тип, применённый к своим параметрам, как в suc (n : nat). Каждое рекурсивное поле добавляет в метод элиминатора гипотезу индукции, сразу после поля:

#data nat := zero | suc (n : nat)

#check ind-nat
  : ( C : nat → U)
  → C zero
  → ( ( n : nat) → C n → C (suc n))
  → ( x : nat) → C x

Поля конструкторов должны быть строго положительны в объявляемом типе.

Индексированные семейства записывают телескоп индексов в сорте. Конструктор индексированного семейства обязан явно указать тип результата, инстанцирующий индексы; непосредственно рекурсивное поле делает то же, и его индексы инстанцируют гипотезу индукции:

#data vec
  ( A : U)
  : nat → U
  :=
    nil : vec A zero
  | cons (n : nat) (x : A) (xs : vec A n) : vec A (suc n)

#check ind-vec
  : ( A : U)
  → ( C : (n : nat) → vec A n → U)
  → C zero (nil A)
  → ( ( n : nat) → (x : A) → (xs : vec A n) → C n xs → C (suc n) (cons A n x xs))
  → ( n : nat) → (xs : vec A n) → C n xs

Параметры (до сорта) однородны: каждый конструктор возвращает объявляемый тип, применённый ровно к переменным параметров, а затем к своим индексам.

Конструкторы путей¶

Конструктор, чей тип результата — тип-тождество над объявляемым типом, записанный как l =_{D} r, объявляет путь с источником l и целью r. Таким образом объявление становится высшим индуктивным типом в стиле книги по HoTT. Например, окружность:

#data S¹
  :=
    base
  | loop : base =_{S¹} base

Каждый конструктор пути добавляет метод в порождённые элиминаторы: уравнение между образами источника и цели под строящимся сечением, над путём для ind-S¹ (транспорт записывается через idJ, так как в Rzk нет примитивного транспорта). Поскольку метод конструктора пути ссылается на методы конструкторов точек, объявление с конструкторами путей связывает аргументы-методы по именам (m-base, m-loop):

#check ind-S¹
  : ( C : S¹ → U)
  → ( b : C base)
  → ( ℓ : idJ (S¹ , base , \ y _ → C base → C y , \ u → u , base , loop) b = b)
  → ( x : S¹)
  → C x

#check rec-S¹ : (C : U) → (b : C) → (ℓ : b = b) → S¹ → C

Вычисление следует книге по HoTT: β остаётся определительной на конструкторах точек и пропозициональна на конструкторах путей. Ничего не вычисляется, когда элиминатор встречает путь; вместо этого объявление порождает по одному правилу вычисления на конструктор пути и элиминатор, с именами compute-ind-<name>-<con> и compute-rec-<name>-<con>, утверждающему, что ap/apd элиминатора на пути равно методу.

Источник и цель пути обязаны строиться из конструкторов объявления и полей самого конструктора (непосредственно рекурсивное поле допустимо, и его образ — гипотеза индукции). Например, пропозициональное усечение:

#data trunc
  ( A : U)
  :=
    in-trunc (a : A)
  | squash (x : trunc A) (y : trunc A) : x =_{trunc A} y

Клаузы переприписывания¶

Объявление может заканчиваться клаузами переприписывания: eliminate with называет один из двух порождённых элиминаторов, compute with — порождённое правило вычисления, и обе задают тип записью пользователя. Проверяется, что эта запись определительно равна каноническому порождённому типу, при этом формирователь типа и конструкторы находятся в области видимости. Поскольку определительно равные типы взаимозаменяемы, значения и правила вычисления не затрагиваются; меняется только сохранённая запись типа, и она распространяется всюду, где тип отображается, например в подсказки при наведении и в цели. Если запись не является определительно равной каноническому типу, ошибка печатает канонический тип.

Важнее всего это для конструкторов путей, чьи канонические типы раскрывают транспорт и ap/apd через idJ. С библиотечными transport, ap и apd (каждый определим из idJ до любых объявлений) окружность читается так:

#define transport
  ( A : U) (C : A → U) (x y : A) (p : x =_{A} y) (u : C x)
  : C y
  := idJ (A , x , \ y' _ → C x → C y' , \ v → v , y , p) u

#define ap
  ( A B : U) (f : A → B) (x y : A) (p : x =_{A} y)
  : f x =_{B} f y
  := idJ (A , x , \ y' _ → f x =_{B} f y' , refl , y , p)

#define apd
  ( A : U) (C : A → U) (f : (a : A) → C a) (x y : A) (p : x =_{A} y)
  : transport A C x y p (f x) =_{C y} f y
  := idJ (A , x , \ y' q → transport A C x y' q (f x) =_{C y'} f y' , refl , y , p)

#data circle
  :=
    pt
  | turn : pt =_{circle} pt
  eliminate with ind-circle
    : ( C : circle → U)
    → ( b : C pt)
    → ( ℓ : transport circle C pt pt turn b = b)
    → ( x : circle)
    → C x
  compute with compute-rec-circle-turn
    : ( C : U)
    → ( b : C)
    → ( ℓ : b = b)
    → ap circle C (rec-circle C b ℓ) pt pt turn = ℓ
  compute with compute-ind-circle-turn
    : ( C : circle → U)
    → ( b : C pt)
    → ( ℓ : transport circle C pt pt turn b = b)
    → apd circle C (ind-circle C b ℓ) pt pt turn = ℓ

Клаузы точно так же доступны и на объявлениях без конструкторов путей, например чтобы записать тип элиминатора через раскрывающийся синоним.

Текущие ограничения¶

На данный момент:

рекурсивные поля должны быть непосредственными: положительное поле функционального типа, как node (f : A → tree) (форма W-типа), пока не поддерживается;
индексы должны быть обычными типами (индексы-кубы и индексы-формы не поддерживаются), и конструкторы не могут принимать аргументы-кубы и аргументы-формы (над направленным интервалом они объявляли бы направленные клетки);
конструкторы путей не поддерживаются в индексированных семействах, и поддерживаются только пути между точками: носитель, сам являющийся типом-тождеством, или поле типа-тождества (высший путь, как в 0-усечении) отвергается.

Отметим также, что индуктивный тип приходит ровно со своим принципом индукции; взаимодействие типа с симплициальной структурой — отдельный вопрос. См. предупреждение о дискретности в разделе Зависимые типы.

Команда #data¶