Типы и термы¶

#lang rzk-1

Функции (зависимые произведения)¶

Типы функций (зависимых произведений) \(\prod_{x : A} B\) записываются как (x : A) -> B x. Значения типов функций — это \(\lambda\)-абстракции, записанные одним из следующих способов:

\x -> <body> — это обычно подходит;
\(x : A) -> <body> — это иногда помогает проверщику типов.

Зависимые суммы¶

Тип зависимой суммы \(\sum_{x : A} B\) записывается как ∑ (x : A), B или Sigma (x : A), B. Значения типов зависимых сумм — это пары, записанные как (x, y).

Чтобы получить доступ к компонентам зависимой пары p, используйте first p и second p.

Warning

first и second не являются валидным синтаксисом без аргумента!

Локальные определения (`let`)¶

Локальные определения записываются как let x := val in body и могут нести необязательную аннотацию типа: let x : A := val in body. Связываемое имя находится в области видимости только в body.

#def example-let
  : Unit
  :=
  let x := unit in
  let y : Unit := x in
  y

В связке поддерживаются образцы, поэтому можно прямо разобрать пару:

#def example-let-pair
  : Unit
  :=
  let (a , b) := (unit , unit) in
  a

Типы-тождества¶

Тип-тождество (путь) \(x =_A y\) записывается как x =_{A} y.

Tip

Указание типа A необязательно: x = y — это валидный синтаксис!

Для любого значения существует конструктор refl_{x : A}, тип которого — x =_{A} x, когда x : A

Tip

Указание терма и типа refl_{x : A} необязательно: refl_{x} и refl — оба валидные выражения.

Индукция по путям выполняется с использованием элиминатора путей \(\mathcal{J}\):

для
любого типа \(A\) и \(a : A\),
семейства типов \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) и
\(d : C(a,\mathsf{refl}_a)\) и
\(x : A\) и \(p : a =_A x\)
мы имеем \(\mathcal{J}(A, a, C, d, x, p) : C(x, p)\)

В rzk-1 мы пишем idJ(A, a, C, d, x, p)

Warning

idJ не является валидным синтаксисом без ровно 6-ти аргументов в скобках!