lection14.tex

\section{Лекция 14}

\newcommand{\ard}[1]{\mintinline{latex}{#1}}

\subsection{Индуктивные типы и равенства}

Возьмём исчисление конструкций $\lambda C$ \footnote{См. $\lambda$-куб} и дополним его базовыми конструкциями --- \textbf{индуктивными типами} и \textbf{равенством}.

\medskip
\textbf{Индуктивный тип:} это обобщение конструкций, которые можно получить с помощью индукции,
пользуясь некоторым набором базовых утверждений и индукционных переходов. В качестве примера можно рассмотреть аксиоматику Пеано.
Здесь конструкторами (выражениями, конструирующими объекты надлежащего типа) будут $0$ и $'$: если $n$ --- натуральное, то и $n'$ натуральное.

Таким образом, мы определяем новый тип, индуктивно задавая объекты, которые населяют его.

Рассмотрим реализацию натуральных чисел в языке Аренд.\footnote{\url{https://github.com/JetBrains/Arend/blob/master/lib/Prelude.ard}}
\begin{minted}[samepage]{latex}
\data Nat
    | zero
    | suc Nat
\where {
    func \infixl 6 + (x y : Nat) : Nat \elim y
        | zero => x
        | suc y => suc (x + y)
}
\end{minted}

Здесь \ard{zero} --- постулирует терм, населяющий \ard{Nat} (является базой индукции), а \ard{suc} из \ard{Nat} конструирует \ard{Nat} (таким образом, мы производим структурную индукцию).
В блоке \ard{where} задаются связанные с типом определения, а \ard{elim} представляет из себя сопоставление с образцом.

\medskip
\textbf{Равенство}. Традиционно рассматривается два типа равенств --- экстенсиональное и интенсиональное.
Интенсиональное основано на сравнении объектов по внутренней структуре, а экстенсиональное --- предполагает, что объекты неразличимы внешне.

Основными отличиями этих двух типов равенств являются разрешимость и сила. Интенсиональное --- разрешимо, но слабо, а экстенсиональное --- сильно, но неразрешимо.
Например, сравнение $0''$ и $0''$ интенсиональный подход успешно завершит, а при экстенсиональном подходе --- нам необходимо предоставить доказательство.

Кроме этого, важным отличием экстенсионального подхода является то, что в нём равенство термов по определению
не отличимо от пропозиционального равенства, которое уже доказывается внутри языка (происходит построение терма соответствующего типа).

\subsection{Пути и равенство в Arend}
В основе подхода языка Arend лежит HoTT --- Homotopy Type Theory.\footnote{The HoTT Book: \url{https://homotopytypetheory.org/book/}}

В нём произвольный тип $\alpha$ является некоторым пространством, а терм $A : \alpha$ --- точкой в нём.
Равенство же в топологии представляет из себя \textit{непрерывный} путь между двумя точками.

Введём интервальный тип \ard{I}, представляющий из себя интервал $[l, r]$.
Определим тип \ard{Path}.

\begin{minted}[samepage]{latex}
\data Path (A : I -> \Type) (a : A left) (a' : A right)
    | path (\Pi (i : I) -> A i)
\end{minted} 

Разберём это определение. Здесь \ard{A} --- это пространство, \ard{a} и \ard{a'} --- точки в нём.
Единственный конструктор является функцией, которая по левому концу пути вернёт конечную точку, а по правому концу --- начальную точку.

Теперь, с помощью путей, определим равенство.

\begin{minted}{latex}
\func \infix 1 = {A : \Type} (a a' : A) => Path (\lam _ => A) a a'
\end{minted}

Таким образом, равенство --- это функция, которая по типу и двум точкам возвращает
зависимый тип \ard{Path}, соединяющий две точки.

Следует обратить внимание на то, что в Arend запрещено на уровне компилятора выполнять
pattern matching по интервальному типу.
Иначе --- можно написать функцию, нарушающую непрерывность и впоследствии получить доказательство $0 = 1$:

\begin{minted}[samepage]{latex}
\func lr (a : I) : Nat
    | left => 0
    | right => 1
\end{minted}

\subsection{Основные функции}
\begin{itemize}
\item [\bf idp:] Вспомним определение равенства. Попробуем населить тип $0 = 0$. Это можно сделать так:

\begin{minted}{latex}
path (\lam _ => 0)
\end{minted}

На практике, необходимость доказать равенство является типичной ситуацией, и конструкция \ard{idp}
является удобным обобщением, составляющим путь по неявному аргументу \ard{a}.

\begin{minted}{latex}
\cons idp {A : \Type} {a : A} => path (\lam _ => a)
\end{minted}

\item [\bf coe:] Функция \ard{coe} позволяет <<разобрать>> равенство. Более формально --- она служит элиминатором для интервального типа.

\begin{minted}{latex}
\func coe (A : I -> \Type) (a : A left) (i : I) : A i
\end{minted}


Первый аргумент показывает, на каких типах определено равенство. Второй --- начальное значение. Третий --- интервал.
Результатом будет применение \ard{A} к \ard{i}.

С её помощью, например, можно показать, что у \ard{I} один элемент

\begin{minted}{latex}
-- Note: `left=i` is a correct identifier
\func left=i (i : I) : (left = i)
    => coe (\lam i => left = i) idp i
\end{minted}

Для доказательства \ard{left = right} можно применить эту же лемму

\begin{minted}{latex}
\func l=r : left = right => left=i right
\end{minted}

\item [\bf pmap:] Принимает функцию $f$ и тип равенства $A = B$. Возвращает тип $f(A) = f(B)$.
Пример: докажем, что если $a = b$, то $a+1 = b+1$.
\begin{minted}{latex}
\lemma example (a b : Nat) (p : a = b) 
    : (suc a = suc b) => pmap suc p
\end{minted}

\item [\bf absurd:] Позволяет получить любой тип из лжи (\ard{Empty}).
\begin{minted}{latex}
    \func absurd {A : \Type} (x : Empty) : A
\end{minted}

\item [\bf rewrite:] Принимает тип равенства $A = B$, некоторое выражение $t$, и эта функция переписывает его, подставляя $B$ вместо $A$.
Пример:
\begin{minted}{latex}
\lemma example (x y : Nat) (f : Nat -> Nat)
: f (x + y) = f (y + x)
    => rewrite (NatSemiring.+-comm {x} {y}) idp
\end{minted}

\item [\bf transport:] Эта функция является основным механизмом для работы \ard{rewrite}.
\begin{minted}{latex}
\func transport {A : \Type} (B : A -> \Type)
    {a a' : A} (p : a = a') (b : B a) : B a'
\end{minted}
\end{itemize}

\subsection{$\Sigma$- и $\Pi$-типы}
Иногда мы хотим оперировать с кортежами зависимых типов, например, если мы хотим,
чтобы одновременно удовлетворялись несколько условий. В языке Аренд сигма-тип --- это тип (зависимых) кортежей.

Покажем их использование на примере:
\begin{minted}[samepage]{latex}
\data DivisibleBy5
    | mkDiv5 (n : Nat) (\Sigma (m : Nat) (m * 5 = n))

\func ten : DivisibleBy5 => mkDiv5 10 (2, idp)
\end{minted}

Здесь, чтобы доказать, что число 10 делится нацело на 5, мы предоставили кортеж из частного $m$ и доказательства, что $m \cdot 5 = 10$.

Также, с помощью сигма-типов удобно требовать выполнение нескольких условий одновременно.
\begin{minted}{latex}
\lemma example (a b k : Nat) (p : a + b < k)
    : (\Sigma (a < k) (b < k))
\end{minted}

Чтобы доказать эту лемму, потребуется предоставить доказательства \ard{(a < k)} и \ard{(b < k)}.
Получить произвольный элемент из сигма-типа можно с помощью паттерн-матчинга или обращения к полям, например \ard{p.1}.

\medskip
Вспомним реализацию путей в языке Аренд. В ней использовался пи-тип~--- функция, возвращавшая начальную или конечную точку пути.
Итак, $\Pi$-тип в Arend~--- это тип зависимых функций. Такая конструкция соответствует квантору всеобщности $\forall$, так как
тип \ard{(\Pi (x : A) -> B a)} населён, когда для любого элемента \ard{a} из \ard{A} существует элемент \ard{B a}. 

Например, представим, что мы определили понятие <<делится нацело>> и хотим определить понятие простого числа $n$.
Хочется проверить, что если число делит $n$ нацело, то оно либо $1$, либо $n$. Здесь можно применить пи-типы.
\begin{minted}{latex}
\Pi (d : Nat) (k : Divisible n d) -> ((d = 1) || (d = n))
\end{minted}

\subsection{Prop, Universe}

Универсум --- это <<тип типов>>. В Arend присутствует следующая иерархия универсумов.

\begin{itemize}
    \item Все типы, которые не содержат в своём определении типы из других универсумов, принадлежат универсуму 0. Например, \ard{Int : \Type 0}
    \item Если есть функция, отображающая куда-нибудь тип, она принадлежит универсуму 1: \ard{(\Type -> Int) : \Type 1}
    \item Кумулятивная последовательность --- каждый следующий универсум включает предыдущий
\end{itemize}

Такая иерархия нужна, чтобы избежать парадоксов, например, парадокса Рассела.

Концепция похожа на сорта, но при этом она включает предыдущие в иерархии. Например, \ard{Int : \Type 100}

\medskip
Заметим, что доказательств существования \ard{Int} много --- например, $10$, $2$ или $9999$.
Давайте заведём некий набор типов, в которых всегда присутствует ровно один элемент если присутствует и назовём такой тип \textbf{собственными утверждениями}.
Чем такой тип интересен --- в нем есть утверждения, которые либо истинны, либо ложны.

Введём специальный универсум \ard{Prop}. Этот универсум состоит только из тех значений, у которых единственный элемент.

\begin{minted}{latex}
\func isProp (A : \Type) => \Pi (a a' : A) -> a = a'
\end{minted}

Такой тип может быть либо пустым, либо одноэлементным (ложь/истина).

Одно из преимуществ \ard{Prop} --- если этот тип обитаем, то мы не зависим от доказательств. Любое доказательство равно любому другому.
\begin{minted}[samepage]{latex}
\func proofIrrelevance (P : \Prop) (p q : P)
    : p = q => Path.inProp {P} p q
\end{minted}

Теперь введём понятие множества (Set). Множеством будут называться все такие элементы, у которых единственное доказательство равенства.

\begin{minted}{latex}
\func isSet (A : \Type) => \Pi (a b : A) -> isProp (a = b)
\end{minted}

Наконец, научимся делать из любого типа \ard{Prop}.

По типу \ard{a} строим тип \ard{||A||}
\begin{itemize}
    \item Если \ard{(a : A)}, то \ard{|a| : ||A||}
    \item Если \ard{(x y : A)}, то \ard{|x| = |y|}
\end{itemize}
Это называется \textbf{пропозициональным обрезанием}. В Аренде его можно сделать с помощью ключевого слова \ard{\truncated}.

Например, с помощью этой конструкции можно определить понятие <<существует>>:
\begin{minted}[samepage]{latex}
\truncated \data Exists (A : \Type) (B : A -> \Type) : \Prop
  | mkExists (a : A) (B a)
\end{minted}

Здесь тип \ard{Exists} определяет существование такого \ard{a : A}, что \ard{B a}. При этом мы не можем ``достать'' это \ard{a} из \ard{Exists}:
\begin{minted}{latex}
% Ошибка:
% Data type 'Exists' is truncated to the universe \Prop,
% which does not fit in the universe of the eliminator type: Nat
\func extract (p : Exists Nat (\lam n => n = 3)) : Nat
    | mkExists a b => a
\end{minted}

Но мы можем элиминировать \ard{Exists}, если возвращаемый тип тоже является утверждением:
\begin{minted}{latex}
\func existsSuc (p : Exists Nat (\lam n => n = 3))
    : Exists Nat (\lam n => suc n = 4)
    | mkExists n p => mkExists n (path (\lam i => suc (p @ i)))
\end{minted}

Таким образом мы можем выражать неконструктивность. Например, мы можем определить аксиому выбора через \ard{TruncP}, которое аналогично \ard{\truncated} производит пропозициональное обрезание:

\begin{minted}{latex}
\truncated \data TruncP (A : \Type) : \Prop
    | inP A

\func choice (A : \Set) (B : A -> \Set) :
    (\Pi (x : A) -> TruncP (B x)) -> TruncP (\Pi (x : A) -> B x)
\end{minted}

Эта функция недоказуема (без других аксиом). Однако если попытаться определить аксиому выбора без обрезания, то мы получим тривиальное утверждение, доказуемое в ИИВ:
\begin{minted}{latex}
\func choice (A B : \Set) (Q : A -> B -> \Prop)
    (not_empty : \Pi (x : A) -> \Sigma (y : B) (Q x y)):
    \Sigma (f : \Pi (x : A) -> B) (\Pi (x : A) -> Q x (f x))
    => (\lam x => (not_empty x).1, \lam x => (not_empty x).2)
\end{minted}

С помощью \ard{\truncated} можно обрезать не только пропозиционально, но и до других универсумов. Например, можно построить фактор-множество над типом \ard{A} с отношением эквивалентности \ard{R} с помощью обрезания до \ard{\Set}:
\begin{minted}{latex}
\truncated \data Quotient (A : \Type) (R : A -> A -> \Type) : \Set
    | inR A
    | eq (a a' : A) (r : R a a') (i : I) \elim i {
        | left => inR a
        | right => inR a'
}
\end{minted}

Число \ard{n} из \ard{\Type n} называется \textbf{предикативным уровнем} типа. Помимо уровня предикативности, универсумы также образуют иерархию по \textbf{гомотопическому уровню}, который определяется индуктивно следующим предикатом:
\[
    \texttt{is-n-type}(A) \coloneqq \begin{cases}
        \texttt{isProp}(A) & n = - 1 \\
        \Pi (x, y : A) \to \texttt{is-n'-type}(x = y) & n' = n - 1
    \end{cases}
\]
Таким образом, гомотопический уровень типа $A$ это $1 +{}$гомотопический уровень типа равенства элементов $A$ и гомотопический уровень \ard{\Prop} это $-1$. Универсум с гомотопическим уровнем \ard{n} и предикативным уровнем \ard{m} обозначается \texttt{\textbackslash{}n-Type m}.

Компилятор не всегда может доказать предикативный уровень типа, иногда нужно доказать самостоятельно с помощью \ard{\use \level}:
\begin{minted}{latex}
\data PropInType-to-Prop (A : \Type) (p : isProp A)
  | inc A
    \where {
      \use \level dataIsProp {A : \Type} {p : isProp A} 
                       (d1 d2 : PropInType-to-Prop A p) : d1 = d2
        \elim d1, d2
        | inc a1, inc a2 => pmap inc (p a1 a2)
    }
\end{minted}