Часто задаваемые вопросы о системах типов

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

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

Динамическая типизация и отсутствие типизации

Некоторые люди считают, что динамическая система типов (dynamic type system) — это то же самое, что и система типов с отсутствием типизации (untyped type system). Отсутствие типизации означает, что в некоей системе типов нет смысла различать типы. Нет смысла различать типы и в том случае, если в системе типов присутствует всего один тип. Например:

• В ассемблере единственный тип — строка битов.
• В лямбда-исчислении единственный тип — функция.

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

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

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

_{«Системы типов для языков программирования», Бенджамин Пирс}

Динамическая и статическая типизация

Динамическая система типов (dynamic type system) — это такая система, в которой типы проверяются динамически (во время исполнения программы). Статическая система типов (static type system) — это система, в которой типы проверяются статически (во время компиляции или транспиляции кода).

Является ли одна из этих систем противоположностью другой? Нет, не является. В одном и том же языке могут применяться обе эти системы типов. На самом деле, в большинстве статических систем типов имеются и динамические проверки типов. В качестве примера можно рассмотреть валидацию операций ввода-вывода (input-output, IO). Представьте себе, что вам нужно прочитать данные, предоставленные пользователем, который должен ввести число. Вы будете проверять, во время исполнения программы, является ли число результатом разбора соответствующей строки (в результате разбора может быть выдано исключение или возвращено нечто вроде NaN). Когда вы проверяете введённые пользователем данные, выясняя, могут ли они рассматриваться как число — вы выполняете динамическую проверку типа.

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

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

Рекомендуется рассматривать статическую систему типов как типы, проверяемые статически. А динамическую систему типов — как типы, проверяемые динамически.

Означает ли применение статических типов знание типов во время компиляции программы?

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

let x = "test";

Оказывается, что парсер знает о том, что "test" — это строка. Делает ли это JavaScript языком со статической типизацией? Нет, не делает.

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

Система типов с постепенной типизацией (gradual type system) — это статическая система типов, которая позволяет пропускать проверки типов для некоторых частей программы. Например — в TypeScript подобное реализуется с помощью any или @ts-ignore.

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

Надёжные и ненадёжные системы типов

При использовании надёжной системы типов (sound type system) программа, в ходе проверки типов, не будет «одобрена» в том случае, если в этой программе есть ошибки, связанные с типами. Применение ненадёжной системы типов (unsound type system) приводит к тому, что в программе могут присутствовать ошибки, связанные с типами. Не следует, правда, впадать в панику после того, как вы об этом узнали. На практике это может вас не коснуться. Надёжность или корректность (soundness) — это математическое свойство алгоритма проверки типов, которое нуждается в доказательстве. Множество существующих компиляторов (внутри это — системы проверки типов) ненадёжны.

Если вы хотите работать с надёжными системами типов — взгляните на языки программирования семейства ML, в которых используется система типов Хиндли-Милнера (Hindley-Milner).

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

Система типов, которая никогда не отвергает правильные программы, называется полной (complete).

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

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

Я считаю нецелесообразным использование терминов «слабая типизация» (weak typing) и «сильная типизация» (strong typing). Эти термины неоднозначны, их применение может дать больше путаницы, чем ясности. Приведу несколько цитат.

Эти языки могут называться, образно говоря, языками со слабой проверкой типов (или слабо типизированными языками, как их обычно называют в различных публикациях). Использование в языке слабой проверки типов означает, что некоторые небезопасные операции выявляются статически, а некоторые — нет. «Слабость» проверок типов в языках этого класса серьёзно варьируется.
_{«Системы типов», Лука Карделли}

Вероятно, самым распространённым способом классификации систем типов является их разделение на системы со «слабой» и «сильной» типизацией. Об этом можно лишь сожалеть, так как данные слова не несут в себе практически никакого смысла. Можно, в ограниченных пределах, сравнивать два языка, имеющих очень похожие системы типов, и выделять один из них, как имеющий более сильную, чем второй, систему типов. В других случаях термины «сильная типизация» и «слабая типизация» совершенно не имеют смысла.
_{«Что надо знать до начала обсуждения систем типов», Стив Клабник}

