Время от времени мне встречаются вопросы по математике, которые в каком-то смысле можно назвать «грамматически неверными».

Пример. «Интервал $[0, 1]$ является замкнутым или открытым?»
Пример. «Является ли $\{ 1, 2, 3 \}$ группой?»
Пример. «Каков ряд Фурье для $\sin x + \sin \pi x$?»

А вот ещё более глупые примеры.

Пример. «Является ли прямоугольник простым?»
Пример. "$17 \in 3$?"
Пример. «Каков ряд Фурье для пустого множества?»

Объединяет все эти примеры то, что они являются ошибками типизации: это попытки применения некого математического процесса к математическому объекту, который никак не может быть входными данными для него. Если для ответа на эти вопросы вы попытаетесь написать программу на каком-нибудь высоко математическом языке программирования, то она (я надеюсь!) не скомпилируется.

Математические объекты обычно не воспринимаются явно как имеющие типы в том же смысле, что и объекты в языках программирования с системой типов. Предполагается, что обычная математика должна формализироваться в системе Цермело — Френкеля (ZF), возможно, с аксиомой выбора, а в ZF каждый математический объект конструируется как множество. В этом смысле все эти объекты имеют одинаковый тип. (В частности, вопрос "$17 \in 3$" вполне логичен в ZF! И это одна из причин, по которой стоит не любить ZF в качестве основы для математики.) Однако, мне кажется, что на практике математические объекты неявно воспринимаются, как имеющие типы, и такой образ мышления математики усваивают, но не часто обсуждают.

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

Неформальное описание математических типов


Неформально можно сказать, что тип математического объекта описывает разновидность этого объекта.

Пример. Объект $2$ имеет тип $\texttt{Nat}$ (натуральное число).
Пример. Объект $-2$ имеет тип $\texttt{Int}$ (целое).
Пример. Объект $\frac{1}{2}$ имеет тип $\texttt{Rat}$ (рациональное число).
Пример. Объект $(2, 3)$ имеет тип $\texttt{Nat} \times \texttt{Nat}$ (пара натуральных чисел).
Пример. Объект $30^{\circ}$ имеет тип $\texttt{Deg}$ (градус).
Пример. Объект $x \mapsto x^2$ имеет тип $\texttt{Nat} \to \texttt{Nat}$ (функция отображается из натуральных чисел в натуральные числа).
Пример. Объект $\texttt{true}$ имеет тип $\texttt{Bool}$ (Boolean).

А вот менее простые примеры:

Пример. Объект $\mathbb{Z}$ имеет тип $\texttt{Grp}$ (группа).
Пример. Объект $S^2$ имеет тип $\texttt{Top}$ (топологическое пространство).
Пример. Объект $X \mapsto H_1(X)$ имеет тип $\texttt{Top} \to \texttt{Grp}$ (функция отображается из топологических пространств в группы).

Типы помогают понять, какие действия мы можем совершать с набором математических объектов.

Пример. Можно взять два объекта типа $\texttt{Nat}$ и сложить или перемножить их. Другими словами, существуют функции $+, \times : \texttt{Nat} \times \texttt{Nat} \to \texttt{Nat}$.
Пример. Можно взять два объекта типа $\texttt{Int}$ в дополнение к сложению и умножению вычесть их. Другими словами, существуют функции $+, \times, - : \texttt{Int} \times \texttt{Int} \to \texttt{Int}$.
Пример. Можно взять объект типа $\texttt{Deg}$ и применить к нему тригонометрические функции. Другими словами, существуют функции $\texttt{sin}, \texttt{cos} : \texttt{Deg} \to \texttt{Real}$.
Пример. Если $\texttt{A}, \texttt{B}$ являются типами, то можно взять объект типа $\texttt{A}$ и другой объект типа $\texttt{A} \to \texttt{B}$, чтобы применить последний к первому. Другими словами, существует функция $\texttt{eval} : \texttt{A} \times (\texttt{A} \to \texttt{B}) \to \texttt{B}$.

Тип $\texttt{Bool}$ занимает в этой теории особое место. Существует всего два объекта этого типа, а именно $\texttt{true}$ и $\texttt{false}$, а функции, на выходе дающие значения $\text{Bool}$, можно использовать для проверки того, верно ли свойство.

