Underskyer1 Sep 2 2023 at 15:16

Теория типов

Medium

43 min

33K

Programming*Scala*Functional Programming*

Review

From sandbox

Так нейронные сети понимают "теорию типов".

Мы так привыкли к типам, что редко задаёмся вопросом, что же они такое на самом деле? А главное - почему возникла необходимость в их использовании? Этот поверхностный обзор сделан для того, чтобы продемонстрировать, как типы и другие связанные абстракции являются следствием из обобщения условий различных задач.

В данной статье освещаются такие вопросы:

почему на основе теории множеств зародилась концепция типов;
какие основные понятия естественно следуют из определения типа;
что такое изоморфизмы типов, и как они реализуется в программировании;
как соотносятся типы с множествами и классами;
как типы помогают обеспечивать корректность алгоритмов.

Предисловие

Не секрет, что программирование основывается на глубокой математической теории. Многие ключевые понятия, которые встречаются в различных областях компьютерных наук, пришли именно из математики. Поэтому всем, кто хочет быть программистом, было бы здорово получить более широкое видение предмета - разобраться в самой математической основе программирования.

Но, зачастую, это возвышенное намерение наталкивается на высокий порог вхождения в высшую математику. Основная проблема заключается в традиционных особенностях математической литературы - нарочитой оторванности от реальности, от практических задач. Типичный математический текст начинается со знакомства со "взятой с потолка" абстракцией, и потом рассматриваются её "удивительной красоты" свойства. И только в редких работах где-то в конце можно увидеть коротенькую заметку, что, мол, какие-то физики нашли как применить эту "красоту" для каких-то там своих нужд.

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

Теория типов - очень богатая тема, поэтому здесь придётся ограничится лишь самыми ключевыми аспектами. Многое останется за кадром - обобщённые, рекурсивные, зависимые типы и многое другое. Практически не будет упоминаться теория категорий, хотя будут использоваться некоторые понятия оттуда. Всё это - очень интересные, но достаточно самостоятельные темы, которые имеет смысл освещать отдельно.

В обзоре допущены некоторые вольности трактовки, неточности. По большей части это сделано нарочно, чтобы упростить подачу, снизить порог вхождения. Но наверняка там хватает и ошибок, связанных с недостаточным пониманием темы автором)). Ожидается, что знающие люди в комментариях будут посылать в правильных направлениях, но всё же надеюсь, что этот обзор приоткроет завесу тайны над типами с не самой известной стороны и окажется интересен широкому кругу читателей.

Множества и классы

Алгоритмы и переменные

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

Более четырёх тысяч лет назад в древнем Междуречье люди умели вычислять объёмы крепостных стен, площади земельных участков, динамику численности стад и проч. Тогда на примере конкретных житейских проблем были описаны способы вычисления, которые применимы для широкого спектра задач, достаточно лишь заменить числа в условии. Но лишь в средние века в Европе в обиход вошло понятие «алгоритм», для которого необходимо использование новой абстракции - переменной.

Вавилонская табличка Plimpton 322 (~4000 лет), в которой собраны пифагоровы тройки — размеры прямоугольных треугольников, у которых оба катета и гипотенуза выражаются целыми числами.

Термин "переменная" вовсе не означает, что связанное с ней значение будет меняться по ходу выполнения алгоритма, но значение будет разным для разных начальных условий. Обычно, наоборот, подразумевается, что в течении решения задачи переменная остаётся неизменяемой. Если же какое-либо значение окажется фиксированным для всего класса задач, то такое значение принято называть константой алгоритма.

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

Свойства таких наборов-множеств, их взаимоотношений исследуются веками. Во второй половине XIX века созрело понимание, что теория множеств может дать фундамент для всех секторов математики, которые развиваются зачастую независимо друг от друга узкими специалистами.

Множества

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

Обычно говорят принадлежности к множеству какого-либо элемента: $a\in A$ . Задать множество можно двумя способами:

интенсионально - указав условие, по которому можно выбрать некоторые элементы существующего множества - $\{$ множество всех читателей этой статьи $\}$ ;
экстенсионально - просто перечислив его элементы - $\{a, b, c\}$ .

Интенсионально, через условие, определяются основные операции над множествами, которые позволяют конструировать новые множества.

Бинарные операции над множествами: пересечение, объединение и разность.

Также полезными оказываются выделенные пустое $\emptyset$ и универсальное (вселенское) $\mathcal{U}$ множества, такие, что для любого утверждения $a\in\emptyset$ ложно, а $a\in\mathcal{U}$ истинно.

Также важно понятие отношения между множествами, в частности, равенство множеств.

Отношения между множествами - вложение и равенство.

На Хабре можно также подсмотреть красочное Введение в теорию множеств.

Неразличимость и вычисления

Множества характеризуют переменные, а следовательно, и алгоритмы, описывающие отношения между переменными (прежде всего, начальными значениями и результатом). Отношения между множествами принято классифицировать так:

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

Например, житейский пример: мы не сможем отличить множество коров от множества яблок, если и яблоки и коровы не только выглядят, но даже пишутся одинаково))). А если не одинаково, значит у нас есть дополнительная структура над множествами - операция отношения, которая позволяет сравнить корову с яблоком. В компьютере восьми-байтовая ячейка памяти может хранить в себе значения как из множества Int64, так и из double - эти множества имеют одинаковую мощность, но различаются они разным набор возможностей (например, для double есть тригонометрические и другие функции, а для Int64 - деление с остатком). Но давайте рассмотрим ещё один

Пример из программирования

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

Для такого класса задач нам требуется дополнительная структура над множествами - набор функций позволяющий "уменьшать количество" элементов списка вплоть до единственного. Такая структура называется "моноид". Абстрактный моноид обычно описывается так:

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

Моноид - это множество M, ассоциативная бинарная операция на нём и нейтральный элемент из него.

На практике для построения алгоритмов с использованием того же моноида "лишним" в его определении оказывается... множество! В самом деле, если есть возможности моноида (бинарная операция и нейтральный элемент) инструкции не меняются, если в качестве множества мы выбираем int, double или string - описание алгоритма остаётся тем же (но потребуются другие реализации моноида). Фактически, множество выступает всего лишь как некий ярлык - связующее звено для композиции различных возможностей (моноида и прочих). Так на переднем плане появляется концепция типа.

upd. Alexander @speshuric в Комментариях заметил, что рассуждать о мощности множества значений типа double может быть затруднительно, так как в некоторых спецификациях значения NaN оказываются не равными себе - связанные с типом отношения эквивалентности могут не позволит классифицировать некоторые значения.

Типы - основные понятия

Определение типа

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

Тип - это метка терма, позволяющая описать процесс вычисления, указав связи-функции (i₁, i₂, p₁, p₂) с другими такими метками.

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

указать совокупность "входящих" отображений (также говорят "инъекторы" или "конструкторы");
указать совокупность "исходящих" отображений (также говорят "проекторы").

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

На картинке выше видно, что

если у нас есть объект типа , или , то мы можем считать, что у нас есть (мы всегда можем получить) и объект типа .
с другой стороны, если у нас есть объект типа , то у нас есть (мы можем получить) объекты типов и .

Можем ли мы определить тип , как " или "? Или как " и "? Формально, мы можем всё, мы ж программисты!!