_{«Типы», Гэри Бернар}

Нуждаются ли языки со статической типизацией в объявлениях типов?

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

const x = "test";

Система типов знает о том, что "test" — это строка (это знание основано на правилах парсинга кода). Система типов знает и о том, что x — это константа, то есть — значение x нельзя переназначить. В результате может быть сделан вывод о том, что x имеет строковой тип.
Вот ещё один пример (Flow):

const add = (x, y) => x / y
//                        ^ Невозможно выполнить арифметическую операцию так как строка [1] не является числом.
add(1, "2")

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

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

Является ли TypeScript небезопасным языком из-за того, что код, написанный на нём, компилируется в JavaScript-код?

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

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

Тут, если вернуться к мысли о небезопасности TS из-за компиляции в JS, у вас может появиться следующая мысль: «Скомпилированный код выполняется в браузере, JS — язык небезопасный, и в то место, где ожидается строка, он вполне может подставить значение null». Мысль это дельная. Но это, опять же, не даёт повода называть TS небезопасным языком. Для того чтобы TS мог гарантировать безопасность внутри приложения, вам нужно разместить «защитные механизмы» в тех местах, где TS-код взаимодействует с внешним миром. То есть, например, нужно проверять корректность данных, поступающих в программу через механизмы ввода-вывода. Скажем, это может быть проверка того, что вводит пользователь, проверка ответов сервера, проверка данных, читаемых из хранилища браузера и так далее.

Например, роль подобных «защитных механизмов» в Elm играют «порты». В TS для этого можно использовать нечто вроде io-ts.

Соответствующий «защитный механизм» создаёт мост между статической и динамической системами типов.

Вот упрощённый пример:

const makeSureIsNumber = (x: any) => {
  const result = parseFloat(x);
  if (isNaN(result)) {
    throw Error("Not a number");
  }
  return result;
}
const read = (input: any) => {
  try {
    const n = makeSureIsNumber(input);
    // в этой ветке кода n, безусловно, является числом
    // в противном случае мы попали бы в другую ветку кода
    // makeSureIsNumber "гарантирует" то,что n является числом
  } catch (e) { }
}

Правда ли то, что типы нужны лишь для компиляторов?

Типы — это всего лишь хак, нужный для того, чтобы давать подсказки компилятору.
_{Ваут Мертенс}

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

Феномен типов существует из-за людей. Типов не существует до тех пор, пока человек не воспринимает нечто в виде «типа данных». Человеческий разум распределяет разные сущности по разным категориям. Типы не имеют смысла без наблюдателя.

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

• «Живая» ячейка, у которой меньше двух «живых» соседей, «умирает», как при низкой плотности населения.
• «Живая» ячейка, имеющая два или три «живых» соседа, выживает, и попадает в следующее поколение.
• «Живая» ячейка, у которой больше трёх «живых» соседей, «умирает», как при перенаселённости.
• «Мёртвая» ячейка, у которой имеется ровно три «живых» соседа, становится «живой», как при воспроизводстве населения.

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

Если какое-то время понаблюдать за «Жизнью», то на поле могут появиться устойчивые структуры наподобие «планера» («glider»).

«Планер»

Видите его? По экрану движется «планер». Правда? А теперь давайте немного притормозим. Существует ли этот «планер» на самом деле? Это — просто отдельные квадраты, которые появляются и исчезают. Но наш мозг может воспринимать эту структуру как нечто, объективно существующее.

Мы, кроме того, можем сказать, что «планер» существует из-за того, что квадраты не являются независимыми (они зависят от соседей), и даже если сам по себе «планер» и не существует, то существует «планер» в виде платонической идеи.

Итоги

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

Уважаемые читатели! Как вы думаете, какая система типов могла бы считаться идеальной для целей веб-разработки?

Автор: ru_vds

Источник