Категоризация систем типов (сильная / слабая, динамическая / статическая)

Вкратце: как системы типов классифицируются в академическом контексте; в частности, где я могу найти авторитетные источники, в которых четко различаются различные типы систем типов?

В некотором смысле, проблема в этом вопросе не в том, что я не могу найти ответ, а скорее в том, что я могу найти слишком много, и ни один не выделяется как правильный. Предпосылкой является то, что я пытаюсь улучшить статью на вики-странице Haskell о наборе текста , которая в настоящее время имеет следующие различия:

• Нет типизации: язык не имеет представления о типах, или с точки зрения типизации: в языке есть только один тип. Язык ассемблера имеет только тип «битовый шаблон», Rexx и Tk имеют только тип «текст», ядро ​​MatLab имеет только тип «комплексная матрица».
• Слабая типизация: существует только несколько выделенных типов и, возможно, синонимов типов для нескольких типов. Например, C использует целые числа для логических, целых чисел, символов, наборов битов и перечислений.
• Строгая типизация: мелкозернистый набор типов, таких как языки ада, виртский язык (паскаль, модула-2), эйфелева

Это полностью противоречит моему личному восприятию, которое было больше похоже на:

• Слабая типизация: объекты имеют типы, но неявно преобразуются в другие типы, когда этого требует контекст. Например, Perl, PHP и JavaScript - это все языки, на которых "1"можно использовать более или менее любой контекст, который 1может.
• Строгая типизация: у объектов есть типы, и не существует неявных преобразований (хотя для их имитации может использоваться перегрузка), поэтому использование объекта в неправильном контексте является ошибкой. В Python индексирование массива со строкой или с плавающей точкой вызывает исключение TypeError; в Haskell это не удастся во время компиляции.

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

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

Насколько я понимаю, первая и последняя характеристики будут называть C слабо типизированными, а вторая будет называть его строго типизированными. Первое и второе будут вызывать Perl и PHP со слабой типизацией, третье будет называть их строго типизированными. Все три описывают Python как строго типизированный.

Я думаю, что большинство людей скажут мне: «Ну, нет консенсуса, нет общепринятого значения терминов». Если эти люди не правы, я был бы рад услышать об этом, но если они правы, то как же исследователи CS описать и сравнить системы типов? Какую терминологию я могу использовать, что менее проблематично?

Как связанный вопрос, я чувствую, что динамическое / статическое различие часто дается в терминах «времени компиляции» и «времени выполнения», что я нахожу неудовлетворительным, учитывая, что то, является ли язык компилируемым, является не столько свойством этого языка как его реализации. Я чувствую, что должно быть чисто семантическое описание динамической и статической типизации; что-то вроде «статический язык - это язык, на котором можно напечатать каждое подвыражение». Я был бы признателен за любые мысли, особенно ссылки, которые вносят ясность в это понятие.

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

• В Фортране существовали вещи, называемые «ОБЩИЕ» области хранения, которые можно было разделять между модулями, но не было проверок, чтобы определить, объявлял ли каждый модуль содержимое хранилища COMMON одними и теми же типами. Таким образом, один модуль может объявить, что конкретный блок хранения COMMON имеет целое число, а другой - число с плавающей запятой, и в результате данные будут повреждены. У Fortran также были операторы «EQUIVALENCE», в результате чего одно и то же хранилище могло быть объявлено как содержащее два разных объекта разных типов.

• В Algol 60 тип параметров процедуры был объявлен просто как «процедура», без указания типов параметров процедуры. Таким образом, можно предположить, что параметр процедуры является целочисленной процедурой, но в качестве аргумента передается реально принимающая процедура. Это приведет к тому же виду коррупции, что и заявления COMMON и EQUIVALENCE. (Тем не менее, Algol 60 действительно устранил старые проблемы.)

• В Паскале были добавлены «вариантные записи», которые были почти такими же, как старые операторы EQUIVALENCE.

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

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

Обратите внимание, что динамически типизированные языки, такие как Lisp, которые выполняют полную проверку типов во время выполнения, «строго типизированы» в смысле защиты представлений. В то же время статически типизированные языки потеряли бы независимость представления, если бы они не проверяли границы массивов. Таким образом, они не являются «строго типизированными» в строгом смысле этого слова. Из-за этих аномальных последствий термин «строго типизированный» вышел из употребления после 70-х годов. Когда Министерство обороны США разработало строгие требования к дизайну Ады, они включали требование, чтобы язык был «строго типизирован». (Кажется, в то время считалось, что идея «строго типизированного» была самоочевидной. Никакого определения не предлагалось. ) Все языковые предложения, представленные в ответ, заявлены как «строго типизированные». Когда Дейкстра проанализировал все языковые предложения, он обнаружил, что ни одно из них не было строго напечатано и, на самом деле, даже не было ясно, что означает этот термин. Смотрите отчетEWD663 . Тем не менее, я вижу, что этот термин снова начинает использоваться благодаря молодому поколению исследователей, которые не знают изменчивой истории этого термина.

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

Новые дебаты о «сильной против слабой типизации», по-видимому, касаются вопроса о том, следует ли разрешать определенные преобразования типов. Разрешение строки, где требуется целое число, является "слабой типизацией" согласно этим людям. В этом есть некоторый смысл, потому что попытка преобразовать строку в целое может потерпеть неудачу, если строка не представляет целое число. Однако преобразование целого числа в строку не имеет этой проблемы. Это было бы примером "слабой типизации" в соответствии с этими людьми? Не имею представления. Я замечаю, что обсуждения в "Википедии" о "слабой типизации" не ссылаются ни на какие рецензируемые публикации. Я не верю, что это последовательная идея.

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

Статья Удая Редди, найденная в его ответе « О понимании типов, абстракции данных и полиморфизме» (1985), дает следующие ответы:

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

Авторитетные ответы можно найти в обзорной статье Карделли и Вегнера: « Понимание типов, абстракция данных и полиморфизм» .

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