Пример. Можно взять натуральное число и спросить, является ли оно простым. Другими словами, существует функция $\texttt{isPrime} : \texttt{Nat} \to \texttt{Bool}$.
Пример. Если $\texttt{A}$ является типом, то можно взять два объекта типа $\texttt{A}$ и спросить, равны ли они. Другими словами, существует функция

$\displaystyle \texttt{isEqual} : \texttt{A} \times \texttt{A} \to \texttt{Bool}$


которую мы также можем записать с помощью знака равенства $=$.
Пример. Можно взять два целых числа и спросить, больше ли первое или равно второму. Другими словами, существует функция

$\ge : \texttt{Int} \times \texttt{Int} \to \texttt{Bool}$


Как следует из этих примеров, существует множество способов комбинирования типов для создания новых типов; они называются конструкторами типов.
Пример. Объект, имеющий тип-произведение $\texttt{A} \times \texttt{B}$, является парой объектов типа $\texttt{A}$ и $\texttt{B}$.
Пример. Объект, имеющий тип-сумму $\texttt{A} + \texttt{B}$ является или объектом типа $\texttt{A}$, или объектом типа $\texttt{B}$.
Пример. Объект функционального типа $\texttt{A} \to \texttt{B}$, также иногда записываемый как $\texttt{B}^{\texttt{A}}$ — это функция, получающая на входе объекты типа $\texttt{A}$ и возвращающая на выходе объекты типа $\texttt{B}$.

(Эти конструкции могут показаться знакомыми любителям теории категорий: в ней все они являются просто произведением, копроизведением и экспоненциалом. Другими словами, категории типов являются бидекартово замкнутыми категориями.)

С помощью представленных выше простых конструкторов типов мы можем создавать более сложные конструкторы типов. Например, имея тип $\texttt{A}$ мы можем создать тип-список $\texttt{[A]}$, который является типом (конечных) списков элементов типа $\texttt{A}$:

$\displaystyle \texttt{[A]} = \texttt{1} + \texttt{A} + \texttt{A} \times \texttt{A} + \texttt{A} \times \texttt{A} \times \texttt{A} + ...$


(где $\texttt{1}$ — это особый тип, называемый типом-единицей; его определяющая характеристика заключается в том, что существует только один объект типа-единицы, который мы будем называть точкой). Эвристически тип-список можно записать как «геометрический ряд» $\frac{ \texttt{1} }{ \texttt{1} - \texttt{A} }$.

Система обозначений


Выше мы использовали запись $\texttt{f} : \texttt{A} \to \texttt{B}$ для обозначения того, что $\texttt{f}$ был объектом типа $\texttt{A} \to \texttt{B}$. Логично будет обобщить эту запись на произвольные типы, чтобы $\texttt{a} : \texttt{A}$ обозначало, что $a$ является объектом типа $\texttt{A}$. Это будет объявлением типа.

Типобезопасность и ошибки типизации


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

Пример. «Является ли $\{ 1, 2, 3 \}$ группой?»
Пример. «Каков ряд Фурье для $\sin x + \sin \pi x$?»

Пример. «Интервал $[0, 1]$ является замкнутым или открытым?» Функции $\texttt{isClosed}$ и $\texttt{isOpen}$ не могут получать на входе множество или даже топографическое пространство; они получают на входе пары $(X, S)$, где $X$ — это топологическое пространство, а $S$ — подпространство $X$ (и выдают на выход то, является ли $S$ замкнутым или открытым подмножеством $X$). Другими словами, они имеют тип не $\texttt{Top} \to \texttt{Bool}$, а тип $\texttt{Pairs} \to \texttt{Bool}$. Вопрос, является ли $[0, 1]$ открытым или замкнутым, зависит от того, рассматривается ли он как подмножество самого себя или, допустим, $\mathbb{R}$.

Пример. «Является ли $\{ 1, 2, 3 \}$ группой?» Функция $\texttt{isGroup}$ не получает на входе множество; она получает на входе пары $(X, \cdot)$, где $X$ — это множество, а $\cdot$ — двоичная операция над $X$ (магма). Другими словами, она имеет тип не $\texttt{Set} \to \texttt{Bool}$, а тип $\texttt{Magma} \to \texttt{Bool}$.