Но к сожалению, такого рода утверждения не будут считаться полными и однозначными определениями. В нашем случае, мы должны ещё гарантировать, что нет никаких , и прочих, кто ещё связан отображениями с . Но с другой стороны, например, если для есть отображение в , то вполне можно исключить из определения типа . Аналогично, среди типов также могут найтись те, кто связан с отображениями, значит там тоже кого-то можно исключить из формулировки через произведения. Нам нужно выбрать "наилучшего" универсального представителя - нам нужно некое универсальное свойство.

Универсальное свойство и композиция функций

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

Универсальное свойство в теории типов можно определить как-то так:

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

Звучит, пожалуй, сложновато)). Наверное, на начальном этапе универсальное свойство стоит воспринимать просто как некий способ однозначного формулирования различных абстракций в теории типов. Но стоит сказать пару слов про "коммутативность".

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

Коммутативная диаграмма композиции функций.

Здесь $g \circ f$ - это композиция функций и :

def f(a: A): B = ???                // какая-то функция
def g(b: B): C = ???                // какая-то функция
assert((g compose f)(a) == g(f(a))) // для любого a: A

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

Самым важным в понятии универсального свойства является именно единственность универсальной функции. Формулирование типов через универсальные свойства (уникальные кратчайшие пути) помогает декомпозировать сложные вычисления на простые шаги и описать их с помощью типов. Понятие коммутативности путей позволяет различать классы аналогичных способов вычисления и искать наилучшие (оптимальные) в каждом таком классе.

К этому моменту ни у кого уже не должно остаться сомнений, что функции - это душа теории типов, а теория типов - основа ~~функционального~~всего программирования!

Сумма типов

Вооружившись понятием универсального свойства, попробуем определить новый тип как " или ". В математике это обычно называют суммой типов. На диаграмме ниже представлено универсальное свойство для типа-суммы:

Для любых типа и функций и существует единственный (с точностью до изоморфизма) тип и единственная функция , делающие диаграмму коммутативной. Здесь и - это два разных конструктора (инъектора) типа из значений типов и . Рассмотрим конкретные примеры сумм типов в языке программирования Scala.

Обязательный тип-сумма, который присутствует в каждом языке программирования - булевский тип, у которого может быть только два разных значения - true или false:

  type Two = Boolean                  // True + False

Кроме того, в парадигме ООП сумма типов обычно определяется через наследование - класс-родитель является суммой своих прямых наследников. Чтобы однозначно определять тип-родитель как конечную сумму типов-наследников, зачастую его можно "запечатать" - в Scala для этих целей используется модификатор sealed:

  sealed trait Type2       // One + Two
  object One extends Type2 
  object Two extends Type2

Типы перечисления в Scala 3 под капотом реализуются аналогично через подтипы-"наследники":

  enum Type3 { case One, Two, Three } // One + Two + Three

Также в библиотеке Scala есть стандартный обобщённый тип Either (и другие), реализующий семантику суммы типов:

  type IntOrInt = Int Either Int  // Int + Int

Но в обобщённые типы мы постараемся не углубляться, дабы не выходить за рамки и без того богатой темы этой публикации.

В Scala 3 также появилось понятие типа-объединения:

  type IntOrString = Int | String     // Integer + String

На самом деле, объединение типов в общем случае - это не то же самое, что их сумма. Например, Int | Int будет точно тоже самое, что и просто Int - такое объединение не позволяет получить сумму двух одинаковых типов, как это было в случае IntOrInt в примере выше. Дело в том, что значения суммы типов Int Either Int "помнят", каким из двух конструкторов ("левым" или "правым") они были построены, что позволяет различить эти ситуации при сопоставлении с шаблонами. В то же время тип-объединение таких мелочей не запоминает. У него есть свои особенности, но их можно считать надстройкой над теорией типов, поэтому здесь они не будут описаны.

На диаграмме универсального свойства видно, что у типа суммы есть несколько конструкторов - несколько параллельных путей получения значения этого типа. Соответственно, чтобы получить из этого типа значения другого типа потребуется учесть все эти ветви. Суммы типов нужны как раз для реализации семантики ветвления алгоритмов. Помимо стандартной языковой конструкций if более общим паттерном в программировании является сопоставление с шаблонами (pattern mathing), как, например, в этом методе choose:

  def choose(variant: Boolean | Int | String): String =
    variant match
      case b: Boolean => "булево значение " + b
      case i: Int     => "целое число " + i
      case s: String  => "строка " + s
      // тип оперделяет выбор ровно из трёх альтернатив!

Подробнее о связи тип сумм с ветвлением алгоритмов будет рассказано в главе про изоморфизмы типов.

Произведение типов

Если на диаграмме универсального свойства для типа суммы мы развернём все стрелки в обратном направлении, то получим универсальное свойство типа-произведения, соответствующего семантике высказывания и :

Диаграмма универсального свойства произведения типов.

Для любых типа и функций и существует единственный (с точностью до изоморфизма) тип $A\times B$ и единственная функция , делающие диаграмму коммутативной. Здесь и - это два проектора типа $A\times B$ на типы и . Рассмотрим конкретные примеры произведения типов в языке программирования Scala.

Прежде всего, это привычные ООП-шные классы (а также трейты, интерфейсы, структуры, записи, объекты или что ещё есть в вашем любимом языке программирования?)):

  case class BoolAndDouble(b: Boolean, d: Double) // Boolean × Double

Поля и свойства класса - это и есть те самые проекции типа-произведения. Методы класса также можно считать проекциями значений функционального типа (этот тип мы рассмотрим позже).

Наиболее выразительно тип произведения определяется в Scala c помощью кортежей:

  type IntStrBool = (Int, String, Boolean) // Int × String × Boolean
  val isb: IntStrBool = (5, "4", false)
  assert(isb._2 == "4") // проекция _2
  val (_, _, b) = isb   // деконструкция через сопоставление с шаблоном
  assert(b == false)

В Scala 3 также появилось понятие типа-пересечения:

  type StringAndLong = String & Long // String × Long

Но тут есть аналогичная проблема, как и с объединением типов. Например, Int & Int будет точно тоже самое, что и просто Int - такое пересечение не позволяет получить произведение двух одинаковых типов, чего вполне можно достичь с помощью тех же кортежей. Кроме того, тип StringAndLong демонстрирует ещё одну особенность пересечения типов в Scala - можно объявить пересечение типов, заблокированных для расширения (sealed или final), но вот создать экземпляр такого типа не получится! Дело в том, что тип String & Long является подтипом и для String, и для Long, а такая подтипизация реализуется в Scala только через ООП-шное наследование от обоих типов. Но эти типы закрыты для расширения, так что String & Long оказывается необитаемым!

Симметричность с точностью до инверсии всех стрелок универсальных свойств суммы и произведения типов является фундаментальной особенностью теории ~~категорий~~типов. Если мы формулируем какое-то универсальное свойство, то мы автоматически получаем и дуальное ему. Дуальность в теории типов следует из возможности декомпозиции вычислений на шаги, выполняемые последовательно во времени - имея такую последовательность, её можно (формально) развернуть в обратную сторону. Инвертированные шаги не всегда может получится реализовать, но общие утверждения об исходном алгоритме будут справедливы и для дуального (опять же с точностью до направления рассуждений). Таким образом, дуальность можно обосновать существованием стрелы времени как таковой!

Экспоненциал типов

Рассмотрим сумму двух одинаковых типов . Это значит, что у нас есть два конструктора типа из типа . Сумма типов устроена так, что её значения "помнят", каким конструктором они были созданы - это необходимо, чтобы из типа суммы получить значения какого-либо другого типа, если мы знаем, как их получить из значений типов-слагаемых (сопоставление с шаблонами). Фактически это значит, что для типа у нас есть не только проекция обратно в , но в некий индексирующий тип, значения которого определяют выбор того или иного конструктора.

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

Тип B является суммой A и A, но его также можно считать произведением A и 2.

Здесь и - два конструктора типа , а - это тот самый индексирующий тип, у которого в нашем случае есть только два возможных значения. Получается, что тип , представленный на диаграмме, можно определить двумя разными способами - и как сумму и как произведение $A\times2$ !

Тут стоит обратить внимание на следующую идею: значения нашего индексирующего типа ставятся в соответствие функциям из в . Так может быть эти функции также являются значениями какого-то типа?..

Но сперва давайте рассмотрим те же самые типы, но с другой точки зрения. Переобозначим конструкторы типа и в проекторы типа и , получая $A=B\times B$ . Имея значение типа мы можем получить значение типа , только если мы выберем один доступных проекторов, т.е. на момент вычисления у нас на руках должно быть, помимо значения типа , ещё одно значение - предпочтённый индекс проектора! Такая пара значений относится к типу $A\times2$ , где - тип, индексирующий проекторы . Тогда имея значение типа $A\times2$ у нас будет возможность вычислить значение типа :

Те же яйца, вид сбоку: конструкторы превратились в проекторы, и мы теперь рассматриваем A = B × B.

Здесь eval - так называемая "функция оценки" (англ. evaluate). Эти соотношения справедливы для любого количества проекторов.

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

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

Экспоненциал имеет очень простую трактовку - это тип функций из значений типа в тип . Пара значений типа $B^C\times C$ - это всё, что необходимо для вычисления значения типа .

Функции, как значения некоторого типа ("первоклассные функции"), есть в том или ином виде практически во всех популярных языках программирования: "указатели на функцию" в С++, "делегаты" в C# и т.п. В Scala для типа функций обычно используются конструкции такого вида:

  val toStr                     // переменная для значение функцонального типа
    : Int => String             // тип функции - из целого числа в строку
    = i   => "#"                // λ-выражение - значение функцонального типа
    
  def toStringDoubled(          // ещё один бестолковый метод
    i: Int,                     // принимает целочисленное значение
    intToString: Int => String  //         и значение-функцию!
  ): String =
    val str = intToString(i);   // используем значение-функцию
    s"($str, $str)"             // возвращение значения

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

Выше приведён пример использования $\lambda$ -выражения, которое является литералом значения функционального типа. Они так же присутствуют в большинстве языков программирования. Помимо $\lambda$ -выражения, для получений значения функционального типа многие языки позволяют (неявно) использовать ссылки на какой-то метод:

  def doubleDouble(i: Int): Double = i * 2.0
  val intToDouble: Int => Double = doubleDouble // ссылка на метод

Методы, принимающие несколько аргументов, соответствуют функциям, принимающим значения типа-произведения. Например, метод toStringDoubled из примера выше можно представить как такую функцию, принимающую кортеж из двух значений:

  // Int × (Int => String) => String
  val toStringDoubledFunc
    : (Int, Int => String) => String
    = toStringDoubled

Существует также дуальное эксопненциалу понятие ко-экспоненциала типов . Это понятие весьма нетривиально, но если игнорировать особенности, связанные с нулевыми типами (про них будет далее), то можно согласиться на такой изоморфизм: $A_B\cong B^A$ . Это вполне соответствует ожиданию, что для получения дуальной диаграммы необходимо развернуть все стрелки, представляющие функции-значения экспоненциального типа. Утрировано, тип функции дуален самому себе.

Типы суммы и произведения естественно следуют из самой концепции типа, буквально, определяются входящими и исходящими стрелками соответственно. В то же время, на их фоне экспоненциал выглядит несколько искусственно. Могут возникнуть вопросы, например, есть ли более фундаментальные конструкции, для которых экспоненциал будет лишь частным случаем? На самом деле, есть глубокая связь экспоненциала с суммой и произведением, делающая эту тройку фундаментом для простой теории типов. К сожалению, не удалось найти способа продемонстрировать это в данной статье без привлечения других интересных понятий из теории категорий. Так что "ждите в следующих сериях"!))

На Хабре можно почитать классную статью Теория категорий на JavaScript. Часть 1. Категория множеств. Там много красивых картинок с детальным разбором универсальных свойств сумм, произведений и других понятий, использующихся в теории типов. К сожалению, продолжения этой статьи найти не удалось...

Подтипизация и наследование

В программировании широко известно такое понятие как "подтипизация" - основа ключевой для ООП разновидности полиморфизма - полиморфизма подтипов. Подтипизация - это такое отношение порядка между типами, что если является подтипом для (пишут , "под типом" ), тогда любой терм типа можно безопасно использовать в любом контексте, где ожидается терм типа . "Безопасное использование" и "контекст" могут трактоваться по разному в разных языках программирования.

В ООП есть схожее понятие, которое иногда путают с подтипизацией - "наследование". Наследование - это способ описать реализацию нового типа на основе реализации существующих типов, в то время, как подтипизация - это только отношение между типами. Подтип не всегда является наследником супертипа. Например Int32 вполне можно считать подтипом для Int64, но ни о каком наследовании тут нет речи. Наследование выстраивает типы в иерархическую структуру, но подтипизация в этом плане гораздо гибче.

Иногда говорят, что терм какого-то типа является также и термом всех супертипов этого типа, т.е. с термом ассоциирован не один тип, а сразу несколько. С такой точки зрения строятся различные интересные ответвления теории типов, но на данную ситуацию можно посмотреть и проще. Ведь по сути, мы имеем дело с наличием неявного преобразования значений от подтипа к супертипу.
Можно сказать, что отношение подтипизации - это просто функция!

Иерархия типов Scala с официального сайта. Все стрелки здесь - неявные функции приведения типов.

В Scala, помимо ООП-шного наследования ("расширения" или "реализации"), есть как встроенные неявные преобразования типов, так и возможность определять свои:

given Conversion[Int Either Int, (Boolean, Int)] = // Int + Int => 2 × Int
  case Left (i) => (false, i)
  case Right(i) => (true,  i)

val intOrInt: Int Either Int = Right(42)           // тип Int + Int
val int2    : (Boolean, Int) = intOrInt            // (true, 42)

Алгебра типов

Изоморфизм

В предыдущем разделе на первой диаграмме показан тип , который можно было представить и как и как $A\times2$ . Эти представления не эквиваленты - они предоставляют разные способы работы со значениями этих типов. Но между множествами их значений можно построить взаимно-однозначное соответствие, биекцию, определяемую парой функций, действующих в противоположных направлениях:

  type Int2     = (Int, Boolean)  // Int × 2
  type IntOrInt = Int Either Int  // Int + Int

  def туда(i2: Int2): IntOrInt =
    i2 match
      case (i, true)  => Right(i) // конструктор правого слагаемого
      case (i, false) => Left (i) // конструктор левого  слагаемого
      
  def обратно(ii: IntOrInt): Int2 =
    ii match
      case Right(i) => (i, true)  // правое слагаемое
      case Left(i)  => (i, false) // левое  слагаемое
  
  assert((обратно compose туда)(i2) == i2) // для любых i2
  assert((туда compose обратно)(ii) == ii) // для любых ii

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

Используя обозначение $\cong$ мы можем записать изоморфизм из примера выше так:

$A+A\cong A\times2,$

где - это тип с двумя значениями, Boolean.

Аналогично, для изоморфизма

$A\times A\cong A^2$

можно предоставить такие методы:

  type IntInt = (Int, Int)                 // Int × Int
  type BoolToInt = Boolean => Int          // 2 => Int

  def туда(ii: IntInt): BoolToInt =
    (b: Boolean) =>                        // функция из Boolean
      if (b)  ii._1                        // первый элемент кортежа
      else    ii._2                        // второй элемент кортежа

  def обратно(i2: BoolToInt): IntInt = (   // кортеж из двух элементов
    i2(true),                              // первый элемент кортежа
    i2(false),                             // второй элемент кортежа
  )
  
  assert((обратно compose туда)(ii) == ii)     // для любых ii
  assert((туда compose обратно)(f)(b) == f(b)) // для любых f и b

Старая добрая школьная алгебра, не так ли? Более того, суммы и произведения типов удовлетворят (с точностью до изоморфизма) основным алгебраическим законам:

коммутативность: $A+B\cong B+A,\;A\times B\cong B\times A$ ;
ассоциативность: $A+(B+C)\cong(A+B)+C,\;A\times(B\times C)\cong(A\times B)\times C;$
дистрибутивность: $A\times(B+C)\cong A\times B+A\times C.$

Уверен, читателю не составит труда доказать эти изоморфизмы самостоятельно, предоставив соответствующие функции, как в примерах выше.

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

Для экспоненциала также можно записать знакомые со школы соотношения. Но зачастую для них в языках программирования предоставляются специальные механизмы. Рассмотрим их подробнее.

Сопоставление с шаблонами

Тип суммы определяется своими конструкторами - способами получения значения этого типа. Но гораздо важнее то, как можно использовать значения этого типа, например, как из них можно получить значения другого типа. Общие соображения подсказывают нам, что для того чтобы преобразовать значения типа суммы в другой тип, нужно предоставить соответствующие преобразования в этот тип из значений типов-слагаемых. Алгебраические соотношения говорят нам то же самое:

$A^{B+C+D}\cong A^B\times A^C\times A^D.$

То есть, функцию из в можно построить, если у нас есть все три функции в из , и . Для этих целей и предназначен упомянутый ранее механизм сопоставления с шаблонами:

  val patternMatching         // Int + Boolean + Double => String
    : Int | Boolean | Double => String =
      case i: Int     => "целое "        + i // Int     => String
      case b: Boolean => "булево "       + b // Boolean => String
      case d: Double  => "рациональное " + d // Double  => String

Компилятор сам отслеживает, чтобы при сопоставлении с шаблонами были учтены все альтернативы - все слагаемые типа-суммы, и чтобы у каждой ветки был обработчик-функция соответствующего типа.

Для встроенных (и многих сторонних) типов-сумм в Scala предоставляются специальные методы, дающие те же возможности, но без необходимости использовать синтаксический сахар:

  val getStr
    : Int Either Double => String   // Int + Double => String
    = intOrDouble       =>          // λ-выражение
      intOrDouble.fold(             // "свертка" суммы типов
        i => "целое "        + i,   // Int          => String
        d => "рациональное " + d)   // Double       => String

В литературе о программировании можно встретить термин алгебраические типы данных (algebraic data types, ADT). Этот загадочный термин не несёт какой-либо мистики - просто так обозначают типы, представимые в виде конечных сумм других типов. В языках программирования для ADT реализуются некоторые алгебраические изоморфизмы и основанные на них механизмы компилятора, наиболее важным из которых является именно сопоставление с шаблонами.

Каррирование

Чтобы вычислить некоторое выражение, зависящее от переменных, нужно "связать" эти переменные с выражением - построить вокруг этого выражения функцию и передать в неё эти переменные как параметры. Однако сделать это можно несколькими способами:

  val f1
    : (Int, Boolean) => String
    = (i,   b)       => if ((i > 0) && b) "тру!" else "дырка!"

  val f2
    : Int => (Boolean => String)  // скобки лишние ("правая ассоциативность")
    = i   =>  b       => if ((i > 0) && b) "тру!" else "дырка!"

  f1(-2, false) // "тру!"
  f2(-2)(false) // "тру!"

Функция f2 принимает один аргумент, но возвращает функцию-замыкание, принимающую второй аргумент и "захватывающую" в своё тело аргумент из f2.

Обе функции из примера выше основаны на одном выражении if ((i > 0) && b) "тру!" else "дырка!" и отличаются друг от друга только способом связывания переменных в выражении и своими типами. Не сложно догадаться, что эти типы также связаны изоморфизмом. Соответствующие функции преобразования от одного типа к другому очевидны, и они уже есть в Scala - это метод curried (в Scala тип функции является ООП-классом, и имеет свои методы) и функция Function.uncurried:

  import Function.uncurried
  assert(f1.curried   (i)(b) == f2(i)(b)) // для любых i, b
  assert(uncurried(f2)(i, b) == f1(i, b)) // для любых i, b

Ниже приведён немного искусственный пример использования метода curried:

  // Int × (Int => Int) => Int
  def doubleModification(i: Int, modifier: Int => Int): Int =
    modifier(modifier(i))

  val sum
    : (Int, Int) => Int
    = (a, b) => a + b
  sum(2, 2)                    // 2 + 2 = 4
  
  val sumCarried = sum.carried // Int => Int => Int
  sumCarried(3)(3)             // 3 + 3 = 6
  
  
  val add5 = sumCarried(5)    // Int => Int     (a => a + 5)
  doubleModification(2, add5)  // 2 + 5 + 5 = 12

У нас есть функция, doubleModification, которая принимает целое число, некоторую функцию-модификатор, и применяет эту функцию к целому числу дважды. И так же есть функция от двух целых чисел, просто складывающая их. Для двойного прибавления к некому числу (например, 2) заданного числа (например, 5) можно сперва построить каррированную версию функции сложения, и применить её к прибавляемому числу (5). Так мы получим функцию, принимающую только один аргумент - оставшееся слагаемое. И эту функцию мы можем смело передавать в doubleModification.

Ключевой момент здесь - чтобы скомбинировать сложение с doubleModification нам не нужно описывать новую функцию вручную - мы просто (явно, с помощью curried) получаем значение sumCarried изоморфного функционального типа и вычислем add5, которую уже можно передать в doubleModification.

