Известный "кризис оснований математики", который произошел в начале XX века. Возник он из-за (или благодаря, тут трудно сказать) "Наивной теории множеств" Георга Кантора, которая на первый взгляд должна была стать точкой сбора всех математиков. Все мы, особенно разработчики, интуитивно понимаем теорию множеств. Например, вот множество натуральных чисел {1,2,3...}, а вот множество целых чисел {..., -1, 0, 1...}. Можно заметить, что множество целых чисел включает в себя множество натуральных чисел. Так что разность этих множеств (Z \ N) будет множество всех отрицательных целых чисел и нуля: {..., -1, 0}. Теория множеств является основой для реляционной алгебры, а значит он будет знаком каждому, кто работал с SQL. Но в наивной теории множеств были серьезные белые пятна, которые приводили к нарастающим год за год парадоксам. Самые известные - парадоксы Рассела, и одна из них сформулирована в виде парадокса брадобрея:
Пусть в некой деревне живёт брадобрей, который бреет всех жителей деревни, которые не бреются сами, и только их. Бреет ли брадобрей сам себя?
Bertrand Russel
Вместо множеств, которые могли включать в себя любые объекты, в том числе и себя, английский философ и логик Бертран Рассел предложил делить их по типам. Типы находились на разных уровнях и тип большего порядка включал в себя только типы меньшего порядка, поэтому это решило парадоксы. Но как я уже писал в предыдущем посте, работы Рассела оказались слишком непрактичными и не получили поддержки математического сообщества.
В 30-х годах XX века американский математик Алонзо Черч (учитель Алана Тьюринга) придумал очень мощную формальную систему под названием "Лямбда-исчисление" (Lambda calculus). Что такое "лямбда-исчисление" мы будем исследовать отдельно, потому что тема невероятно интересная и обширная. Но для понимания, та система, которую придумал Черч была бестиповой. Это сново привело к различным парадоксам в духе парадоксов Рассела (парадокс Клини-Россера). Чтобы спасти свое детище, Черч тоже обратился к типам и придумал "Просто типизированное лямбда-исчисление" (STLC). Почему "Просто типизированное"? Ну, чтобы никто не испугался из-за ассоциаций с теорией типов Рассела. Именно связка типов с лямбда-исчислением поспособствовала к дальнейшему развитию теории типов.
Название "Теория типов" очень обманчивое, потому что оно подразумевает, что это одна общая теория. На самом деле нет единой теории типов, есть множество теорий и два я уже упомянул (разветвленная теория типов Рассела и просто типизированное лямбда-исчисление Черча). Также может показаться, что теория типов изучает типы. Но, к удивлению, не существует общего определения понятия "тип". Долгое время математики понимали его интуитивно, как мы программисты, когда говорим, что тип - это "множество значений и операций над этими значениями". По предыдущим историям можно проследить, что математики изначально вводили типы как защиту от логических ошибок в формальных системах. Но дальнейшее изучение типов дало понять, что логика и типы имеют более глубокую связь.
В тех же 30-х годах американец Хаскелл Карри (в честь которого назван язык программирования Haskell и термин "каррирование") обнаружил удивительное сходство между логикой и типизированной комбинаторной логикой, о чем он решил рассказать только через 20 лет спустя. Тогда мало кто обратил внимание на это совпадение, пока другой американский математик Уильям Ховард не доказал изоморфизм между упомянутым "Просто типизированным лямбда исчислением"(STLC) и интуиционистский логикой. Изоморфизм означает, что структурные элементы этих систем равнозначны:
Это означает, что любая типизированная вычислительная система эквивалентна логической системе и они работают одинаково. Тут внесу ясность, что логическая система используется для доказательств. Отсюда делаем вывод, что любое вычисление в типизированной системе то же самое, что и доказательство какой-либо теоремы. Ну и подставьте сюда вместо страшного слова "Типизированная вычислительная система" какой-нибудь язык программирования - смысл от этого не поменяется.
То что я описал выше известно как Соответствие Карри-Ховарда. И выводы из него повлияли и на математику (появились новые теории типов, т.к. теория типов Мартина-Лефа), и на программирование. Программисты поняли, что типы - это не просто способ разделять данные, но и способ целиком описать систему в терминах логики. По другому - создать спецификацию программы. Данная программа не будет содержать логических ошибок и противоречий, если она скомпилировалась. На этом принципе построены все современные системы автоматического доказательства, такие как Rocq, Agda и Lean.
Чтобы это все работало в языке программирования, нам нужно иметь язык с мощной системой типов. А, к сожалению, таких ЯП среди мейнстрима исторически было мало. Дело в том, что типы в языках программирования появились естественным образом. Вспомните, сперва были типы на аппаратном уровне (integers and floating-point numbers), потом появились простые системы типов как в языке Fortran или С. Все, что мы обсуждали развивалось за стенами университетов, а затем перекочевало в академические языки типа Haskell. Но в последнее десятилетие происходит явный тренд на идеи из Теории типов в мейнстриме. Начали появляться популярные языки с интересной системой типов как TypeScript, Kotlin и Rust (который основан на линейной и аффинной логике Жан-Ив Жирара). Но интереснее поговорить про то, что классические языки как Java, Python, C# тоже начали адаптировать идеи как из функционального программирования, так и из теории типов. Рассмотрим этот феномен в контексте Java, в современных версиях языка мы уже видим реализации этих концепций.
Вывод типов. Это когда нам компилятор разрешает не указывать тип каждого объекта, а использовать var. Но в Java реализован только локальный вывод типов. Самым продвинутым способом вывода типов является алгоритм Хиндли-Милнера и его мы можем видеть, например, в OCaml.
Алгебраические типы данных (ADT). Реализуется через структуры Record и sealed interface. Позволяет нам выполнять алгебру типов (как я уже говорил, как в логике), создавая более сложные типы.
Сопоставление с шаблоном (Pattern matching). Напрямую связан с ADT, так как позволяет выразить все состояния типа. Это помогает нам обработать все возможные сценарии через оператор switch. Данный принцип можно описать как "Make illegal states unrepresentable".
Очевидно, что Java заимствует все последние фичи от своих собратьев по JVM, таких как Scala и Kotlin, потому что их делали дядьки с более сильной академической базой. Но мне как человеку, которому интересна теория типов, неважно откуда они взялись в моем языке программирования, главное что мне это дает. А дает то, что обсуждали выше - систему, которую я могу описать через выразительную систему типов. Практически, язык с мощными типами позволит писать бизнес-логику через них, а также проверить ее корректность на этапе компиляции.
P.S. Теория типов зашагала далеко вперед практики, поэтому многие вещи нам еще предстоит увидеть в своих языках программирования. Одна из таких интересных идей - зависимые типы.
Они позволяют связывать типы со значениями. Например, сделать тип «массив фиксированной длины» или «число строго больше нуля», причем проверку компилятор выполнит статически. Немного такой магии уже можно видеть в TypeScript.
Top comments (0)