Пример. «Каков ряд Фурье для $\sin x + \sin \pi x$?» Функция $\texttt{FourierSeries}$ не получает на входе функцию на $\mathbb{R}$; она получает на входе периодическую функцию на $\mathbb{R}$, например, с периодом $2 \pi$ или, аналогично, функция на $\sin x + \sin \pi x$ не является периодической ни с каким периодом. Другими словами, $\texttt{FourierSeries}$ имеет тип не $(\texttt{Real} \to \texttt{Complex}) \to (\texttt{Int} \to \texttt{Complex})$, а тип $(\texttt{Circle} \to \texttt{Complex}) \to (\texttt{Int} \to \texttt{Complex})$.

Более глупые примеры можно проанализировать аналогично.

Поиск ошибок типизации, или проверка типов помогает в отладке математических вычислений так же, как компилятор ищет ошибки типизации для отладки кода. Например, когда мы видим выражение в виде $a = b$, то прежде чем проверять его истинность, можно проверить, имеет ли оно вообще смысл, удостоверившись, что $a$ и $b$ имеют один тип. Это очень обобщённая версия анализа размерности.

Проверка типов также является способом понимания новых математических тем. Если вы пока не можете пока произносить правильно типизированные предложения по нужной теме (что могут определить другие люди, знающие предмет), то вы ещё не разобрались в типах основных объектов или функций этой области. Например, если вы говорите «фундаментальная группа...», то вам нужно закончить предложение или фразой «точечного топологического пространства» или «линейно-связанного топологического пространства». В противном случае, вы не понимаете важного аспекта определения фундаментальной группы, а именно роли базовых точек.

Приведение типов, создание подтипов и перегрузка


Проверку типов нетривиальной задачей может сделать то, что большинство математических объектов естественным образом считаются имеющими несколько типов. Например, выше мы сказали, что число $2$ имеет тип $\texttt{Nat}$, но также очевидно, что оно имеет тип $\texttt{Int}, \texttt{Rat}, \texttt{Real}$ и даже $\texttt{Complex}$. Один из способов описания этой ситуации заключается в функциях приведения типов

$\displaystyle \texttt{Nat} \to \texttt{Int} \to \texttt{Rat} \to \texttt{Real} \to \texttt{Complex}$


которые преобразуют объекты в разные типы. Если есть оператор приведения типа $\texttt{A} \to \texttt{B}$, то мы можем использовать объекты типа $\texttt{A}$ в качестве входных данных функций, ожидающих объекты типа $\texttt{B}$, если сначала выполним приведение типа.

Ещё один способ описания этой ситуации заключается в том, что некоторые типы являются подтипами других типов; другими словами, вместо набора функций приведения типов вышеуказанная ситуация описывает цепочку включений подтипов. Создание подтипов позволяет объектам иметь одновременно несколько типов, а не быть определённого типа в определённой точке каких-нибудь вычислений.

Подтипы имеют интересную связь с функциональными типами. Если $\texttt{B}'$ является подтипом $\texttt{B}$, то функциональный тип $\texttt{A} \to \texttt{B}'$ является подтипом $\texttt{A} \to \texttt{B}$, но если $\texttt{A}'$ является подтипом $\texttt{A}$ (функция, выдающая на выходе объекты типа $\texttt{B}'$, также выдаёт на выходе объекты типа $\texttt{B}$), то функциональный тип $\texttt{A}' \to \texttt{B}$ является не подтипом, а надтипом $\texttt{A} \to \texttt{B}$ (функция, получающая на входе объекты типа $\texttt{A}$, также может получать объекты типа $\texttt{A}'$). Другими словами, создание функциональных типов ковариантно в выходных типах, но контравариантно во входных типах относительно подтипов.

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

Третий способ описания этой ситуации заключается в том, что функции в математике перегружены, и это описание наверно ближе всего к математической практике. Перегрузкой называется практика задания функций, имеющих одинаковое название, но получающих разные типы входных данных. Например, символ сложения $+$ относится не к одной, а к нескольким функциям, которые имеют одинаковое название, т.е.

$+ : \texttt{Nat} \times \texttt{Nat} \to \texttt{Nat}$


$+ : \texttt{Int} \times \texttt{Int} \to \texttt{Int}$


$+ : \texttt{Rat} \times \texttt{Rat} \to \texttt{Rat}$


$+ : \texttt{Real} \times \texttt{Real} \to \texttt{Real}$


$+ : \texttt{Complex} \times \texttt{Complex} \to \texttt{Complex}$


и так далее. Более обобщённо мы можем использовать $+$ для операции сложения на любом кольце, и даже ещё более обобщённо — для операции группировки в любой абелевой группе. Мы даже использовали его выше для обозначения типов сумм!

С показательной записью $a^b$ дело намного хуже. Она может относиться к функциям любого из следующих типов:

$\displaystyle \texttt{Nat} \times \texttt{Nat} \to \texttt{Nat}$


$\displaystyle \texttt{PosReal} \times \texttt{Real} \to \texttt{Real}$


$\displaystyle \texttt{PosReal} \times \texttt{Complex} \to \texttt{Complex}$


или даже ещё более обобщённо, $a$ может быть элементом группы, а $b$ может быть целым или $a$ может быть $e$, а $b$ может быть элементом и мы даже использовали показательную запись для обозначения функциональных типов! См. также этот вопрос в math.SE.

Кажется, перегрузка сбивает студентов с толку, и я думаю, что частично причина заключается в том, что математики редко явно говорят о ней, когда применяют её. Перегрузка не так плоха, пока все её отличающиеся экземпляры по крайней мере логично связаны друг с другом, но иногда математические концепции перегружаются без всяких причин, кроме исторических, например, слова «нормальный» и «правильный». Это ещё больше запутывает студентов: иногда одно слово используется в двух разных контекстах из-за логической связи, например, «нормальное расширение» и «нормальные подгруппы», но иногда её просто нет. См. также этот вопрос на MO.

Рекурсивные типы


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

Пример. Тип $\texttt{Nat}$ натуральных чисел может быть рекурсивно определён как

$\texttt{Nat} = \texttt{1} + \texttt{Nat}$


то есть, натуральное число является или точкой (а именно $1$), или другим натуральным числом (а именно его предшествующим).

Пример. В более общем случае, тип-список $\texttt{[A]}$ может быть рекурсивно определён как

$\displaystyle \texttt{[A]} = \texttt{1} + \texttt{A} \times \texttt{[A]}$


то есть список элементов типа $\texttt{A}$ является или точкой, или элементом типа $\texttt{A}$ (а именно началом списка) вместе со списком элементов типа $\texttt{A}$ (то есть оставшейся частью списка). В частности, $\texttt{Nat}$ — это просто тип $\texttt{[1]}$ списка точков. Стоит заметить, что это именно то соотношение, которое должно удовлетворяться «геометрическим рядом» $\frac{\texttt{1}}{\texttt{1} - \texttt{A}}$.

Пример. Тип $\texttt{Tree}$ (полностью двоичных) деревьев (с корнем) можно рекурсивно определить как

$\displaystyle \texttt{Tree} = \texttt{1} + \texttt{Tree} \times \texttt{Tree}$


то есть дерево — это или точка или пара деревьев (а именно пара деревьев, полученная удалением их корня).

Пример. Разновидность типа $\texttt{Set}$ множеств можно рекурсивно определить как

$\displaystyle \texttt{Set} = (\texttt{Set} \to \texttt{Bool})$


то есть множество — это функция множеств, которая возвращает или true (для содержащихся в нём элементов), или false (для элементов, которых в нём нет).

Пример. Тип $\texttt{Game}$ (необязательно конечных) комбинаторных игр может быть рекурсивно определён как

$\displaystyle \texttt{Game} = (\texttt{Game} \to \texttt{Bool}) \times (\texttt{Game} \to \texttt{Bool})$


то есть игра — это пара функций игр, которые мы можем назвать $\texttt{L}$ и $\texttt{R}$. Строго говоря, комбинаторную игру на самом деле нужно называть позицией игры, поскольку она описывает некий конкретный момент игры (например, начало шахматной партии), а не то, что мы обычно называем игрой (например, шахматы). Мы воспринимаем игры как нечто, во что играют два человека, левый и правый, и в любой позиции игры левый имеет возможные варианты позиций игры, в которые он может её сдвинуть, а именно такие позиции, для которых $\texttt{L}$ возвращает true, а правый тоже имеет некие возможные варианты позиций игры, в которые он может сдвинуться, а именно такие позиции, для которых $\texttt{R}$ возвращает true.

Конвей заметил, что комбинаторные игры напоминают обобщение обоих порядковых чисел (которое можно описать относительно множества порядковых чисел) и дедекиндовых сечений (которые можно описать парой множеств рациональных чисел). Он использовал эту связь для определения большого класса чисел с помощью игр; подробнее см. в On Numbers and Games.