Из примеров выше видно, что в Scala и вызов, и определение функции и её каррированной версии отличаются лишь синтаксисом. В некоторых языках программирования (ML-семейство - Haskell, F# и т.п.) функции считаютcя каррированными по умолчанию. Например, в F#:

let sum a b = a + b // = функция Int => Int => Int
let four = sum 2 2  // = 4
let add2 = sum 2    // = функция Int => Int
let five = add2 3   // = 5

Не зависимо от того, как вашем любимом языке программирования обрабатывается каррирование, само по себе оно является следствием "школьного" алгебраического изоморфизма типов:

$A^{B\times C}\cong \left(A^B\right)^C.$

Единица

Иногда возникает необходимость в "забывающих" функциях, отображающих значения некого типа в тип, который даже не помнит, каким путём были получены его значения. Значение этого типа отражает лишь сам факт существования чего-то, что мы можем передать на вход другой функции. Для любого типа есть только одна возможность, чтобы забыться - это функция которая просто игнорирует свой аргумент и возвращает единственное значение "типа-существования". Такой тип-одиночка называется единицей , а единственность способа получения его значения из других типов - это его универсальное свойство:

Универсальное свойство единицы: для любого A существует единственный u.

Такой "забывчивый" тип часто встречается в программировании. Но в некоторых языках программирования он доступен не как самостоятельный тип, а как некая синтаксическая конструкция. Например, процедура, которая не возвращает (осмысленного) значения часто обозначается ключевым словом void. Эта "пустота", получающаяся после вызова процедуры, на самом деле не является совсем уж "ничем" - у нас по прежнему существует возможность продолжать вычисления. Процедуры аналогичны функциям, возвращающим значение типа-единицы. Такие процедуры-функции обычно описывают какие-то "эффекты", вроде вывода строки в на экран, но эффекты - тема для отдельной статьи. В случае же отсутствия эффектов, разные реализации таких забывающих функций оказываются эквиваленты, следовательно, типы этих функций являются типами-одиночками, что соответствует известному алгебраическому тождеству:

$1^A\cong1$

- универсальное свойство единицы.

С другой стороны, когда мы вызываем функцию без параметров, мы в любом случае передаём ей саму возможность производить вычисления. Функции без параметров - это отображения из типа единицы. Во многих языках программирования при вызове таких функций необходимо указать пустые круглые скобки. В Scala такая конструкция считается литералом типа Unit - той самой единицы:

  val unitId
    : Unit => Unit         // функция из единицы в единицу
    = u    => ()           // "забываем" единицу))

  assert(unitId(()) == ()) // "незабвенная" единица))

Несложно заметить, что типы таких функций изоморфны типам, которые они возвращают - между ними также можно построить знакомый изоморфизм:

$A^1\cong A.$

Не раз ощущал нехватку такого встроенного изоморфизма. Его наличие могло бы упростить некотрые композиции вычислений. Но его всегда можно добавить вручную.

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

None - подтип Option[A], определяющий факт отсутствия значения типа A.
Nil - подтип List[A], означающий пустой список. Так как они являются подтипами, для них заданы функции неявного преобразования к своим супер-типам. Эти функции определяют их семантическое различие, но очевидно, что они остаются изоморфными Unit.

Из этих примеров видно, что типы-одиночки часто используются в качестве слагаемых для типов сумм. Например тот же тип Option можно представить, как

$Option[A]=A+None\cong A+1,$

где $None\cong1$ - тип-одиночка.

С другой стороны, когда тип-единица выступает в качестве "множителя" для некого типа-произведения, он не привносит новой информации, и всегда можно предоставить такой изоморфизм:

  def туда(a: A): (A, Unit) = (a, ())
  def обратно(pair: (A, Unit)): A = pair._1

  assert((обратно compose туда)(a) == a)              // для любых a
  assert((туда compose обратно)((a, ())) == (a, ()))  // для любых a

Этот изоморфизм представляет собой обычный алгебраический закон для произведения:

$A\times1\cong A.$

(Такого встроенного изоморфизма также иногда очень не хватает в Scala).

В документации Scala сказано, что супертипом для всех типов языка является Any. Однако, универсальный морфизм для Unit встроен в язык как неявное преобразование из любого типа. Так что, следуя написанному ранее определению подтипизации, Unit, будучи подтипом AnyVal и Any, в то же время является супертипом для всех остальных типов, в том числе и для Any:

  val any: Any = new {}
  val unit: Unit = any      // неявное преобразование из Any в Unit

Впрочем, компилятор Scala будет выдавать предупреждения при использовании неявных преобразованиях к Unit, считая, что, скорее всего, вы делаете что-то не то. Наличие неявных преобразований от Any к Unit и обратно ("зацикливание" подтипизации) не образует изоморфизм, так как применение их композиции к значению типа Any в общем случае не вернёт значение, равное ему же. Дело в том, что значения типа Any "помнят", каким путём они были получены, и их можно использовать, например, в сопоставлениях с шаблонами, но Unit не является суммой типов - его единственное значение не знает ничего, кроме факта своего существования.

В программировании есть также понятие null - "пустая ссылка". В большинстве языков программирования литерал null не ассоциирован ни с каким типом, но в Scala у него есть собственный тип Null. Из-за названия его иногда путают с нулевым типом, описанным в следующем разделе. Тем не менее, значение null соответствует отсутствию значения ссылочного типа A, примерно так же, как это было с типом None, упомянутым выше, следовательно, он ближе именно к единичному типу, а не к нулевому! Впрочем, сам автор называет null "ошибкой на миллиард", так что и мы не будем больше его упоминать))).

Ноль

Немного реже, чем "забывание" типа, бывает полезным описать полное прекращение вычисления, без получения какого-либо значения вообще. Это может быть бесконечный цикл/рекурсия, или возникновение исключения. Чтобы продемонстрировать, что функция вообще не завершается, можно прописать, что она отображает некий тип в другой, у которого не может быть значений по определению! Обозначим этот тип как .

Для нулевого типа существуют очевидные изоморфизмы:

$A+0\cong A,$ $A\times0\cong 0,$ $A^0\cong1.$

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

Универсальное свойство ноля: для любого A существует единственный u.

С типами функций, ведущими к нулю, ситуация сложнее. Функция из ноля в ноль существует и единственна (тождественная функция): . Но если $A\ncong0$ , то, согласно конструктивной теории типов, $0^A\cong0$ - невозможно сконструировать значение типа , следовательно, и функцию в этот тип. Вот только честно реализовать конструктивную логику в программировании крайне сложно, поэтому тут допускаются и бесконечные вычисления, и исключения, которые так или иначе не возвращают результата. Неформально это можно трактовать так: у нас есть разные способы "подвесить" или вообще прервать вычисление.

Во многих популярных языках программирования нет нулевого типа. В Scala же он есть - Nothing. Универсальное свойство этого типа реализуется тут как наличие неявного преобразования его "значения" к любому другому типу - Nothing является подтипом всех типов! Также есть встроенная функция, которая определяется примерно так:

val ???                     // вполне допустимый идентификатор Scala
  : Unit => Nothing         // из единицы в ноль
  = u    => throw Exception // никогда не вернёт значение

// использование, через неявное преобразование:
val a: A = ???              // заглушка - скомпилируется, но не выполнится

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

В Scala и многих других языках программирования автоматически реализуется изоморфизм $A\cong A+0$ - каждая функция, которая должна возвращать значения некого типа, может бросить исключение, или просто "зависнуть". Такая особенность не то, чтобы помогает типобезопасности - за возможностью "невозврата" значения приходится следить самому программисту.

Универсальное свойство нулевого типа часто сочетается с ковариантностью обобщённых типов. Например, с его помощью реализованы упомянутые выше типы-одиночки None и Nil. Но в этой статье мы не будем рассказывать об обобщённых типах.

Для типа-ноля можно самому построить изоморфные ему типы, для которых также невозможно получить экземпляр. Такие типы называются фантомными. Они используются, например, для того, чтобы отличать одни типы от других - несмотря на изоморфность друг другу, важным оказывается их неэквивалентность:

// Для этих типов нет конструкторов - их значения невозможно получить
final class NameTag    private {}        // NameTag    ≅ 0
final class AddressTag private {}        // AddressTag ≅ 0
//val nameTag = new NameTag              // Ошибка! Невозможно создать

type UserName    = String | NameTag      // UserName    ≅ String
type UserAddress = String | AddressTag   // UserAddress ≅ String
// типы изоморфны UserName ≅ UserAddress, но
// неэквивалентны UserName ≠ UserAddress  !!!

val userName: UserName = "sdfds";
//val userAddress: UserAddress = userName; // Ошибка! Типы неэквивалентны

