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

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

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

Лука Карделли и типовая безопасность

«Основная цель системы типов - предотвратить возникновение ошибок выполнения во время выполнения программы. Это неформальное утверждение мотивирует изучение систем типов, но требует пояснения. Его точность зависит, прежде всего, от довольно тонкого вопроса о том, что является ошибкой выполнения ».

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

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

Теперь строго проверенная программа имеет следующие свойства:

  • Никаких невыявленных ошибок не возникает (безопасность)
  • перехваченных ошибок, относящихся к запрещенным ошибкам, не возникает.
  • Могут возникнуть другие перехваченные ошибки

Наконец, он исследует роль набора текста:

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

Что касается так называемых «нетипизированных языков», он указывает, что:

«У них нет типов или, что то же самое, есть один универсальный тип, содержащий все значения. […] Нетипизированные языки могут обеспечивать хорошее поведение (включая безопасность) другим способом, выполняя достаточно подробные проверки времени выполнения, чтобы исключить все запрещенные ошибки. Процесс проверки на этих языках называется динамической проверкой […] Большинство нетипизированных языков по необходимости полностью безопасны ».

Наконец, он различает «строго проверенные» и «слабо проверенные» языки:

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

Обсуждение

Определения Карделли, кажется, улавливают большую часть интуиции о безопасности и помогают соответствующим образом классифицировать и сравнивать языки. С его точки зрения, мы можем отличать такие языки, как Python, от C как нетипизированные / динамически проверенные и типизированные / статически проверенные соответственно. Мы также можем различать статически проверенные языки, такие как C, от ML как слабо проверенные и строго проверенные соответственно.

Он отмечает, что в группе «нетипизированных языков» мы можем рассматривать их в равной степени как «единые», и, поскольку тип «универсальный тип» проверяет все операции, эти языки также хорошо типизированы. Другими словами, теоретически в программах, написанных на этих языках, нет запрещенных ошибок ( т.е. ошибок типа ). Что правильно, но в то же время вызывает вопросы. Например, как мы должны рассматривать исключения TypeError в Python?

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

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

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

Бенджамин С. Пирс и безопасность шрифтов

В своем Типах и языках программирования (основной учебник по этому предмету) Бенджамин Пирс пишет:

Самым основным свойством [системы типов] является безопасность (также называемая надежностью): хорошо напечатанные термины не «ошибаются»: […] это означает достижение «Застрявшее состояние», которое не обозначено как окончательное значение, но в котором правила оценки не говорят нам, что делать дальше.

В контексте лямбда-исчисления он предлагает следующую формализацию «застрявшего состояния»:

Закрытый термин застрял, если он имеет нормальную форму, но не имеет значения.

имея в виду следующие определения:

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

Затем он предлагает определение хорошо типизированного термина с помощью двух теорем:

Прогресс: хорошо набранный термин не застрял.
Сохранение: если хорошо набранный термин проходит этап оценки, то полученный термин также хорошо набрал.

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

Обсуждение

Чтобы применить эти определения, рассмотрим простой логический язык (BOOL) ниже:

В грамматике BOOL (как BNF) мы определили, что такое термин (т. Е. Что составляет программу; «точка входа» синтаксического анализа) и что такое значение ( как указано выше, это условия, которые могут быть окончательным результатом оценки). На этом языке мы можем писать такие программы, как true, false, and(true, false), and(false, and(true, true)) и т. Д. Мы оцениваем программы, используя правила оценки STEP-T, STEP-F и STEP-A, , где t обозначает переменную, диапазон которой превышает термины. Ниже приведены примеры оценок программ (сокращения в нормальном порядке, т.е. слева направо):

Мы могли бы расширить наш язык BOOL типами, используя следующие правила:

Что касается обоснованности, должно быть ясно, что все значения хорошо типизированы, как и все термины. Таким образом, ошибки в синтаксически правильных программах невозможны. Теперь рассмотрим следующее (частичное) расширение языка, где разрешены целые числа. Назовем этот язык BOOL-I:

С этим расширением, хотя все предыдущие программы по-прежнему действительны, а также такие программы, как -1 и 99, мы можем писать программы, которые зависают, например: and(2, false). Эта программа неверно типизирована в соответствии с определением Пирса, и это правильно.

Интересно, что есть еще один способ моделирования ошибок типа. Далее Пирс предлагает изменить язык, чтобы обозначить «застрявшее состояние» как термин, например error term, чтобы указать, что это «застрявшее состояние» достигнуто. При таком подходе мы можем переписать язык BOOL-I, добавив error термин и добавив правило оценки, чтобы «всплыть наверх» во время оценки. Назовем этот язык БУЛ-Т.е.

В соответствии с BOOL-Ie, and(2, false) оценивается как error. Таким образом, мы представляем это «застрявшее состояние» (невозможность выполнения) как данные, возвращаемые в программу, что позволяет им продолжить оценку.

Однако, похоже, этим мы снова пригласили ту старую головоломку.

если ошибки оценки становятся значениями, остаются ли они ошибками? Если да, то в каком смысле?

Теперь мы можем сказать, что оба языка, BOOL-I и BOOL-Ie, эквивалентны, если мы рассматриваем error «особый» термин, указывающий на ошибку типа. это так, поскольку error не является значением. Если мы рассматриваем error как значение, тогда and(2, false) хорошо типизирован. Давайте рассмотрим эти две альтернативы более подробно:

“error” как ошибка типа

На языке BOOL-Ie, поскольку error не является значением, но находится в нормальной форме (т. Е. Для него нет шагов оценки), то, по определению, это плохой -типированный термин. Он просто действует как заполнитель, обозначающий возникновение type-error, устройства, используемого в нашем семантическом аппарате. То есть error является ошибкой типа с «семантической точки зрения», а не какой-либо ценностью, заслуживающей рассмотрения с «точки зрения пользователя». Тогда мы могли бы разумно сказать, что тип функции по-прежнему:

“error ”как обычное значение

Альтернативный вариант - рассматривать error как значение, как и любое другое. То есть значение, которое принадлежит типу (например, Error), значение, которое может быть вычислено для получения других типов значений. Мы делаем это, перемещая error в грамматике к продукту value и определяя его тип. В результате error не является ошибкой типа согласно нашим определениям. Таким образом, программа and(2, false) хорошо типизирована и возвращает обычное значение, которое оказывается равным error (то же самое, что и возврат _27 _, _ 28_, IOException()… в популярных языках программирования). Следовательно, and можно оценивать с помощью логических, целых чисел и error значений и возвращать логические значения или error. Итак, тип и будет примерно таким:

… Или, возможно, как полиморфная функция, где T, U и V - переменные типа :

… Или, тем не менее, мы могли бы ввести подтипирование и сказать, что это функция «от чего угодно к чему угодно»: это «нетипизировано» или «объединено»:

В любом случае важно отметить, что потребуется лишь небольшое изменение языка, чтобы программа t могла вычислить нормальный термин x ≠ error, даже если t содержит термины, которые в какой-то момент оцениваются как error (в другими словами, программа может «обработать» error и продолжить работу в обычном режиме - таким образом, error может действовать как значение исключения).

Следовательно, было бы противоречием рассматривать появление определенного типизированного значения error как ошибку типа. Во-первых, поскольку ошибка типа определяется как «застрявшее состояние» на этапах оценки, и если error - значение, которое можно использовать в программе, даже до некоторой степени оно становится «незакрепленным» , то это не может быть ошибкой типа. Во-вторых, если error - это значение, подобное любому другому, принадлежащему типу, то любая функция типа f: Error, возвращающая значение error типа Error, явно хорошо типизирована. Тогда что это за ошибка error, если не ошибка типа?

Заключение

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

Таким образом, мы увидели, что:

  • «Нетипизированные языки» могут показывать «типовые ошибки». И все же они созданы таким образом, что их программы по своей сути типобезопасны.
  • «Статически проверенные» программы гарантированно не проявляют произвольного поведения. И все же, возможно, они все еще могут вести себя произвольно.
  • Точное определение безопасности типов зависит от точного определения type-error.
  • Когда ошибки типа вводятся в язык как значения, даже несмотря на то, что определенная концепция ошибки типа может быть строго определена, она не может удовлетворительно уловить явления, которые мы рассматриваем как «ошибки типа». Таким образом, значение слова «ошибка типа» размывается.
  • Популярное представление о том, что «безопасность типов гарантирует, что программы не содержат ошибок типа», может вводить в заблуждение и может быть поставлено под сомнение, поскольку программы с ошибками типа могут быть переписаны, чтобы получить значение, которое представляет собой именно возникновение ошибки. . Таким образом, можно сказать, что ошибка все еще существует и все еще происходит, она просто стала вычислимой и типобезопасной.

¹ Для полноты может потребоваться несколько дополнительных правил набора текста, но это несущественно для обсуждения.

Хотя эти два текста кажутся довольно популярными (в частности, книга Пирса - это учебник по« PLT-ориентированной теории типов), я не проводил гораздо более широкого поиска. За исключением Практических основ языков программирования Боба Харпера, трактовка которых, похоже, аналогична трактовке Пирса, это лучшие трактовки предмета, о которых я знаю.