Определённый нами ранее тип $\texttt{Set} = (\texttt{Set} \to \texttt{Bool})$, можно также воспринимать как тип беспристрастных игр, то есть игр, в которых возможные ходы не зависят от того, какой игрок играет.

(Для любителей теории категорий: рекурсивные типы являются инициальными алгебрами относительно соответствующего эндофунктора категории типов.)

Функции, получающие на входе рекурсивный тип, тоже можно определить рекурсивно. Примеры с натуральными числами вам должны быть уже знакомы; вот ещё и другие примеры.

Пример. Длину списка можно определить рекурсивно следующим образом: длина точки — это $0$. Если список не является точкой, то он состоит из элемента и подсписка, и тогда длина списка на единицу больше длины подсписка. (Я мог бы записать это псевдокодом, но не знаю чёткого способа отображения псевдокода на сайте с WordPress.)

Пример. В более общем смысле, для любых двух типов $\texttt{A}, \texttt{B}$ существует функция

$\texttt{map} : (\texttt{A} \to \texttt{B}) \to (\texttt{[A]} \to \texttt{[B]})$


которая называется map, получающая на входе функцию $\texttt{f} : \texttt{A} \to \texttt{B}$, а на выходе возвращающая функцию $\texttt{map(f)} : \texttt{[A]} \to \texttt{[B]}$, рекурсивно определяемую следующим образом: если входной список пуст, то таким же является выходной список. В противном случае входной список состоит из объекта типа $\texttt{A}$ и подсписка, а $\texttt{map(f)}$ применяет $\texttt{f}$ к объекту, а затем $\texttt{map}(f)$ к подсписку, и все они вместе составляют выходной список. Длина списка функции получается применением $\texttt{map}$ к уникальной функции $\texttt{A} \to \texttt{1}$.

(Любители теории категорий увидят, что, по сути, в этой записи конструктор списка является функтором. Существуют даже языки программирования типа Haskell, распознающие этот факт и использующие его.)

Пример. Высота дерева может быть рекурсивно определена следующим образом: высота точки равна $0$. Если дерево не является точкой, то оно имеет два поддерева, и тогда высота дерева на единицу больше максимума высоты его поддеревьев.

Пример. Игры с гарантированным завершением можно упорядочить на четыре непересекающихся класса: игра является

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

Здесь под «победой» понимаются победы в условиях обычной игры, когда проигрывает первый игрок, который не может сделать ход. Вышеперечисленные классы соответствуют четырём функциям

$\texttt{isPositive}, \texttt{isNegative}, \texttt{isZero}, \texttt{isFuzzy} : \texttt{Game} \to \texttt{Bool}$


которые можно рекурсивно определить через друг друга следующим образом:

  • Игра положительна тогда и только тогда, когда хотя бы один из вариантов левого является положительным или нулевым, а все варианты правого положительны или нечётки.
  • Игра отрицательна тогда и только тогда, когда все варианты левого отрицательны или нечётки, и хотя бы один из вариантов правого отрицательный или нулевой.
  • Игра нулевая тогда и только тогда, когда ни один из вариантов левого не положительный и не нулевой, и ни один из вариантов правого не отрицательный и не нулевой.
  • Игра нечёткая тогда и только тогда, когда хотя бы один из вариантов левого положительный или нулевой и хотя бы один из вариантов правого отрицательный или нулевой.

(Для любителей теории категорий: рекурсивно определяемые функции являются применением универсального свойства инициальных алгебр.)

Рекурсивные типы — это ещё одна причина считать, что в математике есть система типов: они позволяют гораздо подробнее записывать рекурсию, чем она обычно явно упоминается в математике, где мы записываем её с помощью индукции (рекурсия над $\texttt{Nat}$) или иногда трансфинитной индукции (рекурсия над изменённым $\texttt{Set}$). Рекурсивные же типы, наоборот, обеспечивают общую запись структурной индукции. Часто мы можем свести случаи нужной нам структурной индукции к обычной индукции (например, если мы хотим выполнить структурную индукцию для деревьев, то мы можем выполнить обычную индукцию для их вершин), но концептуально структурная индукция более четка (например, мы можем выполнить структурную индукцию для деревьев без выделения конкретной функции вершин).

Заключение


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