В качестве дополнительного чтения по алгебре типов можно порекомендовать статью Простые алгебраические типы данных - перевод одной главы из книги Category Theory for Programmers от Бартоша Милевски. В его блоге вообще много отличных статей, часть из которых и составили ту книгу. Но, зачастую, там высокий порог вхождения, в то время как предложенный перевод на Хабре достаточно дружелюбен к читателю.

Типы и множества

Тип множеств

Что представляет собой множество с точки зрения теории типов? Можно считать, что множество определяется интенсионально, через возможность проверки принадлежности ему любого объекта:

val contains: (Set, Any) => Boolean

Если эту функцию переписать в каррированном в виде, то получится что-то вроде ООП-представления - множество предоставляет метод проверки принадлежности ему некоторого объекта:

val setChecker: Set => Any => Boolean
val mySetChecker = setChecker(mySet)
mySetChecker(value) // true/false

Ввиду единственности метода, определяющего семантику множества, его тип оказывается изоморфен типу функции из Any в классификатор Boolean:

type Set = Any => Boolean

Из структуры типа-классификатора, следуют два выделенных множества, а также нам потребуется способ создавать одноэлементное множество:

val emptySet      : Set =      x => false  // никто не принадлежит множеству
val universalSet  : Set =      x => true   // любой    принадлежит множеству
val makeSet: Any => Set = a => x => a == x // создать одноэлементное множество

Операции, порождающие другие множества из существующих, определяются через возможности типа Boolean:

val union
  : (Set, Set) => Set
  = (a, b)     => x => a(x) || b(x)
val intersection
  : (Set, Set) => Set
  = (a, b)     => x => a(x) && b(x)
val difference
  : (Set, Set) => Set
  = (a, b)     => x => a(x) && !b(x)

В Scala уже есть встроенный тип Set с различными реализациями, но ключевая семантика множества, как функции-классификатора (true/false) значений там точно такая же. Таким образом, множество - это функция!

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

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

Типы и классы

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

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

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

Рассмотрим пример, как можно от ООП-шных классов перейти к суммам, произведениям, экспоненциалам типов (на реализацию не отвлекаемся).

// есть классы
object classes:
  sealed trait PredictionCalculator:
    def calculate(conditions: Conditions): Estimation
    
  final case class PessimisticPredictor(fallback: SoapAndRope) extends PredictionCalculator:
    def calculate(conditions: Conditions) = ???  

  final case class OptimisticPredictor(continuation: Cocktail) extends PredictionCalculator:
    def calculate(conditions: Conditions) = ???  

// нет классов, только экспоненциал, пара произведений и сумма типов
object classless:
  type PredictionCalcFunction = Conditions => Estimation
  type PessimisticPredictor   = (RopeAndSoap, PredictionCalcFunction)
  type OptimisticPredictor    = (Cocktail,    PredictionCalcFunction)
  type PredictionCalculator   = PessimisticPredictor | OptimisticPredictor

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

Подтипизация и множество значений

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

Иногда предпринимаются попытки ограничить подтипизацию, например, путём "запечатывания" класса, запрещающего произвольное наследование. Запечатанные (sealed) классы можно наследовать (расширять) только внутри определённого блока - пакета, файла, модуля, в зависимости от языка. Через запечатанные классы в ООП реализуются алгебраические типы - запечатанный трейт в Scala представляется в виде конечной суммы реализующих его классов/объектов, описанных в том же файле, что и сам трейт. Благодаря запечатыванию обеспечивается, что больше никто не сможет добавить слагаемых в этот тип-сумму и при сопоставлении с шаблонами компилятор сможет проверить, что мы обработали все слагаемые типа-суммы:

sealed trait StringOrNone // запечатанный трейт, изоморфный String + 1
case class  MyString(val: String) extends StringOrNone // ≅ String
case object MyNone                extends StringOrNone // ≅ 1

val request: StringOrNone = MyString("ты чё?")
val response = requset match
  case MyString(req) => "ничё. а " + req
  case MyNone        => "ничё"
  // больше наследников нет, значит нет и других вариантов!

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

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

Типы и мощности их множеств

Интересно проследить, как операции с типами отражаются на мощностях соответствующих им множеств. Для мощности типа используем обозначение $\|A\|$ .

С типами и всё очевидно - мощности их множеств отражены в названии:

$\|0\|=0,\;\|1\|=1.$

Рассмотрим покомпонентно сумму типов:

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

Рассмотрим теперь произведение типов. Для простоты представим произведение как многократную сумму:

Внутренняя структура произведения типов. Если ||A||=3 и ||B||=2 то ||A×B||=6.

Здесь - это просто обозначение элемента типа $A\times B$ . Очевидно что для произведения выполняется соотношение, аналогичное сумме типов:

$\|A\times B\|=\|A\|\times\|B\|.$

При рассмотрении типа-экспоненциала , достаточно вспомнить что каждый его объект, функция, в теории множеств представляет собой набор пар значений типа и , причём в этом наборе присутствуют все элементы типа в единственном количестве. Чтобы вычислить все возможные значения этого типа достаточно перебрать все различающиеся наборы пар:

Внутренняя структура экспоненциала типов. Если ||A||=3 и ||B||=2 то ||Bᴬ||=8.

Получается, что вычисление мощности типа сохраняет также и экспоненту:

$\|B^A\|=\|B\|^{\|A\|}\;\;\;(B\ncong0).$

Удивительный результат, не правда ли?

В статье Понять TypeScript c помощью теории множеств представлена попытка трактовать типы, как множества их значений. Там предлагается по иному воспринимать некоторые термины, как, например "расширение" (extends), чем это могло бы быть в теории множеств. Простые типы в языках программирования, конечно, можно попробовать ассоциировать с множествами значений, но для работы с типами используется другой набор терминов, обусловленный иным предназначением, чем у множеств.

Типы и корректность алгоритмов

Время, чистые функции и неизменяемые значения

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

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

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

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

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

С побочными эффектами ситуация интереснее. Дело в том, что основная задача программирования - это автоматизация различных процессов материального мира. Польза от компьютерных программ как раз заключается в наличии эффектов, во взаимодействии вычислителя с окружением. Полностью "чистый" алгоритм имеет нулевую практическую ценность! Решение парадокса заключается в том, чтобы отделить чистые функции от эффективных вычислений - сама программа должна быть максимально чистой для гарантии корректности, а вычисленные описания эффектов отдаются в самом конце общим библиотечным методам или среде исполнения. Этот принцип используется в современных Scala-продуктах, написанных на основе библиотек вроде Cats.Effect или ZIO.

На самом деле, честная проверка наличия побочных эффектов у функции (как "чёрного ящика") оказывается весьма нетривиальной. Оценить "невлияние" вычисления одних функций на другие можно лишь статистически, с определённой долей достоверности. И, вообще говоря, мы получаем целую совокупность классов функций, не влияющих на функции из этого же класса, но потенциально "ломающих" детерминизм функции из других таких классов... Так что, "чистые функции" оказываются не таким уж "чистым", но их роль по прежнему крайне важна как рекомендация, позволяющая повысить качество алгоритмов.

Соответствие Карри-Ховарда.

Доказательство корректности алгоритма должно подчиняться законам математической логики. Развивая теорию типов разные исследователи обращали внимание, что построение конструктивного доказательства очень похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений. Такая схожесть логических систем с языками программирования известна как соответствие Карри-Ховарда:

Логические системы	Языки программирования
Высказывание	Тип
Доказательство высказывания	Терм (значение) типа
Утверждение доказуемо	Тип обитаем (могут быть получены значения)
Дизъюнкция $A\lor B$	Тип суммы
Конъюнкция $A\land B$	Тип произведения $A\times B$
Импликация $A\Rightarrow B$	Экспоненциальный тип
Истинная формула	Тип-единица
Ложная формула	Нулевой тип
Отрицание $\neg A$	Экспоненциальный тип

Корректность программы-функции эквивалентна обитаемости соответствующего ей типа. Таким доказательством является "свидетель" - значение (терм, если точнее) этого типа. Например, значением функционального типа, описывающего программу, является реализация этой программы, внутри которой мы получаем значение типа-результата на основе значений типов аргументов. В то же время невозможно предоставить доказательство обитаемости нулевого типа - такой тип соответствует ложному высказыванию.

Особого внимания заслуживает понятие "отрицание типа": $\neg A\cong0^A$ . В конструктивной теории типов попросту невозможно построить незавершающиеся вычисления. Функции из любого обитаемого типа в нулевой тип просто не существует, тип таких функций необитаем: $0^A\cong0$ . Но если необитаем сам $A\cong0$ , тогда $0^A\cong1$ - единственное значение такого типа-экспоненциала - это функция идентичности. Таким образом, "отрицание" обитаемого типа превращает его в "ложный" необитаемый тип, а "отрицание" необитаемого типа - это "истинный" тип-одиночка!

Логическая тавтология $A\Rightarrow \neg\neg A$ полностью соответствует аналогичному выражению в теории типов - если есть обитаемый тип , то мы всегда можем получить его двойное отрицание - тип-одиночку. Первое отрицание в $\neg\neg A$ даёт необитаемый тип, отрицание которого соответствует типу-одиночке. Но вот обратное утверждение $\neg\neg A\Rightarrow A$ уже не является конструктивным - двойное отрицание типа даёт "истинный" тип-одиночку, но не исходный тип.

На данный момент даже самые передовые разновидности теории типов не позволяют выяснить, может ли завершится абсолютно любая программа, или её тип эквивалентен . Типичный пример проблемного алгоритма - сиракузская последовательность (гипотеза Коллаца). Математики до сих пор точно не уверены завершится ли этот алгоритм для всех чисел, или для каких-то нет. Всё это упирается в более фундаментальную проблему останова - невозможность оценить сложность произвольного алгоритма. Доказано, что в общем случае эта проблема неразрешима.

Тем не менее, наука не стоит на месте. В 2020 году опубликованы исследования экономичной (cost-aware) теории типов, позволяющей учитывать сложность алгоритма и, возможно даже позволит каким-то образом обойти проблему останова. Может быть, в ближайшем будущем разработают достаточно гибкий язык, на котором (опционально) невозможно будет написать программу, упирающуюся в эту проблему, и всегда можно будет доказать, выполнятся ли такие программы, или же нет?

Типизация

Разные языки предоставляют разную реализацию понятий теории типов. Система типов конкретного языка определяется его синтаксисом и грамматикой, а также некоторыми механизмами компилятора языка, для которых используется обобщающий термин "типизация".

Часто используются такие классификации типизаций:

сильная/слабая,
статическая/динамическая,
явная/неявная,
иерархическая/утиная.

Рассмотрим эти классификации подробнее.

Сильная типизация

"Сила" типизации заключается в том, насколько сильно компилятор противостоит попыткам программиста сделать некорректное приведение типов. Например, попытка привести указатель на ячейку памяти со значением типа Int8 к указателю типа Int64 может привести к фатальным последствиям, в худшем случае вы даже не заметите, что данные оказались испорчены. Сильная типизация защищает от некорректного использования памяти компьютера. В то же время, слабая типизация допускает изящные хаки, вроде быстрого извлечения квадратного корня на C++:

y = 4.56e1;                   // 45.6: float   ok
i = * ( long * ) &y;          // ??: int32     слабоватая типизация...
i = 0x5f3759df - ( i >> 1 );  // ???????       ???????
y = * ( float * ) &i;         // √number       ну, примерно)))

Статическая типизация

Динамическая типизация позволяет не указывать типы термов - они будут вычисляться и проверяться в процессе выполнения программы. Это делает язык более простым для освоения, что лежит в основе популярности таких языков, как Python или JScript. Статическая же типизация требует, чтобы типы всех термов были определены на этапе компиляции - факт компиляции обеспечивает корректность алгоритма в той степени, насколько хорошо там использованы возможности теории типов.

Позавидовать питонистам или посочувствовать?..

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

Неявная типизация

Статическую типизацию укоряют в необходимости избыточного аннотирования типами всего подряд. На это обычно отвечают что-то вроде "явное всегда лучше не явного" - девиз Капитана-Очевидность. За это все его и любят... или же не все? На самом деле типы некоторых термов вполне однозначно фиксируются их конструкцией, вложенными термами, или же тип можно определить по месту, где он используется. Типы гораздо точнее документируют абстракции предметной области, чем именованных свойств и методов в классах, но при реализации этих абстракций явное указание типов становится лишним. Ранее, в разделе, где обсуждалось каррирование, был приведён фрагмент кода на языке F# - там типы вообще нигде не указывались, тем не менее, код является хоть и неявно, но статически типизированным, благодаря механизму вывода типов Хиндли-Милнера, используемому в языках семейства ML. Типы настолько круты, что лишний раз их лучше не упоминать в программе!

Капитан-Очевидность всё ещё в восторге от явной типизации.

Утиная типизация

"Если код плавает как утка, и крякает как утка, то скорее это и есть утиная типизация". При утиной типизации не требуется, чтобы значение реализовывало конкретный тип, важно лишь наличие проекторов (свойств, методов) с заданной сигнатурой. В Scala к утиной типизации относится использование так называемых структурных типов:

import reflect.Selectable.reflectiveSelectable      // В Scala 2 это не нужно
final class SampleClass { def f(): String = "кря" } // нет наследников
type StructuralType =   { def f(): String         } // структурный тип

val someVal   : SampleClass    = ???                // реализация не важна
val anotherVal: StructuralType = someVal            // утиная типизация
val intVal    : String         = anotherVal.f()     // кря

В этом примере переменная anotherVal относится к структурному типу { def f(): String }, который не наследует от SampleTrait, но преобразование типов происходит автоматически. Утиную типизацию обычно противопоставляют иерархической подтипизации, основанной на наследовании классов. Утиная типизация значительно слабее иерархической, так как теряется семантика различия типов с разными идентификаторами, но с методами и свойствами одинаковой сигнатуры:

Рассуждения о пользе типов и типизации в программировании приводятся также в статьях Система типов — лучший друг программиста, Почему типы так много значат для программистов? и Типы и функции.

Бестиповое исчисление SKI

Ранее в статье упоминались только типизированные языки программирования. Так что остаётся рассмотреть "бестиповые" языки. К таковым иногда относят Assembler, но это спорное утверждение. Мы же "вернёмся к корням" и рассмотрим язык логики комбинаторов SKI.

Фундаментальные работы по теории типов были опубликованы более века назад. Но в те же десятилетия велись и иные исследования в области обоснования математики и теории алгоритмов. В частности, тогда появились такие дисциплины, как $\lambda$ -исчисление, логика комбинаторов, и в те годы они были ещё бестиповыми. Несмотря на то, что понятия из $\lambda$ -исчисления сейчас более распространены и в математике, и в программировании, логика комбинаторов кажется более подходящим примером бестиповых вычислений.

Основы комбинаторной логики

Основные концепции логики комбинаторов достаточно тривиальны:

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

Можно ли, основываясь на этом, описать вообще любую (чистую) функцию? Давайте разберёмся.

Допустим, мы хотим реализовать свою функцию, принимающую в качестве аргумента какую-то другую функцию. Рассмотрим, что можно сделать с этим аргументом:

можно его просто вернуть - это же просто функция;
можно проигнорировать его и вернуть функцию, которая вернёт свой аргумент;
и самое интересное: можно применить её к самой себе произвольное количество раз!

Многоаргументные функции присутствуют в своём каррированом виде - функция, принимая один аргумент, возвращает другую функцию, принимающую остальные аргументы. Применение функции f к аргументу a записывается просто как f a. Следовательно, вычисление многоаргументной функции в каррированном виде будет выглядеть так: f a b c (или же слитно fabc, если это не вызывает недопонимания). Этот же синтаксис используются языках семейства ML (Haskell, OCaml, F# и проч.). Для разграничения применения функций можно использовать скобки: f a (g c).

SKI и другие базисы

Каждая функция только и делает, что комбинирует применение своих функций-аргументов. В этом и заключается смысл названия "комбинаторная логика". Другое название - "исчисление SKI" - следует из того, что существует простой базис из трёх комбинаторов, с помощью которых можно построить абсолютно любую функцию:

S a b c = a(c)(b(c))
K a b = a
I x = x

Названия комбинаторов имею "птичью" природу, об этом можно прочесть тут.

Комбинатор I на самом деле "немного лишний" в том смысле, что его можно по-разному выразить из первых двух, например

SKKx = K(x)(Kx) = x = Ix

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

ιx = xSK
K = ι(ι(ιι))
S = ι(ι(ι(ιι)))

Кодировки Чёрча

Утверждается, что с использованием базиса комбинаторной логики можно реализовать любую функцию, следовательно, можно написать тьюринг-полный язык программирования. Посмотрим, как это может выглядеть.

Сперва определим вспомогательные комбинаторы (конечно, их также можно выразить через базис SKI):

B a b c = a (b c)
С a b c = a c b

Теперь построим булеву логику (слитно написанные строчные символы - это один идентификатор):

𝐭𝐫𝐮𝐞 = K
𝐟𝐚𝐥𝐬𝐞 = SK
𝐢𝐟 = I

𝐧𝐨𝐭 = C (C if false true) true
𝐚𝐧𝐝 = SSK
𝐨𝐫  = SII

Работает это так:

𝐢𝐟 𝐭𝐫𝐮𝐞 a b = a
𝐢𝐟 𝐟𝐚𝐥𝐬𝐞 a b = b

𝐢𝐟 (𝐧𝐨𝐭 𝐭𝐫𝐮𝐞) a b = b
𝐢𝐟 (𝐚𝐧𝐝 𝐭𝐫𝐮𝐞 𝐟𝐚𝐥𝐬𝐞) a b = b
𝐢𝐟 (𝐨𝐫 𝐭𝐫𝐮𝐞 𝐟𝐚𝐥𝐬𝐞) a b = a

Замечательно! Теперь рассмотрим пары:

𝐩𝐚𝐢𝐫 = BC(CI)
𝐡𝐞𝐚𝐝 = CI true
𝐭𝐚𝐢𝐥 = CI false

𝐡𝐞𝐚𝐝(𝐩𝐚𝐢𝐫 a b) = a
𝐭𝐚𝐢𝐥(𝐩𝐚𝐢𝐫 a b) = b

Теперь определим натуральные числа (нумералы Чёрча) и алгебру над ними:

_𝐧 = (SB)^n(KI) // (SB) применяем n раз к KI
𝐚𝐝𝐝 = CI(SB)
𝐦𝐮𝐥 = B
𝐞𝐱𝐩 = CI

_0 = KI
_1 = SB(KI)
_2 = SB(SB(KI))
_3 = SB(SB(SB(KI)))
//.........

𝐚𝐝𝐝 _2 _3 = _5
𝐦𝐮𝐥 _2 _3 = _6
𝐞𝐱𝐩 _2 _3 = _8

Теперь у нас есть булевский тип суммы с конструкторами 𝐭𝐫𝐮𝐞 и 𝐟𝐚𝐥𝐬𝐞, тип произведения 𝐩𝐚𝐢𝐫 с проекторами 𝐡𝐞𝐚𝐝 и 𝐭𝐚𝐢𝐥, а тип-функции есть в SKI по определению (всё есть функция!). Чтобы сформулировать полноценный язык остаётся лишь добавить возможность вызывать функцию рекурсивно, в частности, чтобы работать со списками. Для этого достаточно определить комбинатор неподвижной точки (как и другие комбинаторы, его можно определить разными способами):

Y = S(K(SII))(S(S(KS)K)(K(SII)))
Y f = f(Y(f))

Последнее выражение не совсем точно. Оно будет работать, если функция f будет "ленивой" - её аргумент будет вычисляться только по требованию, в момент обращения к нему в теле f.

Что-то похожее на SKI можно реализовать на любом современном языке программирования. Также для экспериментов можно воспользоваться существующим языком Unlambda, построенном на основе SKI.

Корректность без типов

Итак, мы получили язык для вычисления без каких либо ограничений. В SKI можно как угодно комбинировать функции и получать при этом совершенно корректную функцию. Корректность без типов! Но какой мы можем придать смысл произвольному комбинатору, если это ни к чему нас не обязывает? Для решения задач из материального мира приходится учитывать определённым образом классифицированные (типизированные!) условия и в этом же ключе нужно будет трактовать результат вычисления. Чтобы учесть такие классификации-типизации необходимо корректного пронести их через все вычисления.

Смысл в SKI может появиться, если ограничить себя некоторым подъязком (DSL), вроде того, что представлен выше - с булевским и числовым типами, с парами, списками и деревьями, и c рекурсией. Бестиповое исчисление приобретает смысл, когда некими ограничениями в нем вводятся типы!

Граф возможных путей упрощения комбинатора неподвижной точки S(S(SS))(K(SK))Sx => x(x). Два пути выделены явно красным и оранжевым цветом. Взято отсюда: https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view . Не знаю, для чего может быть полезна эта картинка, но впечатляет!

Заключение

Итак, мы выяснили,

что типы появились, как минимальная абстракция, позволяющая формализовать процесс вычислений;
как из самого определения типов получаются их основные разновидности: сумма, произведение, экспоненциал;
как понятие изоморфизма типов позволяет определить "школьные" алгебраические отношения между типами (каррирование, сопоставление с шаблонами и проч.) и выбирать наиболее оптимальные пути вычислений;
как элементы теории типов (изоморфизмы и т.п.) реализуются в программировании, в частности, в языке Scala;
что, хотя типы - это не множества, но с типом может быть ассоциировано множество его значений, а для мощностей таких множеств выполняются те же алгебраические соотношения, что и для типов;
как типы, благодаря соотношениям Карри-Ховарда, помогают обеспечивать корректность алгоритмов, построенных из чистых функций.

В дальнейшем есть планы осветить с точки зрения "неизбежности появления" другие абстракции теории типов:

обобщённые, рекурсивные, зависимые типы,
классы типов, в частности, функторы и монады,
и многое другое.

Будет ещё интереснее, так что не переключайтесь!

Tags:

Hubs: