Привет, Хабр! Меня зовут Глеб, я Java-разработчик в Сбере. Сегодня я хочу рассказать про исторический контекст двух фундаментальных подходов к системе типов в программировании.

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

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

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

Зарождение. 1930-1950 годы

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

Однако первое отклонение от такого подхода внёс американский математик Алонзо Чёрч, проживший аж целых 92 года, с 1903 по 1995.

Так вот, Чёрч придумал лямбда-исчисление — систему для формализации понятия вычислимости. Тема сама по себе математическая, однако в ней нас интересует подход:

• Все элементы (термы) системы — это функции от одной переменной. Функции не имеют имени.

• Терм можно применять к любому другому терму без ограничений.

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

Однако в системе лямбда-исчисления (нетипизированной) возможны сценарии её парадоксального использования, например, рекурсивная аппликация терма к самому себе. Простая аналогия — парадокс лжеца: «это предложение ложно». Применяя утверждение к самому себе, мы ни к чему не приходим.

В связи с этим, из своей системы Алонзо в 1940 году вывел систему просто типизированного лямбда-исчисления (STLC, Simply typed lambda calculus), накладывающую некоторые ограничения на аппликацию (применение функции к её аргументу) термов. Основные правила STLC:

• Каждому терму приписывается тип.

• Применение друг к другу термов с несовместимыми типами невозможно.

• Все вычисления обязательно должны завершаться.

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

Далее на сцене появились ещё два американских математика: Хаскелл Карри и Уильям Говард, которые предложили идею «соответствия Карри-Говарда». Она гласит: типы в программах можно воспринимать как логические утверждения, а программы — как доказательства этих утверждений.

Wiki: «Более неформально это можно рассматривать как аналогию, которая утверждает, что возвращаемый тип функции (т. е. тип значений, возвращаемых функцией) аналогичен логической теореме с учетом гипотез, соответствующих типам значений аргументов, передаваемых функции; и что программа для вычисления этой функции аналогична доказательству этой теоремы.»

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

Тип данных в программе — это определённое утверждение. А если программа скомпилировалась, то мы строим доказательство, что это утверждение истинно.

Да, всё вышеописанное достаточно абстрактно, поскольку мы пока что рассматриваем именно математические корни типизации. Не переживайте, скоро мы перейдём к более понятным вещам. Кстати, известный язык программирования Haskell назвали в честь вышеупомянутого Хаскелла Карри. Поскольку язык является функциональным, в 1990 году комитет назвал его «Haskell» в благодарность за вклад Карри в теорию типов и функционального программирования (Говард и Чёрч в этом вопросе оказались обделены языками программирования, названными в их честь).

Динамическая типизация. 1950-1960 годы

Lisp

В 1958 году появился Lisp — динамически типизированный язык, разработанный Джоном Маккарти. Этот язык вводит радикальную идею: «код как данные». Программы в Lisp записывают в виде символьных списков (S-выражений в терминологии Lisp). Этими же S-выражениями представляются и сами данные! Поэтому в этом языке стирается грань между операциями над данными и операциями над другой программой.

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

Значения в этом языке носят типы, однако тип не объявляется вместе с переменной, а совместимость типов проверяется при выполнении операций — в случае несоответствия мы получим run-time ошибку. Для чего Джон Маккарти так сделал?

Как уже говорилось, Маккарти проектировал язык для исследований в области ИИ (в 1958 году!). Для этого нужно было быстро прототипировать идеи, работать с языком в интерактивном режиме и манипулировать большим количеством типов данных.

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

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

Позже в Common Lisp появились опциональные декларирования типов и компиляторные подсказки, однако фундамент языка и идея «код как данные» сохранились.

Lisp можно считать первым общедоступным формализованным языком программирования с динамической типизацией. Да, у него был предшественник — язык IPL, появившийся в 1956 году, который тоже использовали для исследований в области ИИ, однако он имел более узкую область применения и экспериментальный статус.

Разумеется, IPL и Lisp были не единственными подобными языками. В 1950-1970 годах вместе с ними возник целый класс интерпретируемых, интерактивных и слаботипизированных языков, спроектированных для быстрой разработки, исследовательских задач (ИИ, лингвистика, математические расчёты) и манипуляций над разными типами данных.

Достойны упоминания:

• COMIT (1957), SNOBOL (1962) — языки для обработки строк, шаблонов и решения задач машинного перевода.

• APL (идея в 1962, первая реализация в 1965) — язык предоставлял компактную нотацию для операций над массивами. Был ориентирован на интерактивную работу с матрицами/векторами.

• JOSS (1963), BASIC (1964) — простые для новичков, интерактивные языки, нацеленные на быстрое написание программ с помощью несложного (по тем временам) синтаксиса.

• Forth (1970) — стек-ориентированный язык, использовался на практике для управления аппаратурой оборудованием — например, с его помощью управляли радиотелескопами NRAO и Kitt Peak.

Новые идеи статической типизации 1960-1970 годов

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

Кристофер Стрейчи был одним из пионеров теории языков программирования. Его лекции Fundamental Concepts in Programming Languages (1967) ввели в обиход множество терминов, до сих пор активно используемых сообществом. В этих лекциях Стрейчи уделял особое внимание концепции полиморфизма — до сегодняшних дней дошли практически все его идеи в этой области.

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

Стрейчи разделял полиморфизм на два вида:

• Ad-hoc полиморфизм, когда одна операция (внешне) способна работать с разными типами, однако на самом деле эта операция представлена множеством различных реализаций. Например, операцию сложения можно определить для различных видов данных. Пример на Kotlin:

  data class Vec(val x: Float, val y: Float) {
      operator fun plus(v: Vec) = Vec(x + v.x, y + v.y)
  }
  data class User(val login: String) {}
  
  fun main() {
    val n = 1+2
    val s = "Hello,"+"world"
    val v = Vec(2f, 3f) + Vec(4f, 1f)
    val u = User(“user1”) + User(“user2”) //compile error here
  }

  Однако, как видно из примера, такой полиморфизм не совсем «настоящий»: сама по себе операция сложения применима не к любому типу, а только к тем, для которых она переопределена.

• Параметрический полиморфизм — это способность функции работать одинаково для любых типов (и при этом быть написанной один раз). Такой полиморфизм является как бы «настоящим», ведь поведение функции совсем не зависит от конкретного типа. В качестве примера можно привести функцию на Java:

  public <T> T justReturn(T t){
      return t;
  }

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

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

Таким образом, параметрический полиморфизм стал теоретическим базисом для дальнейших формальных систем типов: он позволил описать обобщённые (generic) функции, а Ad-hoc полиморфизм породил практики перегрузки операторов и функций, которые со временем крепко закрепились в различных реализациях объектно-ориентированных и функциональных языков.

Закрепление парадигмы статической типизации

Важно понимать, что развитие системы типов шло рука об руку с развитием языков программирования. Одним из важнейших прародителей можно назвать ALGOL — семейство императивных языков, появившееся на свет в 1958. Сейчас можно сказать, что синтаксис большинства современных языков является «алголоподобным». Идеи, введённые этим семейством, получили широкое распространение. Среди них:

• Блоки кода и их разграничения.

• Вложенность и лексическая область действия функций.

• Формальное определение языка программирования (в отчёте Algol 60 язык описан по форме Бэкуса-Наура).

К ALGOL приложили руку:

• Джон Бэкус и Питер Наур (создавшие вышеупомянутую формальную грамматическую нотацию для документирования языка);

• Джон Маккарти (уже известный нам по языку Lisp);

• Джозеф Уэгстен (который в будущем возглавил комитет, разрабатывавший COBOL);

• Эдсгер Дейкстра (будущий лауреат премии Тьюринга) и многие другие.

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

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

Впервые эти ограничения сформулировали в 1974 году Барбара Лисков и Стивен Зиллес в своей работе по созданию языка Clu (Клу): сильно типизированные языки на этапе компиляции гарантируют, что при передаче объекта из вызывающей функции в вызываемую тип этого объекта должен быть совместим с типом, определённым в вызываемой функции.

Другое определение дал итальянский учёный Лука Карделли: система типов называется «сильной», если она исключает возможность возникновения ошибки согласования типов во время выполнения.

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

Pascal стал логическим преемником идей Алгола: Николаус Вирт спроектировал Pascal как язык с ясной, декларативной системой типов и средствами для явного описания структур данных (записи, массивы, перечисления, поддиапазоны и т. д.).

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

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

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

Вывод типов

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

Вот пример кода на современном Rust:

let my_arg = 1;
let my_arg = "  ";

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

Большой вклад в алгоритмы автоматического выведения типов внёс английский ученый Робин Милнер (1934-2010). Вот оригинал статьи и её перевод, где это объяснено подробно. А здесь я приведу лишь небольшой кусочек.

Итак, как же алгоритм Хинли-Милнера предлагает выводить типы?

Начнём с наглядной аналогии. У нас есть несколько фактов:

• Маша высокая.

• Вася высокий.

• Маша любит красный.

• Вася любит синий.

Также у нас есть набор ограничений:

• Некто высок.

• Некто любит красный.

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

• У нас есть городские жители и деревенские.

• Городские жители любят бетон и пряники.

• Деревенские жители не любят ни бетон, ни пряники.

• Маша любит бетон.

• Вася любит пряники.

• Петя не любит бетон.

...и будем искать того, кто удовлетворяет следующему ограничению:

• Некто любит пряники.

...то мы не сможем сказать, кто это будет конкретно. И вообще, мы можем сказать только одно: некто — городской житель.

Таким образом, если есть функция (псеводкод):

fn my_function(person){
    person.eatPryanik();
}

...то компилятор догадается, что функция принимает на вход только городских жителей, и превратит это в:

fn my_function(person: CityResident){
    person.eatPryanik();
}

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

Алгоритм Хиндли-Милнера использовали (и используют) в таких языках, как ML, Haskell, OCaml. Cвоим удобством и понятной идеей он повлиял на огромное количество других языков программирования, и послужил толчком для создания множества алгоритмов автоматического выведения типов.

Стоит также уточнить, что работа Милнера была как бы продолжением первоначальной работы Роджера Хинли. В дальнейшем предложенную Хиндли и развитую Милнером систему типов формализовал и доказал Луис Дамас в своей докторской диссертации, в связи с чем её зачастую называют системой типов Дамас-Хиндли-Милнера.

Вторая волна популярности динамических языков

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

1. Приход программирования в массы. Теперь ему учили в школах (в школах СССР, например, программирование преподавали с 1985 года, в рамках обязательного предмета «Основы информатики и вычислительной техники»). Нужны были простые и наглядные языки с низким порогом входа.

   Сравните код на языке Си:

   #include <stdio.h>
   
   int main() {
       printf("Hello World!\n");
       return 0;
   }

   С кодом на Python:

   print("Hello, World!")

   Или Ruby:

   puts "Hello World"

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

   Например, на Python можно сделать что-то вроде:

   import json
   
   payload = '{"name":"Ivan","age":30,"tags": ["test"]}'
   
   data = json.loads(payload)
   name = data.get('name', 'guest')
   age = data.get('age')
   tags = data.get('tags', [])
   print(f"name = {name}, age = {age}, tags = {tags}")

   Теперь приблизительно такой же код на С++:

   #include <iostream>
   #include <fstream>
   #include <string>
   #include <nlohmann/json.hpp>
   
   using json = nlohmann::json;
   
   int main() {
       std::string input((std::istreambuf_iterator < char > (std::cin)),
           std::istreambuf_iterator < char > ());
     
       try {
           auto data = json::parse(input);
           std::string name = data.value("name", "guest");
           int age = data.value("age", -1);
           if (data.contains("tags") && data["tags"].is_array()) {
               for (const auto& t: data["tags"]) {
                   std::cout << "tag: " << t.get < std::string > () << "\n";
               }
           }
           std::cout << "name=" << name << ", age=" << age << "\n";
       } catch (const json::parse_error& e) {
           std::cerr << "parse error: " << e.what() << "\n";
           return 1;
       } catch (const json::type_error& e) {
           std::cerr << "type error: " << e.what() << "\n";
           return 2;
       }
       return 0;
   }

3. Появление фреймворков, сводящих к минимуму недостатки динамически типизированных языков, сохраняя и преумножая все их преимущества. Например, Rails, который дал новую жизнь Ruby, Django для Python и т. д.

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

   Также массово начали распространятся линтеры и умные IDE, указывающие разработчикам на ошибки несоответствия типов ещё до run-time. Разумеется, это не устраняло все проблемы динамической типизации, однако сильно упрощало жизнь рядовым разработчикам.

Наши дни

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

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

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

Подобные инициативы возникли и в Python (mypy, typing), и в Ruby (sorbet), и во многих других динамических ЯП. Динамические языки от такой надстройки не теряют своей гибкости, однако позволяют пользоваться возможностью строгих проверок там, где они действительно нужны.

Немного в стороне стоит Python — его продолжающийся рост популярности можно объяснить новыми тенденциями в развитии ИИ: для обучения моделей необходимо экспериментировать и проверять гипотезы, а Python и прост в синтаксисе, и имеет высокопроизводительные вычислительные библиотеки, такие так NymPy, Pandas, TensorFlow, PyTorch. Но что ещё важнее, он имеет под собой экосистему удобной интеграции этих инструментов в реальные проекты, и огромное сообщество. Python в сфере ML идеально закрыл путь от идеи до эксперимента.

 

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

Спасибо за внимание!