Теория типов / forpes.ru

Главная
Теория типов

Теория типов +58

02.09.2023 12:16

Underskyer1 67 9400 Источник

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

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

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

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

Предисловие

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

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

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

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

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

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

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

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

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

Вавилонская табличка 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 - описание алгоритма остаётся тем же (но потребуются другие реализации моноида). Фактически, множество выступает всего лишь как некий ярлык - связующее звено для композиции различных возможности (моноида и прочих). Так на переднем плане появляется концепция типа.

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

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

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

Тип - это метка терма, позволяющая описать процесс вычисления, указав связи-функции (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;
что, хотя типы - это не множества, но с типом может быть ассоциировано множество его значений, а для мощностей таких множеств выполняются те же алгебраические соотношения, что и для типов;
как типы, благодаря соотношениям Карри-Ховарда, помогают обеспечивать корректность алгоритмов, построенных из чистых функций.

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

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

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

Комментарии (67)

murkin-kot
02.09.2023 15:05
#25923980
+5
типы появились, как минимальная абстракция, позволяющая формализовать процесс вычислений

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

С другой стороны, автор понимает сложность объяснений, связанную с излишне завышенным уровнем абстракции:

Типичный математический текст начинается со знакомства со "взятой с
потолка" абстракцией, и потом рассматриваются её "удивительной красоты"
свойства

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

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

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

Хотя сама возможность вполне простого отображения алгоритма, записанного на функциональном языке, на алгоритм, записанный процедурно, говорит нам о большой сложности задачи популяризации функционального подхода из-за неочевидности его преимуществ. Поэтому не возьмусь как-то умалять труд автора, хотя замечу, что до идеала ему ещё совсем неблизко.
1. GospodinKolhoznik
  02.09.2023 15:05
  #25924022
  +2
  регистрах - байты, биты, слова. И все эти единицы хранения информации уже являлись типизированными
  
  Не являлись. Если я по-невнимательности положу в регистр AX сумму в рублях, а в BX другую сумму в долларах, то ассемблер не помешает мне их сложить друг с другом и получить бредовый результат.
  1. murkin-kot
    02.09.2023 15:05
    #25924162
    +2
    Являлись. Тип такой - целое из Х бит.
    
    GospodinKolhoznik
    02.09.2023 15:05
    #25924184
    +4
    Когда для всех данных один единственный тип, то это не типизация, а отсутствие типизации.
    
    murkin-kot
    02.09.2023 15:05
    #25925252
    -1
    Расскажите это всем авторам языков программирования, которые используют целочисленные типы.
    
    anonymous
    02.09.2023 15:05
    #25926716
    НЛО прилетело и опубликовало эту надпись здесь
    
    murkin-kot
    02.09.2023 15:05
    #25930254
    assembler
    
    anonymous
    02.09.2023 15:05
    #25930460
    НЛО прилетело и опубликовало эту надпись здесь
1. Underskyer1 Автор
  02.09.2023 15:05
  #25924180
  +3
  Первыми практиками были выдающиеся математики, спроектировавшие языки Ассемблера, Фортран и прочие. На ранних этапах типизация байтов была весьма условной - там скорее речь шла именно о множествах возможных значений а не о возможностях, которые предоставляет тип. Представление чисел с плавающей запятой появилось позднее. Понятие о типах, в появилось в математике задолго до первых ЭВМ.
  
  Мотивом статьи было не столько снижение "сложности объяснения завышенного уровня абстракций", сколько объяснение неизбежности появления этих абстракций. Проблема в том, что обычно математики предоставляют уже готовую "красоту", не особо утруждаясь обоснованием. А потом практики смотрят на это с мыслями вроде "красиво, но нафига, а главное, зачем это мне?". Не считаю, что с поставленной перед собой задачей справился "на отлично", но всё же постарался донести, что в следствие неизбежности появления, эти абстракции являются фундаментом в том числе и в области обеспечения корректности ~~компьютерных программ~~ любых алгоритмов (да, теорию множеств и сейчас развивают в этом плане, но это дальше от программирования и там всё оказывается намного сложнее).
  
  Популярность императивного (процедурного, если угодно) программирования обуславливается в первую очередь историей развития электронно-вычислительной техники. Первые языки программирования строились вокруг архитектуры процессоров. Тогдашние компиляторы просто не тянули абстракции, далёкие от железа. Для популярных тогда языков писалось множество книг, курсов обучения семинаров. Разрабатывались и популяризировались императивно-ориентированные техники программирования. Позднее появилось ООП, в пропаганду которого также влиты гигантские деньги... Но популярность, на самом деле, слабо коррелирует с качеством этих методов. Сейчас компьютеры и компиляторы сильно поумнели, функциональная парадигма стала весьма актуальной, но преодолевать огромную инерцию общественного мнения всё тяжело. Тем не менее, тенденции на изменение мира к лучшему прослеживается везде - в публикациях, в развитии языков программирования и т.п. Без относительно того, замечают ли это сами программисты))
  
  Вообще, такую холиварную тему, как преимущества ФП, наверное, имеет смысл осветить в отдельной статье (угу, ещё одной на эту тему...). Если подумать, то фундаментальный набор абстракций, необходимых для качественного программирования гораздо меньше, чем всё то, чему сейчас традиционно учат в школах/вузах. А научить человека писать качественные программы в традиционной парадигме сложнее, чем в функциональной. Впрочем, данная статья не столько про ФП, сколько про фундаментальность фундамента ФП)))
  
  Безусловно, автору есть многое, над чем нужно поработать. Прошу не судить слишком строго - это мой первый опыт публикации статьи. Большое спасибо за отзыв!
  1. GospodinKolhoznik
    02.09.2023 15:05
    #25924194
    +1
    Вы, наверное на scala пишите, если выбрали её для демонстрации примеров. Сколько раз не пытался, так и не смог писать на Скале в функциональном стиле, такое ощущение, словно язык сопротивляется тому, чтобы код был функциональным и пытается вынудить писать в императивно-оопшном стиле. Когда пишу на Хаскеле или Racket(типизированный Лисп) такого не возникает.
    
    Возможно это связано с тем, что в скале постоянно используются джавовые либы, и при использовании их API неизбежно приходится городить ООП.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25924244
    +1
    Да, последнее время больше пишу на Scala. У языка не мало проблем, по большей части из-за "беттерджавного" наследства. Но в нём сочетаются как традиционные для большинства популярных языков решения, так местами весьма глубокие ФП-шные вкусности. Так что несмотря не некоторые недоработки в плане ФП, мне кажется, он здорово подходит для демонстрации кода в подобных статьях.
    
    Какое-то время назад попробовал в реальном проекте Tagless Final в экосистеме cats и остался доволен - ООП вынесена куда-то на периферию, а про опасную "нечистую" императивность вообще практически можно было забыть))
    
    На всяких Haskel мало кто хочет писать продуктовый софт, а Scala приносит не только боль))
    
    anonymous
    02.09.2023 15:05
    #25924682
    НЛО прилетело и опубликовало эту надпись здесь
    
    sshikov
    02.09.2023 15:05
    #25925272
    Довольно голословное утверждение.
    
    Ну так это чисто субъективный взгляд автора. Как по мне, таких как вы таки на сегодня мало. И даже скорее не потому, что никто не хочет, а вот представим, что я хочу — но это автоматически означает, что мне нужно не просто самому научиться, но и научить команду, а это уже совсем другие требования. И экспертов-то мало, а экспертов готовых научить (и умеющих) — еще меньше. Их и по скале-то кот наплакал.
    
    если в ваших приложениях это полезно, то и на скале писать, конечно, выгоднее, а иначе… ну хз :]
    
    Ну да, у нас во все API — это JVM, ну или по большей части они, и что получается, когда Scala или даже Java заменяют хотя бы на Python — я прекрасно вижу каждый день. Если в том же спарке для питона сделали специальную обертку — то еще как-то можно жить, если забыли — то это тоже боль. Потому что совместимости нету. Ну вот авторы спарка в очередной версии 3.4 обещали, что переделают весь API, так чтобы его можно было дергать из Go, например — то есть, не из JVM языков, может у нас что-то и изменится (когда оная 3.4 до нас доедет).
    
    anonymous
    02.09.2023 15:05
    #25926956
    НЛО прилетело и опубликовало эту надпись здесь
    
    sshikov
    02.09.2023 15:05
    #25929782
    Да, специалистов по скале мало, но как их учить из специалистов по Java, я более-менее представляю. По крайней мере с учетом нашей специфики Spark, где самого языка мало, а много его спарковского API.
  1. murkin-kot
    02.09.2023 15:05
    #25925280
    +1
    Первыми практиками были выдающиеся математики, спроектировавшие языки Ассемблера, Фортран и прочие.
    
    Например, в википедии авторство ассемблера приписывают двум авторам, выпустившим книгу с описанием раннего прототипа ассемблера в 1947 году. Один из авторов по образованию математик, но второй - инженер электрик. Кто из них двигал идею упрощения работы при кодировании программ? Как вы думаете?
    
    Сама по себе идея сделать так, что бы писать было проще, становится очевидной любому, кто должен был писать что-то сложное, особенно в машинных кодах. Напрашивающаяся мысль о замене цифровых кодов буквенными обозначениями, хоть немного похожими на слова, просnо обязана была прийти в голову в первую очередь именно практикам. Ну а отсутствие в такой подстановке каких-либо существенных математических идей подсказывает нам, что математикам такая идея в голову просто не должна попасть, ибо зачем вносить в математику "изобретения" уровня 2+2=4?
    
    Аналогичная история была и с фортраном, и с си, и со многими другими языками.
    
    Хотя функциональный подход, соглашусь, был заимствован прямо из математики. И здесь авторство легко доказуемо, если мы сравним даты появления лямбда-исчисления с датами появления функциональных языков. Но какие даты вы бы предложили сравнить в случае с ассемблером и тому подобными малыми (но вносящими много удобств) изменениями теории языков программирования?
    
    Мотивом статьи было не столько снижение "сложности объяснения завышенного уровня абстракций", сколько объяснение неизбежности появления этих абстракций.
    
    Вообще, стоит указывать конкретику. Если речь идёт о типах, то это один подход, идущий своими корнями в древнюю грецию, а может и много дальше, то есть в те времена, когда люди впервые пришли к понятию классификации, то есть разделения наблюдаемых явлений на группы по сходству тех или иных признаков. Соответственно, "неизбежность" здесь несколько натянутая - разве можно подумать, что кто-то осмысленно (то есть мы не говорим об откровенных идиотах) отказался бы от накопленных тысячелетиями примеров полезного применения инструмента с названием "классификация"?
    
    Если же речь идёт о функциональном подходе, то неизбежность пока что не случилась. Как было упомянуто ранее, лёгкость отображения алгоритмов на много способов их формальной записи, не предполагает лёгкой победы одного из подходов, даже если за ним стоит авторитет математиков. Для победы нужно нечто большее - реальное и заметное без микроскопа облегчение работы по созданию программ.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926066
    Ассемблер создавался, чтобы была возможность записать программу не в виде дырок на перфокарте, а текстом. С прицелом на кроссплатформенность. Семантика языка целиком определялась архитектурой тогдашних процессоров, которые проектировались ведущими учёными. Впрочем, это был по-прежнему язык для пенетрации перфокарт, а не для консольного ввода.
    
    Фортран, Алгол уже создавались по заказу целыми комитетами, куда входили так же самые достойные учёные. Все остальные языки уже шли по их стопам и не особо отступали от первоначальных конструктов.
    
    Деление людей на практиков и "тех, других" вообще кажется не совсем корректным))
    
    Типы - это вполне конкретная абстракция)) Не так важно, кто их придумал, как то, что начиная с определённого периода они начинают изучаться и использоваться повсеместно. Те определения которые лежат в основе теории типов появились вследствие накопившегося объёма проблем, для решения которого старые абстракции не работали, или были неудобны. Именно это я и называю "неизбежностью".
1. Underskyer1 Автор
  02.09.2023 15:05
  #25924274
  И ещё одна ремарка))
  
  Эволюция ФП следует за математикой. А вот традиционное императивное (процедурное, объектно-ориентированное...) программирование - это уже законченные идеи. Они очень вяло мутируют исключительно за счёт впитывания ФП-шных техник.
  1. kozlyuk
    02.09.2023 15:05
    #25924820
    +5
    Императивное программирование выросло из железа и следует за ним. Базовые концепции присутствуют со времен первых компьютеров: вычисления на последовательных шагах (тактах) и изменяемые переменные (регистры, ячейки памяти). Более близкий пример: в семантике языка C запечатлены свойства PDP-11 (C Is Not a Low-Level Language). Объектно-ориентированное, процедурное и даже фундаментальное структурное программирование — это просто способы ограниченным человеческим мозгам ворочать все большим количеством тех же самых элементарных инструкций. Новые подходы в теории типов позволяют выразить в коде более сложные утверждения, инварианты решаемой задачи. ООП и даже элементы ФП в императивных языках не позволяют выразить больше, чем уже можно было выразить машинным кодом — лишь помогают человеку не сделать ошибку при записи. Новых базовых концепций долго не было, соответственно, не было эволюции в том же смысле, что у теории типов, то есть, чтобы стало можно решать принципиально больше задач. Настоящее развитие императивного программирования — квантовые вычисления, поскольку элементная база не позволяет иметь, как минимум, классические переменные. Глядя в обратную сторону, до появления компьютеров "железом" была голова, которой тяжело делать шаги не последовательно, и записи, которые можно править.
  1. murkin-kot
    02.09.2023 15:05
    #25925286
    Пример - расширяемые типы. Они введены в ряд процедурных языков под названием generics. Назовите аналог в лямбда-исчислении.
    
    Это всё к тому, что разделение на концепции (типы и функциональный подход, то есть два разных направления) показывает нам, что практики не во всём были дурнее паровоза.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926076
    Лямбда-исчисление тоже не стоит на месте. Обобщённые типы - это отображения из типа в тип, то бишь функции, что вполне укладываются в лямбда-исчисление. Вообще - это тема моего следующего проекта для хабра))
    
    Ни в коем случае не стараюсь как-нибудь принизить "практиков", кого бы Вы не имели ввиду))
    
    GospodinKolhoznik
    02.09.2023 15:05
    #25926688
    Я наверное что то не понимаю, но о каких типах в лямбда исчислении может идти речь? Ведь лямбда исчисление создавалось, как "математика без множеств", а значит и без типов.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926752
    Создавалось-то оно как бестиповое, но типы в нём появились достаточно скоро. Лямбда-выражения в современных языках построены именно на типизированном лямбда-исчислении.
    
    anonymous
    02.09.2023 15:05
    #25926958
    НЛО прилетело и опубликовало эту надпись здесь
    
    murkin-kot
    02.09.2023 15:05
    #25930286
    Понятие "нормально" требует определения. И я уверен, что ваше не будет принято большинством, просто потому, что вы с ними на разных полюсах планеты "привычки".
    
    anonymous
    02.09.2023 15:05
    #25930472
    НЛО прилетело и опубликовало эту надпись здесь
1. EireenK
  02.09.2023 15:05
  #25925770
  Вода и канцеляриты в ваших комментариях как ~~из диплома~~ от "искусственного интеллекта". Сделать, что ли, в своём расширении для хабра возможность пометок "WARNING: ~~царь~~ автор ненастоящий". Даже если автор изначально мясной, но балуется, то ему же хуже. Читать беседы ботов я не хочу.

gochaorg
02.09.2023 15:05
#25924420
Извините, но вот

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

Почему они не могут считаться полными, и что нам дает отсутствие или наличие еще An... ?

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

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

Зачастую такие отображения бывает удобно отобразить на диаграмме в виде ориентированного графа

Это про все виды отображений или про некоторые виды, отображений? если про некоторые, тогда стрелки в обратную сторону в случае сюръекции не возможны (или возможны) ?
1. Underskyer1 Автор
  02.09.2023 15:05
  #25924534
  Тут речь идёт об однозначности формулировки типа. Вопрос в том, какой тип мы можеи назвать "А1 или А2". Или же не получится выделить какой-то единстаенный тип, подходящий под эту формулировку?
  
  Понятие универсального свойста позволяет однозначно формулировать новые типы. В этой статье подобные вопросы раскрываются очень хорошо, на мой взгляд.
  
  Стрелки-то можно нарисовать какие угодно, но в теории типов принято ассоциировать такие стрелки с конеретными функциями, принимающие аргумент одгого типа и возвращающие значение другого типа (отображение между типами). Т.е. буквально, если у вас есть функция из А в В (написанная только что, или например, неявное преобразование к сурертипу от компиляьора...), то вы можете соединить на диаграмме эти типы стрелкой в соответствующем нарравлении.
  1. gochaorg
    02.09.2023 15:05
    #25924764
    Я же правильно понимаю, что если допустим имеем 2 исходника source-1 source-2 (допустим C)
    
    оба содержат по структуре в которых имена полей разные, но их кол-во и типы полей совпадают, а так же их последовательность
    
    пример
    
    struct A { int a; int b; } struct B { int c; int d; }
    
    Компилятор С как знаем обращается к полям не по имени, а по смещению
    
    то тогда верно утверждать что это один и тот же тип ?
    
    anonymous
    02.09.2023 15:05
    #25924842
    НЛО прилетело и опубликовало эту надпись здесь
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25925172
    Типы изоморфные (при слабой типизации всегда можно переломать указатель с одного типа на другой и обратно без потерь), но разные. С этими типами могут быть связанные разные наборы функций, а типы как раз и отличаются разным набором входящих и исходящих отображений - положением на общей диаграмме типов.
    
    anonymous
    02.09.2023 15:05
    #25926960
    НЛО прилетело и опубликовало эту надпись здесь

gochaorg
02.09.2023 15:05
#25924486
+1
Формулирование типов через универсальные свойства (уникальные кратчайшие пути) помогает факторизовать вычисления - декомпозировать сложные задачи на простые и описать их с помощью типов.

Я дико извиняюсь, но можно как-то разжевать для обычных смертных, что значит
- формулирование типов через уникальные свойства ?
- как проявляется помощь в факторизации вычислений ?
- что за фактор ?
- о каких сложных задачах идет речь? те что в jira или те что доказательство P = NP ?
- что значить описать с помощью типов? пример бы глянуть, о чем речь.
Я смутно догадываюсь о чем речь, но смутно

Про сумму типов

Вот не плохо бы разжевать, есть другое более наглядное объяснение в рамках Scala - это Either, можно сказать Either это такой enum
```
enum Either[A,B] {
  Left(A),
  Right(B)
}

// или Scala2
sealed trait Either[A,B]
case class Left[A,B](a:A) extends Either
case class Right[A,B](b:B) extends Either
```
и дать например ссылку сюда https://github.com/anton-k/ru-neophyte-guide-to-scala/blob/master/src/p07-either.md

Что в конечном итоге Left/Right - это тип (.class) внутри JVM и к некой переменной a типа Either, применима операция instanceOf, а match - это сахар над instanceOf.

Что важно, что переменная a не может одновременно содержать Left и Right. Но, при этом сохраняется информация о типе, что Either переменную можно определить Left/Right - и извлечь ее и с ней работать, зная что она Left.

Тут важно еще пояснить, зачем это знать, просто в Scala - world, точнее в части ее библиотек не принято кидать Exception, и большинство функций используют такую семантику:
```
// было
def some_fun( arg: A ): R

// стало
def some_fun( arg: A ): Either[Error,R]
```
Что обычно в Left хранятся ошибки и это знание важно, а вот не просто, так нам захотелось ввести Left/Right
1. Underskyer1 Автор
  02.09.2023 15:05
  #25924600
  Важный момент. Наверное стоило раскрыть его подробнее.
  
  Вычисления обычно проводяься так: на входе у нас есть значение типа А (возможно, несколько значерий, объединённых типом-произведением), передав его в одну функцию, получаем значение типа В и так далее. Получаетя цепочка вида А->В->...->R - по сути это один из путей на диагрмме типов. Задача состоит в том, чтобы найти путь до R как можно короче.
  
  Допустим есть три функции А->В, В->С и А->С. Очевидно, что если мы хотим получить значение типа С из А, то вызов последней функции будет оптимальнее, чем последоаптельный вызов пнрвых двух - путь на диаграмме короче. Уникальность универсального морфизма и определяет его оптимальность - из всех возможных путей он оказыаается самым коротким. Строя вычисления, основанные на универсальных свойствах типов как раз и получается находить наиболее коротеие пути вычислений.
  
  Под факторизацией здесь понимается разделение длинного пути вычисления на отдельные шаги-функции. По сути, декомпощиция задачи. Возможно, не самое удачное использование слова "факторизация"...
  
  По поводу типа Either я в статье отметил, что не зотел углублятся в тему обобщённых типов - что это и почему их можно захотеть. Надеюсь написать об этом отдельную статью, и её публикация окажется достаточно обоснованной))
  1. gochaorg
    02.09.2023 15:05
    #25924810
    +1
    Я вот про ту самую цепь A->B->C, в целом понятно, что чем короче путь - тем "лучше"
    
    Просто у меня может не правильное понимание, допустим есть такие функции
    
    def a( value:Long ):Int = value % 10 def b( value:Int ):String = value.toString val result = b(a(10))
    
    def c( value:Long ):String = value.toString
    
    Формально с - это короткий путь из Long в String, но его результат очевидно не совпадает с композицией b * a
    
    Я тут сознательно нарушаю, я так понимаю правильнее всего говорить не о буквальной трактовке типов, а о таких типах которые при вычислении значений не дают отличий ?
    
    В теории хороший компилятор пометил бы результат композиции b * a - как некий тип String* (со звездочкой, а-ля зависимый тип) и данный тип не был эквивалентен типу из результата функции c.
    
    Или рассуждения не верны ?
    
    gochaorg
    02.09.2023 15:05
    #25924824
    Другой вопрос, всякий раз когда я смотрю на диаграмму суммы типов
    всегда мучает вопрос, а при чем тут D ?
    
    ну хорошо, есть у нас такие пути
    1) A -- ia -> A+B -- u --> D
    2) A -- f --> D
    
    вроде как короче, A+B получается тогда - как пятое колесо телеге, может сразу из A в D, и выкинуть из проекта A+B ?
    
    A+B - это вроде важный концепт и выкидывать его не хочется
    Что хотел сказать автор этим ? или я читаю не глазами, а жо---ой
    
    Формально я понимаю, что запись в языке `def f( a: A | B )` - короче, чем воротить свои велосипеды с sealed + case class
    
    Другое так же понимаю, что def f( a: A & A ) формально это def f( a: A )
    
    По простой причине некий тип A обладает теми же методами, что и A
    
    А вот тип A & B - по сути обладает методами и свойствами обоих типов одновременно, интересно другое
    
    допустим A имеет метод def f( a : Int ) = a % 10,
    
    а тип B имеет такой же метод, но с другой реализацией def f( a: Int ) = a % 16
    
    тогда вызов a.f( 13 ) - какая в итоге будет вызвана реализация - это на откуп компилятору отдается.
    
    Если сумму типов рассматривать как множественное наследование, тогда как-то легче в голове уложить.
    
    anonymous
    02.09.2023 15:05
    #25924986
    НЛО прилетело и опубликовало эту надпись здесь
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25925208
    Обзор и так получился гигантским. Очень много деталей оказалось за бортом. Для тех, кто заинтересуется, оставлены лишь прямые ссылки, или намёки для загугливания.
    
    Многие понятия были сформулированы ещё в теории типов раньше, чем на её основе появилась теория категорий. Тут лишь хотелось бы подчеркнуть, что понятие универсального свойства автоматически следует из желания чётко сформулировать, что такое типы "А и В", "А или В" и другие. Без чёткой формулировки мы не сможем оперировать этими понятиями, чтобы конструктивно доказывать корректность алгоритма.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25925218
    +1
    С множественным наследованием та же беда, что и с пересечением типов в Scala. Чтобы как-то обеспечить предсказуемость поведения нужно идти на какие-то компромиссы, гвоздями прибивать какие-то дополнительные правила к спецификации языка...
    
    "Сторонние" типы в формулировании универсальных свойств нужны как раз для того, чтобы как-то определить способ, как из них выброать самый оптимальный - универсальный.
    
    gochaorg
    02.09.2023 15:05
    #25925646
    Спасибо за комментарий
    
    Я же правильно понимаю, что множественное наследование - это та самая приславутая проблема алмаза, и что она успешно решается в рамках С3 линириализации https://ru.wikipedia.org/wiki/C3-линеаризация ?
    
    Я к той же Scala, где в Scala 2 до умножения типов (A & B & C) использовали подход class SomeClass extends A with B with C ?
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926126
    Да, все эти вопросы вокруг примерно одной и той же проблемы. Есть разные алгоритмы её решения, но, сугубо на мой взгляд, было бы проще не создавать саму проблему)) "Наследование" - очень популярная, но не самая лучшая идея))
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25925180
    +1
    Типы в этой схеме фиксированы, но тут играет роль понятие коммутативности путей. В данном случае пути "c" и "b * а" не коммутативны - не для всех исходных значений будет получен одинаковый результат. "Коммутативность" входит и в понятие универсального свойства - "существует единственный морфизм, делающий диаграмму коммутативной".
1. primetalk
  02.09.2023 15:05
  #25924626
  +1
  Мне кажется, автор достаточно удачно провёл границу между тем, что включить в статью, а что оставить за рамками. Предложенные Вами примеры сами по себе неплохие, но, на мой взгляд, не очень вписываются в стиль статьи. В частности, instanceOf, перекос (bias) Either, исключения - это низкоуровневые детали реализации, несущественные с точки зрения рассматриваемых понятий.

karrakoliko
02.09.2023 15:05
#25924978
+3
Потрясающая статья.
Спасибо за проделанную работу!

spidersarecute
02.09.2023 15:05
#25925144
+2
Статья очень интересная, но очень непонятная. Видимо, рассчитана не на новичков. Постоянно при чтении возникают вопросы:

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

Абстрактный моноид обычно описывается так:
ассоциативная бинарная операция

У вас написано сначала, что «моноид» это набор функций, но дальше в определении вы пишете «[одна] бинарная операция». Противоречие.

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

Как можно в алгоритме заменить int на string и получить тот же алгоритм? 2 + 2 = 4, но "2" + "2" = "22". Было бы хорошо, если бы вы привели пример в статье.

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

Я не понимаю, что на этом графе является узлами и что обозначают ребра. Узлы - это типы (вроде Int, String), а ребра - функции, которые преобразуют их (вроде strlen(), которая преобразует String в Int)? А где тут тогда функции, принимающие несколько аргументов? Было бы хорошо, если бы вы объяснили, как строится такой граф и привели пример графа для простого алгоритма.

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

Я не вижу тут логики. Вот у нас есть тип String, мы из него можем получить Int (длина строки) и Bool (является ли строка пустой), тогда по вашей логике, String это «Int и Bool»? Очевидно же, что нет.

Но с другой стороны, например, если для A_1 есть отображение в A_2, то A_2 вполне можно исключить из определения типа C. Аналогично, среди типов B также могут найтись те, кто связан с отображениями, значит там тоже кого-то можно исключить из формулировки C через произведения.

Здесь просто непонятно ничего. Что значит «связан с отображениями»? Что значит «из формулировки C через произведения». Слово «произведения», конечно, вызывает в памяти product types, но в статье до этого момента про них ни слова.

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

Что значит «универсальный представитель»? По какому критерию он «наилучший»? Что за свойство имеется в виду?

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

Я не понимаю, если у нас функция одна и единственная, то откуда взялись «все функции, связывающие эти типы»?

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

Что значит «соответствующая диаграмма»? Диаграмма всех типов и функций в программе? И зачем нужно условие про диаграмму, если у нас есть только одна функция, возвращающая значения типа? Где тут возьмутся «разные пути» (из определения коммутативности), если стрелка к этому типу только одна?

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

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

Для любых типа D и функций f и g существует единственный (с точностью до изоморфизма) тип A+B и единственная функция u, делающие диаграмму коммутативной.

Я не очень понимаю, если у нас есть функции f и g, преобразующие A и B в D, то зачем нам тип A + B? Он выглядит как лишнее звено. И еще не понимаю, как будет выглядеть диаграмма, если A и B это один и тот же тип, например, Int.

Для любых типа D и функций f и g существует единственный (с точностью до изоморфизма) тип A\times B

У вас на диаграмме C вместо D...

Если мы формулируем какое-то универсальное свойство, то мы автоматически получаем и дуальное ему.

Было бы неплохо объяснить с простыми примерами, что значит дуальность. Я встречал это слово в нескольких местах (например, в схемах логических элементов на CMOS-транзисторах), но тут это явно что-то другое.

Но сперва давайте рассмотрим те же самые типы, но с другой точки зрения. Переобозначим конструкторы типа B i_1 и i_2 п проекторы типа A p_1 и p_2, получая A=B\times B.

А нельзя ли тут было привести простой пример с типами вроде Int? Пусть A это Int. Тогда B = A + A = A × 2 это структура из Int и, допустим, Bool, а по формуле A = B×B, получается Int = структура из 2 таких структур? Что-то в голове не укладывается.

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

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

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

val div = (a) => (b) => a/b val div10 = div(10) // Зафиксировали 1-й аргумент var divBy2 = ??? // а как зафиксировать второй?

Нелогично, согласитесь?

Я бы заменил каррирование на фиксирование произвольных аргументов:

val div = (a, b) => a/b val divBy2 = div(?, 2)

Вот так гораздо удобнее и логичнее, чем с вашим каррированием.

Такой тип-одиночка называется единицей

В чем смысл использовать тип, у которого единственное значение? Не проще ли вообще ничего не передавать в функцию тогда?

A × 0 = 0

Непонятно, как это интерпретировать. Структура из 2 полей, где первое имеет тип A, а второе?
1. sshikov
  02.09.2023 15:05
  #25925258
  +3
  У вас написано сначала, что «моноид» это набор функций, но дальше в определении вы пишете «[одна] бинарная операция». Противоречие.
  
  Одна функция — это тоже набор функций. Попробуйте мыслить чуть абстрактнее.
  
  Как можно в алгоритме заменить int на string и получить тот же алгоритм? 2 + 2 = 4, но "2" + "2" = "22".
  
  Тут две части алгоритма. Одна часть — это функция "суммирования", что бы это ни означало. Она "складывает" два аргумента, и она разумеется является разной для строк и целых, и она специфична для каждого типа. Другая часть — это функция высшего порядка, которая может работать с разными функциями "суммирования" (смысл у которых может быть достаточно разный, поэтому обычно это называют более общим термином свертка), при условии, что они удовлетворяют некоторым свойствам. Пример тут очень простой — функция высшего порядка fold/foldr/reduce и многие другие названия, потому что такие функции существуют во множестве языков.
  
  То что вы многое не поняли — вполне естественно, статья довольно сложная и не для новичков.
1. Underskyer1 Автор
  02.09.2023 15:05
  #25925270
  Уровень статьи выше "начального", но далёк от "сложного"))
  
  Бинарную операцию в моноиде можно трактовать как функцию из пары значений (ну или в каррированном виде). С другой стороны, нейтральный элемент можно понимать как нулярную операцию, не принимающую аргументов типов А - функция из типа единицы. Итого, моноид - это пара функций. Ловкость рук и никакого мошенничества))
  
  Алгоритм определяется прежде всего своей сигантурой. Например, на входе список типа А, а на выходе значение типа А. Если мы ничего не знаем про тип А, но на предоставили моноид для типа А, то мы можем свернуть этот список. При разных типах и разных моноидах результат будет, конечно, разный, но сам алгоритм свёртки списка не измениться. Попробуйте сами написать такой алгоритм, например, с циклом foreach (на входе список тип А и моноид для него, а на выходе значение типа А) - алгоритм не будет зависеть от того, что именно пониматься под А.
  
  Несколько аргументов на вход функции - это кортеж - произведение типов, которое также отображается на диаграмме типов. А значит там есть место и для функции от нескольких переменных.
  
  По поводу заморочек с универсальным свойствами - часть ответов есть в самой статье, а за подробностями обычно предлагаю перейти по этой ссылке.
  
  Про каррирование тоже можно отдельную статью написать)). Обычно используется в тех случаях, когда какая функция требует на вход функцию меньшего числа аргументов, чем у нас есть, а первый аргумент можно фиксировать. Иногда сразу опеределяют функции в каррированном виде, а в других случаях можно воспользоваться методами, уже реализованными в стандартной библиотеке языка. В статье подчёркивается сам факт наличия такого изоморфизма. А примеров применения его в интернете не мало (боюсь у меня сейчас не найдётся возможности написать что-нибудь прямо в этом ответе((( )
  
  Метод без параметров эквивалентен функции из единицы. Просто в теории типов речь всегда идёт о функциях одного аргумента (даже если это кортеж).
  
  В статье говорится не о равенстве типов (А, Nothing) и Nothing, а об их изоморфизме - значения обоих типов невозможно получить честным (чистым) способом.

Myclass
02.09.2023 15:05
#25925210
Статья по стилю и оформлению хорошая. Но уверен, разбив её на несколько статей - было-бы правильней. Но всё равно - спасибо.

Многие вопросы по теме затронули предыдущие комментаторы. Хотел-бы со своей стороны маленькую деталь спросить.

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

Подтипом считать можно, но такого понятия как подтип в языках ведь не существует и на этот манер под такой подтип можно и bool занести. Он вообще наверное по вашим критериям основа всех типов?

И гибкость подтипов - не совсем понял, какая практическая польза от этой 'гибкости' типов? Но видать статью надо попробовать ещё раз пройти.
1. Underskyer1 Автор
  02.09.2023 15:05
  #25925478
  +1
  Спасибо за отзыв! Хотел, разбить статью, но не получилось - каждый раздел получается незаконченным, оторванным от основной темы.. Видимо, опыта пока малоато))
  
  Понятие подипизации есть в разных языках, но в каждом оно может иметь какие-то отличительные особенности. Где-то вполне допускается неявное привеление от bool к int (0 или 1), а в других языках - нет.
  
  "Гибкость" подтипищации упомянута в сравнении с наследованием, которое часто путают с подтипищацией. Подтипищация проявлятся как наличие неявного преобразования от одного типа к другому. Во многих языках мы можем сами создаватьнеявные преобразования (гибкость)) - иерархия наследования нас не ограничивает.
  1. gochaorg
    02.09.2023 15:05
    #25925692
    Я в своем pet-proj делал для себя компилятор, так чтоб всегда вычислялись типы конечного выражения и в рамках вычисления проводил проверку на совместимость типов
    
    в качестве совместимости я определил одну бинарную функцию isAssignable( left: Type, right: Type ) : bool, в Scalа она выглядила так leftSomeType.isAssignable( rightType )
    
    при помощи нее строил граф отношений (частично упорядоченное множество на базе упомянутой функции) в рамках области видимости импортируемых типов
    
    isAssignable включала как и отношения наследования, так и не явных преобразований из Int в Long
    
    Правильно ли я понимаю что речь именно о этом ? что это и есть случай под-типизации ?
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926162
    isAssignable, судя по названию, как раз проверяет наличие неявного преобразования. Оно может предоставляться как вручную, так и автоматически, если классы связаны наследованием.

Sergey_Kovalenko
02.09.2023 15:05
#25925572
Знаком с математической логикой и теорий категорий. Где-то на индексных типах понимание текста утратилось полностью. Думаю для человека, который видит это впервые, будет совершенно не понятно. Предлагаю эксперимент: напишите 5-6 задач на понимание "вашей теории типов" и сделайте опрос, кто сколько решил.
1. Underskyer1 Автор
  02.09.2023 15:05
  #25926168
  Где-то на индексных типах
  
  Все совпадения названий с "книжными" совершенно случайны!))
  Кажется, что контекстуальный смысл слова "индекс" раскрыт в статье, разве нет?
  
  В любом случае, тут я не раскрываю "свою теорию типов". Как и было упомянуто в начале, это лишь поверхностный обзор основных понятий теории. А за деталями лучше обращаться к специализированной литературе. Мною допущено много вольностей в изложении, но если есть принципиальные ошибки, которые могут ввести читателя в заблуждение - буду рад их исправить.

rukhi7
02.09.2023 15:05
#25925630
Насколько я понял статья рассматривает "Теорию типов" как некую всем известную теорию, неужели никто не поинтересуется кто же является автором этой всем известной теории, в каком году появились первые упоминания этой теории, неужели никому не интересно?

Неужели никто не обратит внимания на то что определения в виде:

Тип - это не более чем некая метка, приписываемая к каждому терму (переменной, выражению и т.п.)

Никак не достаточно чтобы основать какую либо теорию!

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

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

Вы же можете прочитать здесь и то что пропагандирует эта статья:

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

...

Не знаю, для чего может быть полезна эта картинка, но впечатляет!

Неужели никого не смущает что "Теория" нашла "язык без ограничений" для области применения ВНЕ смысла или смыслов.

Я согласен: потрясающая статья!
1. Underskyer1 Автор
  02.09.2023 15:05
  #25926188
  Не нужно воспринимать эту статью как некое научное откровение. Это именно что популярный поверхностный обзор известных положений теории типов. Уверен, что у аудитории достаточно высокий уровень, чтобы именно в таком ключе воспринимать эту работу. После прочтения у читателя может возникнуть много вопросов, на некоторые пробую ответить сам, ответы на другие несложно найти в свободном доступе.
  1. murkin-kot
    02.09.2023 15:05
    #25926226
    +1
    Это именно что популярный поверхностный обзор известных положений теории типов
    
    Тогда вы начинаете противоречить самому себе. Ранее вы утверждали, что хотели показать неизбежность применения теории типов в программировании. Теперь - это уже просто обзор.
    
    Со своей стороны соглашусь с комментаторами, которые указывают на сложность понимания статьи. Если внимательно вчитываться, да ещё пользоваться дополнительными источниками, тогда можно понять о чём речь. Но терпение заканчивается и далее статья просто пролистывается до комментариев.
    
    Задайте себе следующие вопросы:
    
    Кто ваша целевая аудитория?
    
    Как много представителей такой аудитории на популярном околоайтишном ресурсе?
    
    Сколь сильна мотивация тех, кто всё же соответствует пересечению множеств "целевая аудитория" и "аудитория ресурса"?
    
    Сколько человек из полученного пересечения смогут выдержать напряжённое чтение с постоянным отвлечение на дополнительные источники информации?
    
    Сколько из способных выдержать плюнут на всё и получат информацию из более подробно излагающих тему материалов?
    
    Надеюсь, в следующий раз вы поменяете способ изложения.
    
    А про мотивацию добавлю, что она есть следствие понимания нужности и важности темы для читающего. Но именно пояснению полезности вы и не уделили внимания, а это стоило начать делать с первых же строк. Пример вам уже приводили - покажите преимущество подхода в сравнении с альтернативой.
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25926658
    +2
    Среди законов Мёрфи есть такой: "Если есть хоть один шанс, что вас поймут неправильно, то вас ОБЯЗАЕЛЬНО поймут неправильно"))
    
    Никаких противоречий в своих словах не вижу. В этой статье не излагался какой-либо "подход", полезность которого осталась не раскрытой. Это именно фрагментарный обзор (местами сложной) теории, без глубоких деталей. С акцентом на не раз уже упомянутую в комментариях "неизбежность", естественность появления представленных абстракций.
    
    Представленный материал интересен мне самому, я верю что найдутся читатели, с кем я смогу разделить эти интересы. Да, такой формат и стиль изложения может понравиться не всем, но, как говорится, всем не угодишь... Важным показателем для меня являются оценки под статьёй и комментарии читателей, в том числе и Ваш. Постараюсь учесть все мнения при подготовке следующей статьи.
    
    murkin-kot
    02.09.2023 15:05
    #25930292
    Если есть хоть один шанс, что вас поймут неправильно, то вас ОБЯЗАЕЛЬНО поймут неправильно
    
    Забавно конечно, но математическое сообщество давно выработало защиту - полнота и точность определений.
  1. rukhi7
    02.09.2023 15:05
    #25929200
    -3
    я как раз воспринимаю эту статью как не-научное откровение, как поверхостный обзор придуманных положений несуществующей теории.
    
    Статья демонстрирует не просто высокий уровень наукообразной демагогии, по моему это, определенно, талант!
    
    Можете ответить на вопрос когда, где и кем была сформулирована "Теория типов"?
    
    или
    
    какой смысл проводить
    
    популярный поверхностный обзор известных положений теории
    
    если они известны?
    
    Кстати, словосочетание "популярный поверхностный обзор" вполне можно использовать как определение "демагогии", как мне кажется.

speshuric
02.09.2023 15:05
#25929694
В компьютере восьми-байтовая ячейка памяти может хранить в себе значения как из множества Int64, так и из double - эти множества имеют одинаковую мощность...

Не совсем. В классическом double двоичное представление NaN-значения не уникально.
1. Underskyer1 Автор
  02.09.2023 15:05
  #25929762
  Там речь шла о том, что и `Int64`, и `double` занимает в памяти 8 байт, и каждое сочетание бит там может интерпретироваться как корректное значение любого из этих типов. Разные NaNы также являются корректными в том смысле, что их можно использовать во всех операциях (результатом как правило будут также NaNы, но это уже на важно).
  1. speshuric
    02.09.2023 15:05
    #25929934
    +1
    Конечно, двоичных представлений наборов из 8 байт одно и то же количество (2^64) и можно между этими двоичными представлениями создать (тривиальную) биекцию. Но дальше начинается скользкое поле "что является одним и тем же значением". В принципе, если пользоваться totalOrder IEEE 754 и сделать на основе его отношение эквивалентности, то значений действительно 2^64, но все другие способы сравнения значений дают меньше значений, чем 2^64. Правда с оговоркой, что в большинстве этих "других способов сравнения" результат этого сравнения NaN и NaN даёт false (т. е. математически это не является симметричным, а значит не является отношением эквивалентности). А в прикладном ПО totalOrder IEEE 754 фактически не используется.
    
    Короче, я бы поостерёгся писать, что они равномощны, потому что это сильно зависит от контекста и деталей реализации (полнота поддержки IEEE 754 - тоже одна из таких деталей).
    
    Underskyer1 Автор
    02.09.2023 15:05
    #25929976
    Понял, о чём вы. Сложно рассуждать о мощности множества значений типа double, когда некоторые из значений могут оказаться не равны сами себе))
    
    Буду за компом - посмотрю, можно ли переписать это место корректнее. Спасибо!

ebt
02.09.2023 15:05
#25930326
Очень примечательно: по-видимому, из соответствия Карри-Ховарда следует, что любая сколь угодно сложная логика (темпоральная, немонотонная) представима в виде теории типов. А ещё любой современный компилятор, скажем, Rust, также является продвинутой системой доказательств, т.е. ризонером для очень выразительных логических вычислений.
1. anonymous
  02.09.2023 15:05
  #25930474
  НЛО прилетело и опубликовало эту надпись здесь
1. Underskyer1 Автор
  02.09.2023 15:05
  #25930548
  +1
  К сожалению, не хватает компетенции, чтобы ответить за все системы логики, но теория типов разрабатывалась для самого обоснования математики, чтобы была возможность проверить, корректны ли рассуждения в этом весьма гибком формализме, или нет. Конструктивная теория типов привнесла существенные выразительные возможности, а HoTT вообше претендует на звание фундамента всей математики. Теория категорий зародилась как обобщение теории типов, но и её саму можно выразить с помощью типов!
  
  Дейстаительно, инструмены статической типизации отвечают за доказательство корректности программы. Вот только во многих языках они.. "альтернативно продвинутые")). Например, при слабой системе вывода типов случаются ложноотрицательные вердикты, а изменяемые переменные приводят к ложноположительным и т.п.
  
  В Scala достаточно мощная система типов, в сравнении с Java, C# и т.п., но до каких нибудь Coq или Agda ему далеко...

Теория типов +58

Содержание

Предисловие

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

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

Множества

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

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

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

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

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

Сумма типов

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

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

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

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

Изоморфизм

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

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

Единица

Ноль

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

Тип множеств

Типы и классы

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

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

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

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

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

Типизация

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

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

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

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

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

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

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

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

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

Заключение

Комментарии (67)

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор

Underskyer1 Автор