Хабрахабр

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

Автор статьи, перевод которой мы сегодня публикуем, говорит, что источником вдохновения для её написания послужил этот пост и комментарии к нему. По его словам, 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). Эти термины неоднозначны, их применение может дать больше путаницы, чем ясности. Приведу несколько цитат.

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

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

Вот несколько примеров их использования: Термины «сильная типизация» и «слабая типизация» чрезвычайно неоднозначны.

  • Иногда под «сильной типизацией» понимают «статическую типизацию». Такую «подмену» произвести несложно, но лучше, говоря о статической типизации, просто называть её «статической». Дело в том, что большинство программистов вполне однозначно понимают этот термин.
  • Иногда, говоря «сильная типизация», имеют в виду «отсутствие неявного преобразования типов». Например, в JavaScript можно использовать выражения вроде "a" - 1. Это можно назвать образцом «слабой типизации». Но почти все языки дают программисту некие возможности по неявному преобразованию типов, например, поддерживая автоматическое преобразование целых чисел в числа с плавающей точкой в выражениях наподобие 1 - 1.1. На практике большинство специалистов, использующих подобным образом термин «сильная типизация», разграничивают «приемлемые» и «неприемлемые» преобразования типов. Но общепринятой границы между подобными преобразованиями типов не существует. «Приемлемость» и «неприемлемость» преобразований — это субъективная оценка, зависящая от мнения конкретного человека.
  • Иногда языками с «сильной типизацией» называют те языки, в которых никак нельзя обойти правила имеющейся в них системы типов.
  • Иногда «сильная типизация» означает наличие системы типов, которая позволяет безопасно работать с памятью. Язык C — это заметный пример языка, который небезопасно работает с памятью. Например, если xs — это массив из четырёх чисел — C без проблем одобрит код, в котором используются конструкции наподобие xs[5] или xs[1000]. Они позволят обратиться к памяти, которая находится после адресов, выделенных на хранение содержимого массива xs.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

«Планер»

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

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

Итоги

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

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

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть